# mathlibdocumentation

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} {H : Type u_3} {E : Type u_4} [normed_group E] [ E] (I : H) (G : Type u_5) [has_add G] [ 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} {H : Type u_3} {E : Type u_4} [normed_group E] [ E] (I : H) (G : Type u_5) [has_add G] [ G] [s : G] :

@[class]
structure has_smooth_mul {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [normed_group E] [ E] (I : H) (G : Type u_5) [has_mul G] [ 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} {H : Type u_3} {E : Type u_4} [normed_group E] [ E] (I : H) (G : Type u_5) [has_mul G] [ G] [s : G] :

theorem smooth_add {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [normed_group E] [ E] {I : H} {G : Type u_5} [has_add G] [ G] [ G] :
smooth (I.prod I) I (λ (p : G × G), p.fst + p.snd)

theorem smooth_mul {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [normed_group E] [ E] {I : H} {G : Type u_5} [has_mul G] [ G] [ G] :
smooth (I.prod I) I (λ (p : G × G), (p.fst) * p.snd)

theorem smooth.mul {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [normed_group E] [ E] {I : H} {G : Type u_5} [has_mul G] [ G] [ G] {E' : Type u_6} [normed_group E'] [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ 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} {H : Type u_3} {E : Type u_4} [normed_group E] [ E] {I : H} {G : Type u_5} [has_add G] [ G] [ G] {E' : Type u_6} [normed_group E'] [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ 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} {H : Type u_3} {E : Type u_4} [normed_group E] [ E] {I : H} {G : Type u_5} [has_mul G] [ G] [ G] {a : G} :
I (λ (b : G), a * b)

theorem smooth_add_left {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [normed_group E] [ E] {I : H} {G : Type u_5} [has_add G] [ G] [ G] {a : G} :
I (λ (b : G), a + b)

theorem smooth_mul_right {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [normed_group E] [ E] {I : H} {G : Type u_5} [has_mul G] [ G] [ G] {a : G} :
I (λ (b : G), b * a)

theorem smooth_add_right {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [normed_group E] [ E] {I : H} {G : Type u_5} [has_add G] [ G] [ G] {a : G} :
I (λ (b : G), b + a)

theorem smooth_on.mul {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [normed_group E] [ E] {I : H} {G : Type u_5} [has_mul G] [ G] [ G] {E' : Type u_6} [normed_group E'] [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {f g : M → G} {s : set M} (hf : I f s) (hg : I g s) :
I (f * g) s

theorem smooth_on.add {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [normed_group E] [ E] {I : H} {G : Type u_5} [has_add G] [ G] [ G] {E' : Type u_6} [normed_group E'] [ E'] {H' : Type u_7} {I' : H'} {M : Type u_8} [ M] {f g : M → G} {s : set M} (hf : I f s) (hg : I g s) :
I (f + g) s

@[instance]
def has_smooth_add.sum {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) (G : Type u_4) [ G] [has_add G] [ G] {E' : Type u_5} [normed_group E'] [ E'] {H' : Type u_6} (I' : H') (G' : Type u_7) [ G'] [has_add G'] [ G'] :
has_smooth_add (I.prod I') (G × G')

@[instance]
def has_smooth_mul.prod {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) (G : Type u_4) [ G] [has_mul G] [ G] {E' : Type u_5} [normed_group E'] [ E'] {H' : Type u_6} (I' : H') (G' : Type u_7) [ G'] [has_mul G'] [ G'] :
has_smooth_mul (I.prod I') (G × G')

structure smooth_add_monoid_morphism {𝕜 : Type u_2} {E : Type u_3} [normed_group E] [ E] {E' : Type u_4} [normed_group E'] [ E'] (I : E) (I' : E') (G : Type u_5) [ G] [add_monoid G] [ G] (G' : Type u_6) [ G'] [add_monoid G'] [ G'] :
Type (max u_5 u_6)

structure smooth_monoid_morphism {𝕜 : Type u_2} {E : Type u_3} [normed_group E] [ E] {E' : Type u_4} [normed_group E'] [ E'] (I : E) (I' : E') (G : Type u_5) [ G] [monoid G] [ G] (G' : Type u_6) [ G'] [monoid G'] [ G'] :
Type (max u_5 u_6)

Morphism of smooth monoids.

@[instance]
def smooth_add_monoid_morphism.has_zero {𝕜 : Type u_2} {E : Type u_3} [normed_group E] [ E] {E' : Type u_4} [normed_group E'] [ E'] {I : E} {I' : E'} {G : Type u_5} [ G] [add_monoid G] [ G] {G' : Type u_6} [ G'] [add_monoid G'] [ G'] :
has_zero G G')

@[instance]
def smooth_monoid_morphism.has_one {𝕜 : Type u_2} {E : Type u_3} [normed_group E] [ E] {E' : Type u_4} [normed_group E'] [ E'] {I : E} {I' : E'} {G : Type u_5} [ G] [monoid G] [ G] {G' : Type u_6} [ G'] [monoid G'] [ G'] :
has_one G G')

Equations
@[instance]
def smooth_add_monoid_morphism.inhabited {𝕜 : Type u_2} {E : Type u_3} [normed_group E] [ E] {E' : Type u_4} [normed_group E'] [ E'] {I : E} {I' : E'} {G : Type u_5} [ G] [add_monoid G] [ G] {G' : Type u_6} [ G'] [add_monoid G'] [ G'] :
inhabited G G')

@[instance]
def smooth_monoid_morphism.inhabited {𝕜 : Type u_2} {E : Type u_3} [normed_group E] [ E] {E' : Type u_4} [normed_group E'] [ E'] {I : E} {I' : E'} {G : Type u_5} [ G] [monoid G] [ G] {G' : Type u_6} [ G'] [monoid G'] [ G'] :
inhabited G G')

Equations
@[instance]
def smooth_add_monoid_morphism.has_coe_to_fun {𝕜 : Type u_2} {E : Type u_3} [normed_group E] [ E] {E' : Type u_4} [normed_group E'] [ E'] {I : E} {I' : E'} {G : Type u_5} [ G] [add_monoid G] [ G] {G' : Type u_6} [ G'] [add_monoid G'] [ G'] :

@[instance]
def smooth_monoid_morphism.has_coe_to_fun {𝕜 : Type u_2} {E : Type u_3} [normed_group E] [ E] {E' : Type u_4} [normed_group E'] [ E'] {I : E} {I' : E'} {G : Type u_5} [ G] [monoid G] [ G] {G' : Type u_6} [ G'] [monoid G'] [ G'] :

Equations
structure has_smooth_add_core {𝕜 : Type u_2} {H : Type u_3} {E : Type u_4} [normed_group E] [ E] (I : H) (G : Type u_5) [has_add G] [ G] :
Prop
• to_smooth_manifold_with_corners :
• 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} {H : Type u_3} {E : Type u_4} [normed_group E] [ E] (I : H) (G : Type u_5) [has_mul G] [ G] :
Prop
• to_smooth_manifold_with_corners :
• 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} {E : Type u_3} [normed_group E] [ E] {I : E} {G : Type u_5} [ G] [group G] (c : G) :

theorem has_smooth_add_core.to_has_continuous_add {𝕜 : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : E} {G : Type u_5} [ G] [add_group G] (c : G) :

theorem has_smooth_mul_core.to_has_smooth_mul {𝕜 : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : E} {G : Type u_5} [ G] [group G] (c : G) :

theorem has_smooth_add_core.to_has_smooth_add {𝕜 : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : E} {G : Type u_5} [ G] [add_group G] (c : G) :