# 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_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] (I : H) (G : Type u_4) [has_add G] [ G] :
Prop
• to_smooth_manifold_with_corners :
• 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 α.

Instances
@[class]
structure has_smooth_mul {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] (I : H) (G : Type u_4) [has_mul G] [ G] :
Prop
• to_smooth_manifold_with_corners :
• 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.

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

If the addition is smooth, then it is continuous. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].

theorem has_continuous_mul_of_smooth {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] (I : H) {G : Type u_4} [has_mul G] [ G] [ G] :

If the multiplication is smooth, then it is continuous. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].

theorem smooth.mul {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [has_mul G] [ G] [ G] {E' : Type u_5} [normed_group E'] [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ 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_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [has_add G] [ G] [ G] {E' : Type u_5} [normed_group E'] [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ 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_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [has_mul G] [ G] [ G] {a : G} :
I (λ (b : G), a * b)
theorem smooth_add_left {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [has_add G] [ G] [ G] {a : G} :
I (λ (b : G), a + b)
theorem smooth_mul_right {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [has_mul G] [ G] [ G] {a : G} :
I (λ (b : G), b * a)
theorem smooth_add_right {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [has_add G] [ G] [ G] {a : G} :
I (λ (b : G), b + a)
theorem smooth_on.mul {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [has_mul G] [ G] [ G] {E' : Type u_5} [normed_group E'] [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ 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_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [has_add G] [ G] [ G] {E' : Type u_5} [normed_group E'] [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {f g : M → G} {s : set M} (hf : I f s) (hg : I g s) :
I (f + g) s
def smooth_left_mul {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] (I : H) {G : Type u_4} [has_mul G] [ G] [ G] (g : G) :

Left multiplication by g. It is meant to mimic the usual notation in Lie groups. Lemmas involving smooth_left_mul with the notation 𝑳 usually use L instead of 𝑳 in the names.

Equations
def smooth_right_mul {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] (I : H) {G : Type u_4} [has_mul G] [ G] [ G] (g : G) :

Right multiplication by g. It is meant to mimic the usual notation in Lie groups. Lemmas involving smooth_right_mul with the notation 𝑹 usually use R instead of 𝑹 in the names.

Equations
@[simp]
theorem L_apply {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] (I : H) {G : Type u_4} [has_mul G] [ G] [ G] (g h : G) :
(𝑳 I g) h = g * h
@[simp]
theorem R_apply {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] (I : H) {G : Type u_4} [has_mul G] [ G] [ G] (g h : G) :
(𝑹 I g) h = h * g
@[simp]
theorem L_mul {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] (I : H) {G : Type u_4} [semigroup G] [ G] [ G] (g h : G) :
𝑳 I (g * h) = (𝑳 I g).comp (𝑳 I h)
@[simp]
theorem R_mul {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] (I : H) {G : Type u_4} [semigroup G] [ G] [ G] (g h : G) :
𝑹 I (g * h) = (𝑹 I h).comp (𝑹 I g)
theorem smooth_left_mul_one {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] (I : H) {G' : Type u_8} [monoid G'] [ G'] [ G'] (g' : G') :
(𝑳 I g') 1 = g'
theorem smooth_right_mul_one {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] (I : H) {G' : Type u_8} [monoid G'] [ G'] [ G'] (g' : G') :
(𝑹 I g') 1 = g'
@[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')
theorem smooth_pow {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [monoid G] [ G] [ G] (n : ) :
I (λ (a : G), a ^ n)
structure smooth_add_monoid_morphism {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {H' : Type u_5} {E' : Type u_6} [normed_group E'] [ E'] (I : H) (I' : H') (G : Type u_8) [ G] [add_monoid G] [ G] (G' : Type u_9) [ G'] [add_monoid G'] [ G'] :
Type (max u_8 u_9)

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

Morphism of smooth monoids.

@[instance]
def smooth_add_monoid_morphism.has_zero {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [add_monoid G] [ G] [ G] {H' : Type u_5} {E' : Type u_6} [normed_group E'] [ E'] {I' : H'} {G' : Type u_7} [add_monoid G'] [ G'] [ G'] :
has_zero G G')
Equations
@[instance]
def smooth_monoid_morphism.has_one {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [monoid G] [ G] [ G] {H' : Type u_5} {E' : Type u_6} [normed_group E'] [ E'] {I' : H'} {G' : Type u_7} [monoid G'] [ G'] [ G'] :
has_one G G')
Equations
@[instance]
def smooth_add_monoid_morphism.inhabited {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [add_monoid G] [ G] [ G] {H' : Type u_5} {E' : Type u_6} [normed_group E'] [ E'] {I' : H'} {G' : Type u_7} [add_monoid G'] [ G'] [ G'] :
inhabited G G')
Equations
@[instance]
def smooth_monoid_morphism.inhabited {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [monoid G] [ G] [ G] {H' : Type u_5} {E' : Type u_6} [normed_group E'] [ E'] {I' : H'} {G' : Type u_7} [monoid G'] [ G'] [ G'] :
inhabited G G')
Equations
@[instance]
def smooth_add_monoid_morphism.has_coe_to_fun {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [add_monoid G] [ G] [ G] {H' : Type u_5} {E' : Type u_6} [normed_group E'] [ E'] {I' : H'} {G' : Type u_7} [add_monoid G'] [ G'] [ G'] :
has_coe_to_fun G G') (λ (_x : G'), G → G')
Equations
@[instance]
def smooth_monoid_morphism.has_coe_to_fun {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [monoid G] [ G] [ G] {H' : Type u_5} {E' : Type u_6} [normed_group E'] [ E'] {I' : H'} {G' : Type u_7} [monoid G'] [ G'] [ G'] :
has_coe_to_fun G G') (λ (_x : G G'), G → G')
Equations
theorem smooth_finset_sum' {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [ G] [ G] {E' : Type u_5} [normed_group E'] [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {ι : Type u_8} {s : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i ssmooth I' I (f i)) :
smooth I' I (∑ (i : ι) in s, f i)
theorem smooth_finset_prod' {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [comm_monoid G] [ G] [ G] {E' : Type u_5} [normed_group E'] [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {ι : Type u_8} {s : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i ssmooth I' I (f i)) :
smooth I' I (∏ (i : ι) in s, f i)
theorem smooth_finset_prod {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [comm_monoid G] [ G] [ G] {E' : Type u_5} [normed_group E'] [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {ι : Type u_8} {s : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i ssmooth I' I (f i)) :
smooth I' I (λ (x : M), ∏ (i : ι) in s, f i x)
theorem smooth_finset_sum {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [ G] [ G] {E' : Type u_5} [normed_group E'] [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {ι : Type u_8} {s : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i ssmooth I' I (f i)) :
smooth I' I (λ (x : M), ∑ (i : ι) in s, f i x)
theorem smooth_finprod {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [comm_monoid G] [ G] [ G] {E' : Type u_5} [normed_group E'] [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {ι : Type u_8} {f : ι → M → G} (h : ∀ (i : ι), smooth I' I (f i)) (hfin : locally_finite (λ (i : ι), function.mul_support (f i))) :
smooth I' I (λ (x : M), ∏ᶠ (i : ι), f i x)
theorem smooth_finsum {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [ G] [ G] {E' : Type u_5} [normed_group E'] [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {ι : Type u_8} {f : ι → M → G} (h : ∀ (i : ι), smooth I' I (f i)) (hfin : locally_finite (λ (i : ι), function.support (f i))) :
smooth I' I (λ (x : M), ∑ᶠ (i : ι), f i x)
theorem smooth_finsum_cond {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [ G] [ G] {E' : Type u_5} [normed_group E'] [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {ι : Type u_8} {f : ι → M → G} {p : ι → Prop} (hc : ∀ (i : ι), p ismooth I' I (f i)) (hf : locally_finite (λ (i : ι), function.support (f i))) :
smooth I' I (λ (x : M), ∑ᶠ (i : ι) (hi : p i), f i x)
theorem smooth_finprod_cond {𝕜 : Type u_1} {H : Type u_2} {E : Type u_3} [normed_group E] [ E] {I : H} {G : Type u_4} [comm_monoid G] [ G] [ G] {E' : Type u_5} [normed_group E'] [ E'] {H' : Type u_6} {I' : H'} {M : Type u_7} [ M] {ι : Type u_8} {f : ι → M → G} {p : ι → Prop} (hc : ∀ (i : ι), p ismooth I' I (f i)) (hf : locally_finite (λ (i : ι), function.mul_support (f i))) :
smooth I' I (λ (x : M), ∏ᶠ (i : ι) (hi : p i), f i x)