Algebraic structures over smooth functions #
In this file, we define instances of algebraic structures over smooth functions.
@[protected, instance]
def
smooth_map.has_add
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[has_add G]
[topological_space G]
[charted_space H' G]
[has_smooth_add I' G] :
@[protected, instance]
def
smooth_map.has_mul
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[has_mul G]
[topological_space G]
[charted_space H' G]
[has_smooth_mul I' G] :
@[simp]
theorem
smooth_map.coe_add
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[has_add G]
[topological_space G]
[charted_space H' G]
[has_smooth_add I' G]
(f g : C^⊤⟮I, N; I', G⟯) :
@[simp]
theorem
smooth_map.coe_mul
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[has_mul G]
[topological_space G]
[charted_space H' G]
[has_smooth_mul I' G]
(f g : C^⊤⟮I, N; I', G⟯) :
@[simp]
theorem
smooth_map.add_comp
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{E'' : Type u_7}
[normed_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_8}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{N' : Type u_9}
[topological_space N']
[charted_space H'' N']
{G : Type u_10}
[has_add G]
[topological_space G]
[charted_space H' G]
[has_smooth_add I' G]
(f g : C^⊤⟮I'', N'; I', G⟯)
(h : C^⊤⟮I, N; I'', N'⟯) :
@[simp]
theorem
smooth_map.mul_comp
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{E'' : Type u_7}
[normed_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_8}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{N' : Type u_9}
[topological_space N']
[charted_space H'' N']
{G : Type u_10}
[has_mul G]
[topological_space G]
[charted_space H' G]
[has_smooth_mul I' G]
(f g : C^⊤⟮I'', N'; I', G⟯)
(h : C^⊤⟮I, N; I'', N'⟯) :
@[protected, instance]
def
smooth_map.has_one
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[monoid G]
[topological_space G]
[charted_space H' G] :
Equations
@[protected, instance]
def
smooth_map.has_zero
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[add_monoid G]
[topological_space G]
[charted_space H' G] :
Equations
@[simp]
theorem
smooth_map.coe_zero
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[add_monoid G]
[topological_space G]
[charted_space H' G] :
@[simp]
theorem
smooth_map.coe_one
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[monoid G]
[topological_space G]
[charted_space H' G] :
Group structure #
In this section we show that smooth functions valued in a Lie group inherit a group structure under pointwise multiplication.
@[protected, instance]
def
smooth_map.add_semigroup
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[add_semigroup G]
[topological_space G]
[charted_space H' G]
[has_smooth_add I' G] :
Equations
@[protected, instance]
def
smooth_map.semigroup
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[semigroup G]
[topological_space G]
[charted_space H' G]
[has_smooth_mul I' G] :
Equations
@[protected, instance]
def
smooth_map.add_monoid
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[add_monoid G]
[topological_space G]
[charted_space H' G]
[has_smooth_add I' G] :
Equations
- smooth_map.add_monoid = {add := add_semigroup.add smooth_map.add_semigroup, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := nsmul_rec (add_zero_class.to_has_add C^⊤⟮I, N; I', G⟯), nsmul_zero' := _, nsmul_succ' := _}
@[protected, instance]
def
smooth_map.monoid
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[monoid G]
[topological_space G]
[charted_space H' G]
[has_smooth_mul I' G] :
Equations
- smooth_map.monoid = {mul := semigroup.mul smooth_map.semigroup, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul C^⊤⟮I, N; I', G⟯), npow_zero' := _, npow_succ' := _}
def
smooth_map.coe_fn_monoid_hom
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[monoid G]
[topological_space G]
[charted_space H' G]
[has_smooth_mul I' G] :
Coercion to a function as an monoid_hom. Similar to monoid_hom.coe_fn.
Equations
def
smooth_map.coe_fn_add_monoid_hom
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[add_monoid G]
[topological_space G]
[charted_space H' G]
[has_smooth_add I' G] :
Coercion to a function as an add_monoid_hom. Similar to add_monoid_hom.coe_fn.
Equations
@[simp]
theorem
smooth_map.coe_fn_monoid_hom_apply
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[monoid G]
[topological_space G]
[charted_space H' G]
[has_smooth_mul I' G]
(x : C^⊤⟮I, N; I', G⟯)
(ᾰ : N) :
⇑smooth_map.coe_fn_monoid_hom x ᾰ = ⇑x ᾰ
@[simp]
theorem
smooth_map.coe_fn_add_monoid_hom_apply
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[add_monoid G]
[topological_space G]
[charted_space H' G]
[has_smooth_add I' G]
(x : C^⊤⟮I, N; I', G⟯)
(ᾰ : N) :
⇑smooth_map.coe_fn_add_monoid_hom x ᾰ = ⇑x ᾰ
@[protected, instance]
def
smooth_map.add_comm_monoid
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[add_comm_monoid G]
[topological_space G]
[charted_space H' G]
[has_smooth_add I' G] :
Equations
- smooth_map.add_comm_monoid = {add := add_monoid.add smooth_map.add_monoid, add_assoc := _, zero := add_monoid.zero smooth_map.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul smooth_map.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[protected, instance]
def
smooth_map.comm_monoid
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[comm_monoid G]
[topological_space G]
[charted_space H' G]
[has_smooth_mul I' G] :
Equations
- smooth_map.comm_monoid = {mul := monoid.mul smooth_map.monoid, mul_assoc := _, one := monoid.one smooth_map.monoid, one_mul := _, mul_one := _, npow := monoid.npow smooth_map.monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}
@[protected, instance]
def
smooth_map.add_group
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[add_group G]
[topological_space G]
[charted_space H' G]
[lie_add_group I' G] :
Equations
- smooth_map.add_group = {add := add_monoid.add smooth_map.add_monoid, add_assoc := _, zero := add_monoid.zero smooth_map.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul smooth_map.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := λ (f : C^⊤⟮I, N; I', G⟯), {to_fun := λ (x : N), -⇑f x, times_cont_mdiff_to_fun := _}, sub := λ (f g : C^⊤⟮I, N; I', G⟯), {to_fun := ⇑f - ⇑g, times_cont_mdiff_to_fun := _}, sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul._default add_monoid.add smooth_map.add_group._proof_9 add_monoid.zero smooth_map.add_group._proof_10 smooth_map.add_group._proof_11 add_monoid.nsmul smooth_map.add_group._proof_12 smooth_map.add_group._proof_13 (λ (f : C^⊤⟮I, N; I', G⟯), {to_fun := λ (x : N), -⇑f x, times_cont_mdiff_to_fun := _}), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _}
@[protected, instance]
def
smooth_map.group
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[group G]
[topological_space G]
[charted_space H' G]
[lie_group I' G] :
Equations
- smooth_map.group = {mul := monoid.mul smooth_map.monoid, mul_assoc := _, one := monoid.one smooth_map.monoid, one_mul := _, mul_one := _, npow := monoid.npow smooth_map.monoid, npow_zero' := _, npow_succ' := _, inv := λ (f : C^⊤⟮I, N; I', G⟯), {to_fun := λ (x : N), (⇑f x)⁻¹, times_cont_mdiff_to_fun := _}, div := λ (f g : C^⊤⟮I, N; I', G⟯), {to_fun := ⇑f / ⇑g, times_cont_mdiff_to_fun := _}, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default monoid.mul smooth_map.group._proof_9 monoid.one smooth_map.group._proof_10 smooth_map.group._proof_11 monoid.npow smooth_map.group._proof_12 smooth_map.group._proof_13 (λ (f : C^⊤⟮I, N; I', G⟯), {to_fun := λ (x : N), (⇑f x)⁻¹, times_cont_mdiff_to_fun := _}), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
@[simp]
theorem
smooth_map.coe_inv
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[group G]
[topological_space G]
[charted_space H' G]
[lie_group I' G]
(f : C^⊤⟮I, N; I', G⟯) :
@[simp]
theorem
smooth_map.coe_neg
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[add_group G]
[topological_space G]
[charted_space H' G]
[lie_add_group I' G]
(f : C^⊤⟮I, N; I', G⟯) :
@[simp]
theorem
smooth_map.coe_div
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[group G]
[topological_space G]
[charted_space H' G]
[lie_group I' G]
(f g : C^⊤⟮I, N; I', G⟯) :
@[simp]
theorem
smooth_map.coe_sub
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[add_group G]
[topological_space G]
[charted_space H' G]
[lie_add_group I' G]
(f g : C^⊤⟮I, N; I', G⟯) :
@[protected, instance]
def
smooth_map.comm_group
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[comm_group G]
[topological_space G]
[charted_space H' G]
[lie_group I' G] :
Equations
- smooth_map.comm_group = {mul := group.mul smooth_map.group, mul_assoc := _, one := group.one smooth_map.group, one_mul := _, mul_one := _, npow := group.npow smooth_map.group, npow_zero' := _, npow_succ' := _, inv := group.inv smooth_map.group, div := group.div smooth_map.group, div_eq_mul_inv := _, zpow := group.zpow smooth_map.group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}
@[protected, instance]
def
smooth_map.add_comm_group
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{G : Type u_7}
[add_comm_group G]
[topological_space G]
[charted_space H' G]
[lie_add_group I' G] :
Equations
- smooth_map.add_comm_group = {add := add_group.add smooth_map.add_group, add_assoc := _, zero := add_group.zero smooth_map.add_group, zero_add := _, add_zero := _, nsmul := add_group.nsmul smooth_map.add_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg smooth_map.add_group, sub := add_group.sub smooth_map.add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul smooth_map.add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
Ring stucture #
In this section we show that smooth functions valued in a smooth ring R inherit a ring structure
under pointwise multiplication.
@[protected, instance]
def
smooth_map.semiring
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{R : Type u_7}
[semiring R]
[topological_space R]
[charted_space H' R]
[smooth_ring I' R] :
Equations
- smooth_map.semiring = {add := add_comm_monoid.add smooth_map.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero smooth_map.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul smooth_map.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := monoid.mul smooth_map.monoid, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := monoid.one smooth_map.monoid, one_mul := _, mul_one := _, npow := monoid.npow smooth_map.monoid, npow_zero' := _, npow_succ' := _}
@[protected, instance]
def
smooth_map.ring
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{R : Type u_7}
[ring R]
[topological_space R]
[charted_space H' R]
[smooth_ring I' R] :
Equations
- smooth_map.ring = {add := semiring.add smooth_map.semiring, add_assoc := _, zero := semiring.zero smooth_map.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul smooth_map.semiring, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg smooth_map.add_comm_group, sub := add_comm_group.sub smooth_map.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul smooth_map.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := semiring.mul smooth_map.semiring, mul_assoc := _, one := semiring.one smooth_map.semiring, one_mul := _, mul_one := _, npow := semiring.npow smooth_map.semiring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
@[protected, instance]
def
smooth_map.comm_ring
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{R : Type u_7}
[comm_ring R]
[topological_space R]
[charted_space H' R]
[smooth_ring I' R] :
Equations
- smooth_map.comm_ring = {add := semiring.add smooth_map.semiring, add_assoc := _, zero := semiring.zero smooth_map.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul smooth_map.semiring, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg smooth_map.add_comm_group, sub := add_comm_group.sub smooth_map.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul smooth_map.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := semiring.mul smooth_map.semiring, mul_assoc := _, one := semiring.one smooth_map.semiring, one_mul := _, mul_one := _, npow := semiring.npow smooth_map.semiring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
def
smooth_map.coe_fn_ring_hom
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{R : Type u_7}
[comm_ring R]
[topological_space R]
[charted_space H' R]
[smooth_ring I' R] :
Coercion to a function as a ring_hom.
Equations
- smooth_map.coe_fn_ring_hom = {to_fun := coe_fn times_cont_mdiff_map.has_coe_to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
theorem
smooth_map.coe_fn_ring_hom_apply
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{R : Type u_7}
[comm_ring R]
[topological_space R]
[charted_space H' R]
[smooth_ring I' R]
(x : C^⊤⟮I, N; I', R⟯)
(ᾰ : N) :
⇑smooth_map.coe_fn_ring_hom x ᾰ = ⇑x ᾰ
def
smooth_map.eval_ring_hom
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{H' : Type u_5}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{R : Type u_7}
[comm_ring R]
[topological_space R]
[charted_space H' R]
[smooth_ring I' R]
(n : N) :
function.eval as a ring_hom on the ring of smooth functions.
Equations
- smooth_map.eval_ring_hom n = (pi.eval_ring_hom (λ (ᾰ : N), R) n).comp smooth_map.coe_fn_ring_hom
Semiodule stucture #
In this section we show that smooth functions valued in a vector space M over a normed
field 𝕜 inherit a vector space structure.
@[protected, instance]
def
smooth_map.has_scalar
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{V : Type u_3}
[normed_group V]
[normed_space 𝕜 V] :
@[simp]
theorem
smooth_map.coe_smul
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{V : Type u_3}
[normed_group V]
[normed_space 𝕜 V]
(r : 𝕜)
(f : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯) :
@[simp]
theorem
smooth_map.smul_comp
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{E'' : Type u_7}
[normed_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_8}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{N' : Type u_9}
[topological_space N']
[charted_space H'' N']
{V : Type u_3}
[normed_group V]
[normed_space 𝕜 V]
(r : 𝕜)
(g : C^⊤⟮I'', N'; 𝓘(𝕜, V), V⟯)
(h : C^⊤⟮I, N; I'', N'⟯) :
@[protected, instance]
def
smooth_map.module
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{V : Type u_3}
[normed_group V]
[normed_space 𝕜 V] :
Equations
- smooth_map.module = module.of_core {to_has_scalar := {smul := has_scalar.smul smooth_map.has_scalar}, smul_add := _, add_smul := _, mul_smul := _, one_smul := _}
def
smooth_map.coe_fn_linear_map
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{V : Type u_3}
[normed_group V]
[normed_space 𝕜 V] :
Coercion to a function as a linear_map.
Equations
@[simp]
theorem
smooth_map.coe_fn_linear_map_apply
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{V : Type u_3}
[normed_group V]
[normed_space 𝕜 V]
(x : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯)
(ᾰ : N) :
⇑smooth_map.coe_fn_linear_map x ᾰ = ⇑x ᾰ
Algebra structure #
In this section we show that smooth functions valued in a normed algebra A over a normed field 𝕜
inherit an algebra structure.
def
smooth_map.C
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{A : Type u_10}
[normed_ring A]
[normed_algebra 𝕜 A]
[smooth_ring 𝓘(𝕜, A) A] :
Smooth constant functions as a ring_hom.
Equations
- smooth_map.C = {to_fun := λ (c : 𝕜), {to_fun := λ (x : N), ⇑(algebra_map 𝕜 A) c, times_cont_mdiff_to_fun := _}, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[protected, instance]
def
smooth_map.algebra
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{A : Type u_10}
[normed_ring A]
[normed_algebra 𝕜 A]
[smooth_ring 𝓘(𝕜, A) A] :
Equations
- smooth_map.algebra = {to_has_scalar := {smul := λ (r : 𝕜) (f : C^⊤⟮I, N; 𝓘(𝕜, A), A⟯), {to_fun := r • ⇑f, times_cont_mdiff_to_fun := _}}, to_ring_hom := smooth_map.C _inst_17, commutes' := _, smul_def' := _}
@[protected, instance]
def
function.algebra
(I : Type u_1)
{R : Type u_2}
(A : Type u_3)
{r : comm_semiring R}
[semiring A]
[algebra R A] :
algebra R (I → A)
A special case of pi.algebra for non-dependent types. Lean get stuck on the definition
below without this.
Equations
- function.algebra I A = pi.algebra I (λ (ᾰ : I), A)
def
smooth_map.coe_fn_alg_hom
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{A : Type u_10}
[normed_ring A]
[normed_algebra 𝕜 A]
[smooth_ring 𝓘(𝕜, A) A] :
Coercion to a function as an alg_hom.
@[simp]
theorem
smooth_map.coe_fn_alg_hom_apply
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{A : Type u_10}
[normed_ring A]
[normed_algebra 𝕜 A]
[smooth_ring 𝓘(𝕜, A) A]
(x : C^⊤⟮I, N; 𝓘(𝕜, A), A⟯)
(ᾰ : N) :
⇑smooth_map.coe_fn_alg_hom x ᾰ = ⇑x ᾰ
Structure as module over scalar functions #
If V is a module over 𝕜, then we show that the space of smooth functions from N to V
is naturally a vector space over the ring of smooth functions from N to 𝕜.
@[protected, instance]
def
smooth_map.has_scalar'
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{V : Type u_3}
[normed_group V]
[normed_space 𝕜 V] :
@[simp]
theorem
smooth_map.smul_comp'
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{E'' : Type u_7}
[normed_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_8}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{N' : Type u_9}
[topological_space N']
[charted_space H'' N']
{V : Type u_3}
[normed_group V]
[normed_space 𝕜 V]
(f : C^⊤⟮I'', N'; 𝓘(𝕜, 𝕜), 𝕜⟯)
(g : C^⊤⟮I'', N'; 𝓘(𝕜, V), V⟯)
(h : C^⊤⟮I, N; I'', N'⟯) :
@[protected, instance]
def
smooth_map.module'
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{N : Type u_6}
[topological_space N]
[charted_space H N]
{V : Type u_3}
[normed_group V]
[normed_space 𝕜 V] :
Equations
- smooth_map.module' = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := has_scalar.smul smooth_map.has_scalar'}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}