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.
@[class]
structure
has_smooth_add
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{H : Type u_3}
[topological_space H]
{E : Type u_4}
[normed_group E]
[normed_space 𝕜 E]
(I : model_with_corners 𝕜 E H)
(G : Type u_5)
[has_add G]
[topological_space G]
[has_continuous_add G]
[charted_space H G] :
Prop
- 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 α.
@[instance]
def
has_smooth_add.to_smooth_manifold_with_corners
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{H : Type u_3}
[topological_space H]
{E : Type u_4}
[normed_group E]
[normed_space 𝕜 E]
(I : model_with_corners 𝕜 E H)
(G : Type u_5)
[has_add G]
[topological_space G]
[has_continuous_add G]
[charted_space H G]
[s : has_smooth_add I G] :
@[class]
structure
has_smooth_mul
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{H : Type u_3}
[topological_space H]
{E : Type u_4}
[normed_group E]
[normed_space 𝕜 E]
(I : model_with_corners 𝕜 E H)
(G : Type u_5)
[has_mul G]
[topological_space G]
[has_continuous_mul G]
[charted_space H G] :
Prop
- 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.
@[instance]
def
has_smooth_mul.to_smooth_manifold_with_corners
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{H : Type u_3}
[topological_space H]
{E : Type u_4}
[normed_group E]
[normed_space 𝕜 E]
(I : model_with_corners 𝕜 E H)
(G : Type u_5)
[has_mul G]
[topological_space G]
[has_continuous_mul G]
[charted_space H G]
[s : has_smooth_mul I G] :
theorem
smooth_add
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{H : Type u_3}
[topological_space H]
{E : Type u_4}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E H}
{G : Type u_5}
[has_add G]
[topological_space G]
[has_continuous_add G]
[charted_space H G]
[has_smooth_add I G] :
theorem
smooth_mul
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{H : Type u_3}
[topological_space H]
{E : Type u_4}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E H}
{G : Type u_5}
[has_mul G]
[topological_space G]
[has_continuous_mul G]
[charted_space H G]
[has_smooth_mul I G] :
theorem
smooth.mul
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{H : Type u_3}
[topological_space H]
{E : Type u_4}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E H}
{G : Type u_5}
[has_mul G]
[topological_space G]
[has_continuous_mul G]
[charted_space H G]
[has_smooth_mul I G]
{E' : Type u_6}
[normed_group E']
[normed_space 𝕜 E']
{H' : Type u_7}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_8}
[topological_space M]
[charted_space H' M]
[smooth_manifold_with_corners I' M]
{f g : M → G}
(hf : smooth I' I f)
(hg : smooth I' I g) :
theorem
smooth.add
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{H : Type u_3}
[topological_space H]
{E : Type u_4}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E H}
{G : Type u_5}
[has_add G]
[topological_space G]
[has_continuous_add G]
[charted_space H G]
[has_smooth_add I G]
{E' : Type u_6}
[normed_group E']
[normed_space 𝕜 E']
{H' : Type u_7}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_8}
[topological_space M]
[charted_space H' M]
[smooth_manifold_with_corners I' M]
{f g : M → G}
(hf : smooth I' I f)
(hg : smooth I' I g) :
theorem
smooth_mul_left
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{H : Type u_3}
[topological_space H]
{E : Type u_4}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E H}
{G : Type u_5}
[has_mul G]
[topological_space G]
[has_continuous_mul G]
[charted_space H G]
[has_smooth_mul I G]
{a : G} :
theorem
smooth_add_left
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{H : Type u_3}
[topological_space H]
{E : Type u_4}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E H}
{G : Type u_5}
[has_add G]
[topological_space G]
[has_continuous_add G]
[charted_space H G]
[has_smooth_add I G]
{a : G} :
theorem
smooth_mul_right
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{H : Type u_3}
[topological_space H]
{E : Type u_4}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E H}
{G : Type u_5}
[has_mul G]
[topological_space G]
[has_continuous_mul G]
[charted_space H G]
[has_smooth_mul I G]
{a : G} :
theorem
smooth_add_right
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{H : Type u_3}
[topological_space H]
{E : Type u_4}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E H}
{G : Type u_5}
[has_add G]
[topological_space G]
[has_continuous_add G]
[charted_space H G]
[has_smooth_add I G]
{a : G} :
theorem
smooth_on.mul
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{H : Type u_3}
[topological_space H]
{E : Type u_4}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E H}
{G : Type u_5}
[has_mul G]
[topological_space G]
[has_continuous_mul G]
[charted_space H G]
[has_smooth_mul I G]
{E' : Type u_6}
[normed_group E']
[normed_space 𝕜 E']
{H' : Type u_7}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_8}
[topological_space M]
[charted_space H' M]
[smooth_manifold_with_corners I' M]
{f g : M → G}
{s : set M}
(hf : smooth_on I' I f s)
(hg : smooth_on I' I g s) :
theorem
smooth_on.add
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{H : Type u_3}
[topological_space H]
{E : Type u_4}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E H}
{G : Type u_5}
[has_add G]
[topological_space G]
[has_continuous_add G]
[charted_space H G]
[has_smooth_add I G]
{E' : Type u_6}
[normed_group E']
[normed_space 𝕜 E']
{H' : Type u_7}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_8}
[topological_space M]
[charted_space H' M]
[smooth_manifold_with_corners I' M]
{f g : M → G}
{s : set M}
(hf : smooth_on I' I f s)
(hg : smooth_on I' I g s) :
@[instance]
def
has_smooth_add.sum
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(G : Type u_4)
[topological_space G]
[charted_space H G]
[has_add G]
[has_continuous_add G]
[has_smooth_add I G]
{E' : Type u_5}
[normed_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
(G' : Type u_7)
[topological_space G']
[charted_space H' G']
[has_add G']
[has_continuous_add G']
[has_smooth_add I' G'] :
has_smooth_add (I.prod I') (G × G')
@[instance]
def
has_smooth_mul.prod
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(G : Type u_4)
[topological_space G]
[charted_space H G]
[has_mul G]
[has_continuous_mul G]
[has_smooth_mul I G]
{E' : Type u_5}
[normed_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
(G' : Type u_7)
[topological_space G']
[charted_space H' G']
[has_mul G']
[has_continuous_mul G']
[has_smooth_mul I' G'] :
has_smooth_mul (I.prod I') (G × G')
structure
smooth_add_monoid_morphism
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_4}
[normed_group E']
[normed_space 𝕜 E']
(I : model_with_corners 𝕜 E E)
(I' : model_with_corners 𝕜 E' E')
(G : Type u_5)
[topological_space G]
[charted_space E G]
[add_monoid G]
[has_continuous_add G]
[has_smooth_add I G]
(G' : Type u_6)
[topological_space G']
[charted_space E' G']
[add_monoid G']
[has_continuous_add G']
[has_smooth_add I' G'] :
Type (max u_5 u_6)
- to_add_monoid_hom : G →+ G'
- smooth_to_fun : smooth I I' c.to_add_monoid_hom.to_fun
Morphism of additive smooth monoids.
structure
smooth_monoid_morphism
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_4}
[normed_group E']
[normed_space 𝕜 E']
(I : model_with_corners 𝕜 E E)
(I' : model_with_corners 𝕜 E' E')
(G : Type u_5)
[topological_space G]
[charted_space E G]
[monoid G]
[has_continuous_mul G]
[has_smooth_mul I G]
(G' : Type u_6)
[topological_space G']
[charted_space E' G']
[monoid G']
[has_continuous_mul G']
[has_smooth_mul I' G'] :
Type (max u_5 u_6)
- to_monoid_hom : G →* G'
- smooth_to_fun : smooth I I' c.to_monoid_hom.to_fun
Morphism of smooth monoids.
@[instance]
def
smooth_add_monoid_morphism.has_zero
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_4}
[normed_group E']
[normed_space 𝕜 E']
{I : model_with_corners 𝕜 E E}
{I' : model_with_corners 𝕜 E' E'}
{G : Type u_5}
[topological_space G]
[charted_space E G]
[add_monoid G]
[has_continuous_add G]
[has_smooth_add I G]
{G' : Type u_6}
[topological_space G']
[charted_space E' G']
[add_monoid G']
[has_continuous_add G']
[has_smooth_add I' G'] :
has_zero (smooth_add_monoid_morphism I I' G G')
@[instance]
def
smooth_monoid_morphism.has_one
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_4}
[normed_group E']
[normed_space 𝕜 E']
{I : model_with_corners 𝕜 E E}
{I' : model_with_corners 𝕜 E' E'}
{G : Type u_5}
[topological_space G]
[charted_space E G]
[monoid G]
[has_continuous_mul G]
[has_smooth_mul I G]
{G' : Type u_6}
[topological_space G']
[charted_space E' G']
[monoid G']
[has_continuous_mul G']
[has_smooth_mul I' G'] :
has_one (smooth_monoid_morphism I I' G G')
Equations
- smooth_monoid_morphism.has_one = {one := {to_monoid_hom := {to_fun := 1.to_fun, map_one' := _, map_mul' := _}, smooth_to_fun := _}}
@[instance]
def
smooth_add_monoid_morphism.inhabited
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_4}
[normed_group E']
[normed_space 𝕜 E']
{I : model_with_corners 𝕜 E E}
{I' : model_with_corners 𝕜 E' E'}
{G : Type u_5}
[topological_space G]
[charted_space E G]
[add_monoid G]
[has_continuous_add G]
[has_smooth_add I G]
{G' : Type u_6}
[topological_space G']
[charted_space E' G']
[add_monoid G']
[has_continuous_add G']
[has_smooth_add I' G'] :
inhabited (smooth_add_monoid_morphism I I' G G')
@[instance]
def
smooth_monoid_morphism.inhabited
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_4}
[normed_group E']
[normed_space 𝕜 E']
{I : model_with_corners 𝕜 E E}
{I' : model_with_corners 𝕜 E' E'}
{G : Type u_5}
[topological_space G]
[charted_space E G]
[monoid G]
[has_continuous_mul G]
[has_smooth_mul I G]
{G' : Type u_6}
[topological_space G']
[charted_space E' G']
[monoid G']
[has_continuous_mul G']
[has_smooth_mul I' G'] :
inhabited (smooth_monoid_morphism I I' G G')
Equations
@[instance]
def
smooth_add_monoid_morphism.has_coe_to_fun
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_4}
[normed_group E']
[normed_space 𝕜 E']
{I : model_with_corners 𝕜 E E}
{I' : model_with_corners 𝕜 E' E'}
{G : Type u_5}
[topological_space G]
[charted_space E G]
[add_monoid G]
[has_continuous_add G]
[has_smooth_add I G]
{G' : Type u_6}
[topological_space G']
[charted_space E' G']
[add_monoid G']
[has_continuous_add G']
[has_smooth_add I' G'] :
has_coe_to_fun (smooth_add_monoid_morphism I I' G G')
@[instance]
def
smooth_monoid_morphism.has_coe_to_fun
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_4}
[normed_group E']
[normed_space 𝕜 E']
{I : model_with_corners 𝕜 E E}
{I' : model_with_corners 𝕜 E' E'}
{G : Type u_5}
[topological_space G]
[charted_space E G]
[monoid G]
[has_continuous_mul G]
[has_smooth_mul I G]
{G' : Type u_6}
[topological_space G']
[charted_space E' G']
[monoid G']
[has_continuous_mul G']
[has_smooth_mul I' G'] :
has_coe_to_fun (smooth_monoid_morphism I I' G G')
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}
structure
has_smooth_add_core
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{H : Type u_3}
[topological_space H]
{E : Type u_4}
[normed_group E]
[normed_space 𝕜 E]
(I : model_with_corners 𝕜 E H)
(G : Type u_5)
[has_add G]
[topological_space G]
[charted_space H G] :
Prop
- 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.
structure
has_smooth_mul_core
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{H : Type u_3}
[topological_space H]
{E : Type u_4}
[normed_group E]
[normed_space 𝕜 E]
(I : model_with_corners 𝕜 E H)
(G : Type u_5)
[has_mul G]
[topological_space G]
[charted_space H G] :
Prop
- 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.
theorem
has_smooth_mul_core.to_has_continuous_mul
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E E}
{G : Type u_5}
[topological_space G]
[charted_space E G]
[group G]
(c : has_smooth_mul_core I G) :
theorem
has_smooth_add_core.to_has_continuous_add
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E E}
{G : Type u_5}
[topological_space G]
[charted_space E G]
[add_group G]
(c : has_smooth_add_core I G) :
theorem
has_smooth_mul_core.to_has_smooth_mul
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E E}
{G : Type u_5}
[topological_space G]
[charted_space E G]
[group G]
(c : has_smooth_mul_core I G) :
has_smooth_mul I G
theorem
has_smooth_add_core.to_has_smooth_add
{𝕜 : Type u_2}
[nondiscrete_normed_field 𝕜]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E E}
{G : Type u_5}
[topological_space G]
[charted_space E G]
[add_group G]
(c : has_smooth_add_core I G) :
has_smooth_add I G