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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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] :
has_add (cont_mdiff_map I I' N G ⊤)
Equations
- smooth_map.has_add = {add := λ (f g : cont_mdiff_map I I' N G ⊤), {to_fun := ⇑f + ⇑g, cont_mdiff_to_fun := _}}
@[protected, instance]
def
smooth_map.has_mul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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] :
has_mul (cont_mdiff_map I I' N G ⊤)
Equations
- smooth_map.has_mul = {mul := λ (f g : cont_mdiff_map I I' N G ⊤), {to_fun := ⇑f * ⇑g, cont_mdiff_to_fun := _}}
@[simp]
theorem
smooth_map.coe_add
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : cont_mdiff_map I I' N G ⊤) :
@[simp]
theorem
smooth_map.coe_mul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : cont_mdiff_map I I' N G ⊤) :
@[simp]
theorem
smooth_map.add_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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_add_comm_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 : cont_mdiff_map I'' I' N' G ⊤)
(h : cont_mdiff_map I I'' N N' ⊤) :
@[simp]
theorem
smooth_map.mul_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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_add_comm_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 : cont_mdiff_map I'' I' N' G ⊤)
(h : cont_mdiff_map I I'' N N' ⊤) :
@[protected, instance]
def
smooth_map.has_one
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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_one (cont_mdiff_map I I' N G ⊤)
Equations
@[protected, instance]
def
smooth_map.has_zero
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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_zero (cont_mdiff_map I I' N G ⊤)
Equations
@[simp]
theorem
smooth_map.coe_zero
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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] :
add_semigroup (cont_mdiff_map I I' N G ⊤)
Equations
@[protected, instance]
def
smooth_map.semigroup
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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] :
semigroup (cont_mdiff_map I I' N G ⊤)
Equations
@[protected, instance]
def
smooth_map.add_monoid
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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] :
add_monoid (cont_mdiff_map I I' N 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 (cont_mdiff_map I I' N G ⊤)), nsmul_zero' := _, nsmul_succ' := _}
@[protected, instance]
def
smooth_map.monoid
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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] :
monoid (cont_mdiff_map I I' N 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 (cont_mdiff_map I I' N G ⊤)), npow_zero' := _, npow_succ' := _}
def
smooth_map.coe_fn_monoid_hom
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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] :
cont_mdiff_map I I' N G ⊤ →* N → G
Coercion to a function as an monoid_hom. Similar to monoid_hom.coe_fn.
Equations
- smooth_map.coe_fn_monoid_hom = {to_fun := coe_fn cont_mdiff_map.has_coe_to_fun, map_one' := _, map_mul' := _}
def
smooth_map.coe_fn_add_monoid_hom
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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] :
cont_mdiff_map I I' N G ⊤ →+ N → 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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : cont_mdiff_map I I' N G ⊤)
(ᾰ : N) :
⇑smooth_map.coe_fn_monoid_hom x ᾰ = ⇑x ᾰ
@[simp]
theorem
smooth_map.coe_fn_add_monoid_hom_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : cont_mdiff_map I I' N G ⊤)
(ᾰ : N) :
⇑smooth_map.coe_fn_add_monoid_hom x ᾰ = ⇑x ᾰ
@[protected, instance]
def
smooth_map.add_comm_monoid
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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] :
add_comm_monoid (cont_mdiff_map I I' N 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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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] :
comm_monoid (cont_mdiff_map I I' N 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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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] :
add_group (cont_mdiff_map I I' N 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 : cont_mdiff_map I I' N G ⊤), {to_fun := λ (x : N), -⇑f x, cont_mdiff_to_fun := _}, sub := λ (f g : cont_mdiff_map I I' N G ⊤), {to_fun := ⇑f - ⇑g, 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 : cont_mdiff_map I I' N G ⊤), {to_fun := λ (x : N), -⇑f x, cont_mdiff_to_fun := _}), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _}
@[protected, instance]
def
smooth_map.group
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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] :
group (cont_mdiff_map I I' N 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 : cont_mdiff_map I I' N G ⊤), {to_fun := λ (x : N), (⇑f x)⁻¹, cont_mdiff_to_fun := _}, div := λ (f g : cont_mdiff_map I I' N G ⊤), {to_fun := ⇑f / ⇑g, 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 : cont_mdiff_map I I' N G ⊤), {to_fun := λ (x : N), (⇑f x)⁻¹, cont_mdiff_to_fun := _}), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
@[simp]
theorem
smooth_map.coe_inv
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : cont_mdiff_map I I' N G ⊤) :
@[simp]
theorem
smooth_map.coe_neg
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : cont_mdiff_map I I' N G ⊤) :
@[simp]
theorem
smooth_map.coe_div
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : cont_mdiff_map I I' N G ⊤) :
@[simp]
theorem
smooth_map.coe_sub
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : cont_mdiff_map I I' N G ⊤) :
@[protected, instance]
def
smooth_map.comm_group
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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] :
comm_group (cont_mdiff_map I I' N 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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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] :
add_comm_group (cont_mdiff_map I I' N 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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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] :
semiring (cont_mdiff_map I I' N 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 := _, nat_cast := non_assoc_semiring.nat_cast._default monoid.one add_comm_monoid.add smooth_map.semiring._proof_14 add_comm_monoid.zero smooth_map.semiring._proof_15 smooth_map.semiring._proof_16 add_comm_monoid.nsmul smooth_map.semiring._proof_17 smooth_map.semiring._proof_18, nat_cast_zero := _, nat_cast_succ := _, npow := monoid.npow smooth_map.monoid, npow_zero' := _, npow_succ' := _}
@[protected, instance]
def
smooth_map.ring
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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] :
ring (cont_mdiff_map I I' N 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 := _, int_cast := add_comm_group_with_one.int_cast._default semiring.nat_cast semiring.add smooth_map.ring._proof_12 semiring.zero smooth_map.ring._proof_13 smooth_map.ring._proof_14 semiring.nsmul smooth_map.ring._proof_15 smooth_map.ring._proof_16 semiring.one smooth_map.ring._proof_17 smooth_map.ring._proof_18 add_comm_group.neg add_comm_group.sub smooth_map.ring._proof_19 add_comm_group.zsmul smooth_map.ring._proof_20 smooth_map.ring._proof_21 smooth_map.ring._proof_22 smooth_map.ring._proof_23, nat_cast := semiring.nat_cast smooth_map.semiring, one := semiring.one smooth_map.semiring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := semiring.mul smooth_map.semiring, mul_assoc := _, 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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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] :
comm_ring (cont_mdiff_map I I' N 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 := _, int_cast := ring.int_cast._default semiring.nat_cast semiring.add smooth_map.comm_ring._proof_13 semiring.zero smooth_map.comm_ring._proof_14 smooth_map.comm_ring._proof_15 semiring.nsmul smooth_map.comm_ring._proof_16 smooth_map.comm_ring._proof_17 semiring.one smooth_map.comm_ring._proof_18 smooth_map.comm_ring._proof_19 add_comm_group.neg add_comm_group.sub smooth_map.comm_ring._proof_20 add_comm_group.zsmul smooth_map.comm_ring._proof_21 smooth_map.comm_ring._proof_22 smooth_map.comm_ring._proof_23 smooth_map.comm_ring._proof_24, nat_cast := semiring.nat_cast smooth_map.semiring, one := semiring.one smooth_map.semiring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := semiring.mul smooth_map.semiring, mul_assoc := _, 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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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] :
cont_mdiff_map I I' N R ⊤ →+* N → R
Coercion to a function as a ring_hom.
Equations
- smooth_map.coe_fn_ring_hom = {to_fun := coe_fn 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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : cont_mdiff_map I I' N R ⊤)
(ᾰ : N) :
⇑smooth_map.coe_fn_ring_hom x ᾰ = ⇑x ᾰ
def
smooth_map.eval_ring_hom
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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) :
cont_mdiff_map I I' N R ⊤ →+* R
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_smul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_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_add_comm_group V]
[normed_space 𝕜 V] :
has_smul 𝕜 (cont_mdiff_map I (model_with_corners_self 𝕜 V) N V ⊤)
Equations
- smooth_map.has_smul = {smul := λ (r : 𝕜) (f : cont_mdiff_map I (model_with_corners_self 𝕜 V) N V ⊤), {to_fun := r • ⇑f, cont_mdiff_to_fun := _}}
@[simp]
theorem
smooth_map.coe_smul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_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_add_comm_group V]
[normed_space 𝕜 V]
(r : 𝕜)
(f : cont_mdiff_map I (model_with_corners_self 𝕜 V) N V ⊤) :
@[simp]
theorem
smooth_map.smul_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_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_add_comm_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_add_comm_group V]
[normed_space 𝕜 V]
(r : 𝕜)
(g : cont_mdiff_map I'' (model_with_corners_self 𝕜 V) N' V ⊤)
(h : cont_mdiff_map I I'' N N' ⊤) :
@[protected, instance]
def
smooth_map.module
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_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_add_comm_group V]
[normed_space 𝕜 V] :
module 𝕜 (cont_mdiff_map I (model_with_corners_self 𝕜 V) N V ⊤)
Equations
- smooth_map.module = function.injective.module 𝕜 smooth_map.coe_fn_add_monoid_hom smooth_map.module._proof_4 smooth_map.coe_smul
def
smooth_map.coe_fn_linear_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_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_add_comm_group V]
[normed_space 𝕜 V] :
cont_mdiff_map I (model_with_corners_self 𝕜 V) N V ⊤ →ₗ[𝕜] N → V
Coercion to a function as a linear_map.
Equations
- smooth_map.coe_fn_linear_map = {to_fun := coe_fn cont_mdiff_map.has_coe_to_fun, map_add' := _, map_smul' := _}
@[simp]
theorem
smooth_map.coe_fn_linear_map_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_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_add_comm_group V]
[normed_space 𝕜 V]
(x : cont_mdiff_map I (model_with_corners_self 𝕜 V) N 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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_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 (model_with_corners_self 𝕜 A) A] :
𝕜 →+* cont_mdiff_map I (model_with_corners_self 𝕜 A) N A ⊤
Smooth constant functions as a ring_hom.
Equations
- smooth_map.C = {to_fun := λ (c : 𝕜), {to_fun := λ (x : N), ⇑(algebra_map 𝕜 A) c, cont_mdiff_to_fun := _}, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[protected, instance]
def
smooth_map.algebra
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_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 (model_with_corners_self 𝕜 A) A] :
algebra 𝕜 (cont_mdiff_map I (model_with_corners_self 𝕜 A) N A ⊤)
Equations
- smooth_map.algebra = {to_has_smul := {smul := λ (r : 𝕜) (f : cont_mdiff_map I (model_with_corners_self 𝕜 A) N A ⊤), {to_fun := r • ⇑f, cont_mdiff_to_fun := _}}, to_ring_hom := smooth_map.C _inst_17, commutes' := _, smul_def' := _}
def
smooth_map.coe_fn_alg_hom
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_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 (model_with_corners_self 𝕜 A) A] :
cont_mdiff_map I (model_with_corners_self 𝕜 A) N A ⊤ →ₐ[𝕜] N → A
Coercion to a function as an alg_hom.
@[simp]
theorem
smooth_map.coe_fn_alg_hom_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_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 (model_with_corners_self 𝕜 A) A]
(x : cont_mdiff_map I (model_with_corners_self 𝕜 A) N 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_smul'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_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_add_comm_group V]
[normed_space 𝕜 V] :
has_smul (cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) N 𝕜 ⊤) (cont_mdiff_map I (model_with_corners_self 𝕜 V) N V ⊤)
Equations
- smooth_map.has_smul' = {smul := λ (f : cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) N 𝕜 ⊤) (g : cont_mdiff_map I (model_with_corners_self 𝕜 V) N V ⊤), {to_fun := λ (x : N), ⇑f x • ⇑g x, cont_mdiff_to_fun := _}}
@[simp]
theorem
smooth_map.smul_comp'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_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_add_comm_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_add_comm_group V]
[normed_space 𝕜 V]
(f : cont_mdiff_map I'' (model_with_corners_self 𝕜 𝕜) N' 𝕜 ⊤)
(g : cont_mdiff_map I'' (model_with_corners_self 𝕜 V) N' V ⊤)
(h : cont_mdiff_map I I'' N N' ⊤) :
@[protected, instance]
def
smooth_map.module'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_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_add_comm_group V]
[normed_space 𝕜 V] :
module (cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) N 𝕜 ⊤) (cont_mdiff_map I (model_with_corners_self 𝕜 V) N V ⊤)
Equations
- smooth_map.module' = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := has_smul.smul smooth_map.has_smul'}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}