Continuous Monoid Homs #
This file defines the space of continuous homomorphisms between two topological groups.
Main definitions #
ContinuousMonoidHom A B
: The continuous homomorphismsA →* B
.ContinuousAddMonoidHom A B
: The continuous additive homomorphismsA →+ B
.
The type of continuous additive monoid homomorphisms from A
to B
.
- toFun : A → B
- map_add' (x y : A) : (↑self.toAddMonoidHom).toFun (x + y) = (↑self.toAddMonoidHom).toFun x + (↑self.toAddMonoidHom).toFun y
- continuous_toFun : Continuous (↑self.toAddMonoidHom).toFun
Instances For
The type of continuous monoid homomorphisms from A
to B
.
When possible, instead of parametrizing results over (f : ContinuousMonoidHom A B)
,
you should parametrize
over (F : Type*) [FunLike F A B] [ContinuousMapClass F A B] [MonoidHomClass F A B] (f : F)
.
When you extend this structure,
make sure to extend ContinuousMapClass
and/or MonoidHomClass
, if needed.
- toFun : A → B
- map_mul' (x y : A) : (↑self.toMonoidHom).toFun (x * y) = (↑self.toMonoidHom).toFun x * (↑self.toMonoidHom).toFun y
- continuous_toFun : Continuous (↑self.toMonoidHom).toFun
Instances For
The type of continuous monoid homomorphisms from A
to B
.
Equations
Instances For
The type of continuous monoid homomorphisms from A
to B
.
Equations
Instances For
Equations
Equations
Turn an element of a type F
satisfying MonoidHomClass F A B
and ContinuousMapClass F A B
into aContinuousMonoidHom
. This is declared as the default coercion from F
to
(A →ₜ* B)
.
Equations
Instances For
Turn an element of a type F
satisfying
AddMonoidHomClass F A B
and ContinuousMapClass F A B
into aContinuousAddMonoidHom
.
This is declared as the default coercion from F
to ContinuousAddMonoidHom A B
.
Equations
Instances For
Any type satisfying MonoidHomClass
and ContinuousMapClass
can be cast into
ContinuousMonoidHom
via ContinuousMonoidHom.toContinuousMonoidHom
.
Equations
Any type satisfying AddMonoidHomClass
and ContinuousMapClass
can be cast into
ContinuousAddMonoidHom
via ContinuousAddMonoidHom.toContinuousAddMonoidHom
.
Equations
Composition of two continuous homomorphisms.
Equations
Instances For
Composition of two continuous homomorphisms.
Equations
Instances For
Product of two continuous homomorphisms on the same space.
Equations
Instances For
Product of two continuous homomorphisms on the same space.
Equations
Instances For
Product of two continuous homomorphisms on different spaces.
Equations
Instances For
Product of two continuous homomorphisms on different spaces.
Equations
Instances For
The trivial continuous homomorphism.
Equations
The trivial continuous homomorphism.
Equations
Equations
Equations
The identity continuous homomorphism.
Equations
Instances For
The identity continuous homomorphism.
Equations
Instances For
The continuous homomorphism given by projection onto the first factor.
Equations
Instances For
The continuous homomorphism given by projection onto the first factor.
Equations
Instances For
The continuous homomorphism given by projection onto the second factor.
Equations
Instances For
The continuous homomorphism given by projection onto the second factor.
Equations
Instances For
The continuous homomorphism given by inclusion of the first factor.
Equations
Instances For
The continuous homomorphism given by inclusion of the first factor.
Equations
Instances For
The continuous homomorphism given by inclusion of the second factor.
Equations
Instances For
The continuous homomorphism given by inclusion of the second factor.
Equations
Instances For
The continuous homomorphism given by the diagonal embedding.
Equations
Instances For
The continuous homomorphism given by the diagonal embedding.
Equations
Instances For
The continuous homomorphism given by swapping components.
Equations
Instances For
The continuous homomorphism given by swapping components.
Equations
Instances For
The continuous homomorphism given by multiplication.
Equations
Instances For
The continuous homomorphism given by addition.
Equations
Instances For
Equations
Equations
Coproduct of two continuous homomorphisms to the same space.
Equations
Instances For
Coproduct of two continuous homomorphisms to the same space.
Equations
Instances For
The continuous homomorphism given by inversion.
Equations
Instances For
The continuous homomorphism given by negation.
Equations
Instances For
Equations
Equations
For f : F
where F
is a class of continuous monoid hom, this yields an element
ContinuousMonoidHom A B
.
Equations
Instances For
For f : F
where F
is a class of continuous additive monoid hom, this yields
an element ContinuousAddMonoidHom A B
.
Equations
Instances For
Continuous MulEquiv #
This section defines the space of continuous isomorphisms between two topological groups.
Main definitions #
The structure of two-sided continuous isomorphisms between additive groups. Note that both the map and its inverse have to be continuous.
- toFun : G → H
- invFun : H → G
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
- continuous_toFun : Continuous self.toFun
- continuous_invFun : Continuous self.invFun
Instances For
The structure of two-sided continuous isomorphisms between groups. Note that both the map and its inverse have to be continuous.
- toFun : G → H
- invFun : H → G
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
- continuous_toFun : Continuous self.toFun
- continuous_invFun : Continuous self.invFun
Instances For
The structure of two-sided continuous isomorphisms between groups. Note that both the map and its inverse have to be continuous.
Equations
Instances For
The structure of two-sided continuous isomorphisms between additive groups. Note that both the map and its inverse have to be continuous.
Equations
Instances For
Equations
Equations
Two continuous multiplicative isomorphisms agree if they are defined by the same underlying function.
Two continuous additive isomorphisms agree if they are defined by the same underlying function.
Makes a continuous multiplicative isomorphism from a homeomorphism which preserves multiplication.
Equations
Instances For
Makes an continuous additive isomorphism from a homeomorphism which preserves addition.
Equations
Instances For
The identity map is a continuous multiplicative isomorphism.
Equations
Instances For
The identity map is a continuous additive isomorphism.
Equations
Instances For
Equations
Equations
The inverse of a ContinuousMulEquiv.
Equations
Instances For
The inverse of a ContinuousAddEquiv.
Equations
Instances For
e.symm
is a right inverse of e
, written as e (e.symm y) = y
.
e.symm
is a right inverse of e
, written as e (e.symm y) = y
.
The composition of two ContinuousMulEquiv.
Equations
Instances For
The composition of two ContinuousAddEquiv.
Equations
Instances For
The MulEquiv
between two monoids with a unique element.
Equations
Instances For
The AddEquiv
between two AddMonoid
s with a unique element.
Equations
Instances For
There is a unique monoid homomorphism between two monoids with a unique element.
Equations
There is a unique additive monoid homomorphism between two additive monoids with a unique element.