mathlib documentation

geometry.manifold.algebra.monoid

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

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 α.

Instances
@[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

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.

Instances
@[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] :
smooth (I.prod I) I (λ (p : G × G), p.fst + p.snd)

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] :
smooth (I.prod I) I (λ (p : G × G), (p.fst) * p.snd)

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) :
smooth I' I (f * 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) :
smooth I' I (f + 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} :
smooth I I (λ (b : G), a * b)

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} :
smooth I I (λ (b : G), a + b)

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} :
smooth I I (λ (b : G), b * a)

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} :
smooth I I (λ (b : G), b + a)

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) :
smooth_on I' I (f * 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) :
smooth_on I' I (f + 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)

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)

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'] :

@[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'] :

Equations
@[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'] :

@[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'] :

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'] :

@[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'] :

Equations
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

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

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) :

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) :