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
.
- toFun : A → B
- map_zero' : ZeroHom.toFun (↑s.toAddMonoidHom) 0 = 0
- map_add' : ∀ (x y : A), ZeroHom.toFun (↑s.toAddMonoidHom) (x + y) = ZeroHom.toFun (↑s.toAddMonoidHom) x + ZeroHom.toFun (↑s.toAddMonoidHom) y
- continuous_toFun : Continuous s.toFun
Proof of continuity of the Hom.
The type of continuous additive monoid homomorphisms from A
to B
.
Instances For
- toFun : A → B
- map_one' : OneHom.toFun (↑s.toMonoidHom) 1 = 1
- map_mul' : ∀ (x y : A), OneHom.toFun (↑s.toMonoidHom) (x * y) = OneHom.toFun (↑s.toMonoidHom) x * OneHom.toFun (↑s.toMonoidHom) y
- continuous_toFun : Continuous s.toFun
Proof of continuity of the Hom.
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*) [ContinuousMonoidHomClass F A B] (f : F)
.
When you extend this structure, make sure to extend ContinuousAddMonoidHomClass
.
Instances For
- coe : F → A → B
- coe_injective' : Function.Injective FunLike.coe
- map_zero : ∀ (f : F), ↑f 0 = 0
- map_continuous : ∀ (f : F), Continuous ↑f
Proof of the continuity of the map.
ContinuousAddMonoidHomClass F A B
states that F
is a type of continuous additive monoid
homomorphisms.
You should also extend this typeclass when you extend ContinuousAddMonoidHom
.
Instances
- coe : F → A → B
- coe_injective' : Function.Injective FunLike.coe
- map_one : ∀ (f : F), ↑f 1 = 1
- map_continuous : ∀ (f : F), Continuous ↑f
Proof of the continuity of the map.
ContinuousMonoidHomClass F A B
states that F
is a type of continuous additive monoid
homomorphisms.
You should also extend this typeclass when you extend ContinuousMonoidHom
.
Instances
Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun
.
Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun
directly.
Reinterpret a ContinuousAddMonoidHom
as a ContinuousMap
.
Instances For
Reinterpret a ContinuousMonoidHom
as a ContinuousMap
.
Instances For
Construct a ContinuousAddMonoidHom
from a Continuous
AddMonoidHom
.
Instances For
Construct a ContinuousMonoidHom
from a Continuous
MonoidHom
.
Instances For
Composition of two continuous homomorphisms.
Instances For
Composition of two continuous homomorphisms.
Instances For
Product of two continuous homomorphisms on the same space.
Instances For
Product of two continuous homomorphisms on the same space.
Instances For
Product of two continuous homomorphisms on different spaces.
Instances For
Product of two continuous homomorphisms on different spaces.
Instances For
The trivial continuous homomorphism.
Instances For
The trivial continuous homomorphism.
Instances For
The identity continuous homomorphism.
Instances For
The identity continuous homomorphism.
Instances For
The continuous homomorphism given by projection onto the first factor.
Instances For
The continuous homomorphism given by projection onto the first factor.
Instances For
The continuous homomorphism given by projection onto the second factor.
Instances For
The continuous homomorphism given by projection onto the second factor.
Instances For
The continuous homomorphism given by inclusion of the first factor.
Instances For
The continuous homomorphism given by inclusion of the first factor.
Instances For
The continuous homomorphism given by inclusion of the second factor.
Instances For
The continuous homomorphism given by inclusion of the second factor.
Instances For
The continuous homomorphism given by the diagonal embedding.
Instances For
The continuous homomorphism given by the diagonal embedding.
Instances For
The continuous homomorphism given by swapping components.
Instances For
The continuous homomorphism given by swapping components.
Instances For
The continuous homomorphism given by addition.
Instances For
The continuous homomorphism given by multiplication.
Instances For
The continuous homomorphism given by negation.
Instances For
The continuous homomorphism given by inversion.
Instances For
Coproduct of two continuous homomorphisms to the same space.
Instances For
Coproduct of two continuous homomorphisms to the same space.
Instances For
Instances For
ContinuousAddMonoidHom _ f
is a functor.
Instances For
ContinuousMonoidHom _ f
is a functor.
Instances For
ContinuousAddMonoidHom f _
is a functor.
Instances For
ContinuousMonoidHom f _
is a functor.
Instances For
The Pontryagin dual of A
is the group of continuous homomorphism A → circle
.
Instances For
PontryaginDual
is a functor.
Instances For
ContinuousMonoidHom.dual
as a ContinuousMonoidHom
.