Smooth monoid #
A smooth monoid is a monoid that is also a smooth manifold, in which multiplication is a smooth map
of the product manifold G
× G
into G
.
In this file we define the basic structures to talk about smooth monoids: has_smooth_mul
and its
additive counterpart has_smooth_add
. These structures are general enough to also talk about smooth
semigroups.
- compatible : ∀ {e e' : local_homeomorph G H}, e ∈ atlas H G → e' ∈ atlas H G → e.symm ≫ₕ e' ∈ times_cont_diff_groupoid ⊤ I
- smooth_add : smooth (I.prod I) I (λ (p : G × G), p.fst + p.snd)
Basic hypothesis to talk about a smooth (Lie) additive monoid or a smooth additive
semigroup. A smooth additive monoid over α
, for example, is obtained by requiring both the
instances add_monoid α
and has_smooth_add α
.
- compatible : ∀ {e e' : local_homeomorph G H}, e ∈ atlas H G → e' ∈ atlas H G → e.symm ≫ₕ e' ∈ times_cont_diff_groupoid ⊤ I
- smooth_mul : smooth (I.prod I) I (λ (p : G × G), (p.fst) * p.snd)
Basic hypothesis to talk about a smooth (Lie) monoid or a smooth semigroup.
A smooth monoid over G
, for example, is obtained by requiring both the instances monoid G
and has_smooth_mul I G
.
- to_add_monoid_hom : G →+ G'
- smooth_to_fun : smooth I I' c.to_add_monoid_hom.to_fun
Morphism of additive smooth monoids.
- to_monoid_hom : G →* G'
- smooth_to_fun : smooth I I' c.to_monoid_hom.to_fun
Morphism of smooth monoids.
Equations
- smooth_monoid_morphism.has_one = {one := {to_monoid_hom := {to_fun := 1.to_fun, map_one' := _, map_mul' := _}, smooth_to_fun := _}}
Equations
Equations
- smooth_monoid_morphism.has_coe_to_fun = {F := λ (a : smooth_monoid_morphism I I' G G'), G → G', coe := λ (a : smooth_monoid_morphism I I' G G'), a.to_monoid_hom.to_fun}
- to_smooth_manifold_with_corners : smooth_manifold_with_corners I G
- smooth_add : smooth (I.prod I) I (λ (p : G × G), p.fst + p.snd)
Sometimes one might want to define a smooth additive monoid G
without having proved previously
that G
is a topological additive monoid. In such case it is possible to use has_smooth_add_core
that does not require such instance, and then get a smooth additive monoid by invoking
to_has_smooth_add
.
- to_smooth_manifold_with_corners : smooth_manifold_with_corners I G
- smooth_mul : smooth (I.prod I) I (λ (p : G × G), (p.fst) * p.snd)
Sometimes one might want to define a smooth monoid G
without having proved previously that G
is a topological monoid. In such case it is possible to use has_smooth_mul_core
that does not
require such instance, and then get a smooth monoid by invoking to_has_smooth_mul
.