Algebraic structures over smooth functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 ⊤), ⟨⇑f + ⇑g, _⟩}
@[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 ⊤), ⟨⇑f * ⇑g, _⟩}
@[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 fun_like.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
- smooth_map.coe_fn_add_monoid_hom = {to_fun := coe_fn fun_like.has_coe_to_fun, map_zero' := _, map_add' := _}
@[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 ᾰ
def
smooth_map.comp_left_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]
{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''}
{G' : Type u_9}
[add_monoid G']
[topological_space G']
[charted_space H' G']
[has_smooth_add I' G']
{G'' : Type u_10}
[add_monoid G'']
[topological_space G'']
[charted_space H'' G'']
[has_smooth_add I'' G'']
(φ : G' →+ G'')
(hφ : smooth I' I'' ⇑φ) :
cont_mdiff_map I I' N G' ⊤ →+ cont_mdiff_map I I'' N G'' ⊤
For a manifold N and a smooth homomorphism φ between additive Lie groups G',
G'', the 'left-composition-by-φ' group homomorphism from C^∞⟮I, N; I', G'⟯ to
C^∞⟮I, N; I'', G''⟯.
def
smooth_map.comp_left_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]
{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''}
{G' : Type u_9}
[monoid G']
[topological_space G']
[charted_space H' G']
[has_smooth_mul I' G']
{G'' : Type u_10}
[monoid G'']
[topological_space G'']
[charted_space H'' G'']
[has_smooth_mul I'' G'']
(φ : G' →* G'')
(hφ : smooth I' I'' ⇑φ) :
cont_mdiff_map I I' N G' ⊤ →* cont_mdiff_map I I'' N G'' ⊤
For a manifold N and a smooth homomorphism φ between Lie groups G', G'', the
'left-composition-by-φ' group homomorphism from C^∞⟮I, N; I', G'⟯ to C^∞⟮I, N; I'', G''⟯.
noncomputable
def
smooth_map.restrict_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]
{U V : topological_space.opens N}
(h : U ≤ V) :
cont_mdiff_map I I' ↥V G ⊤ →+ cont_mdiff_map I I' ↥U G ⊤
For an additive Lie group G and open sets U ⊆ V in N, the 'restriction' group
homomorphism from C^∞⟮I, V; I', G⟯ to C^∞⟮I, U; I', G⟯.
Equations
- smooth_map.restrict_add_monoid_hom I I' G h = {to_fun := λ (f : cont_mdiff_map I I' ↥V G ⊤), ⟨⇑f ∘ set.inclusion h, _⟩, map_zero' := _, map_add' := _}
noncomputable
def
smooth_map.restrict_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]
{U V : topological_space.opens N}
(h : U ≤ V) :
cont_mdiff_map I I' ↥V G ⊤ →* cont_mdiff_map I I' ↥U G ⊤
For a Lie group G and open sets U ⊆ V in N, the 'restriction' group homomorphism from
C^∞⟮I, V; I', G⟯ to C^∞⟮I, U; I', G⟯.
Equations
- smooth_map.restrict_monoid_hom I I' G h = {to_fun := λ (f : cont_mdiff_map I I' ↥V G ⊤), ⟨⇑f ∘ set.inclusion h, _⟩, map_one' := _, map_mul' := _}
@[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 ⊤), ⟨λ (x : N), -⇑f x, _⟩, sub := λ (f g : cont_mdiff_map I I' N G ⊤), ⟨⇑f - ⇑g, _⟩, 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 ⊤), ⟨λ (x : N), -⇑f x, _⟩), 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 ⊤), ⟨λ (x : N), (⇑f x)⁻¹, _⟩, div := λ (f g : cont_mdiff_map I I' N G ⊤), ⟨⇑f / ⇑g, _⟩, 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 ⊤), ⟨λ (x : N), (⇑f x)⁻¹, _⟩), 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.comp_left_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]
{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''}
{R' : Type u_9}
[ring R']
[topological_space R']
[charted_space H' R']
[smooth_ring I' R']
{R'' : Type u_10}
[ring R'']
[topological_space R'']
[charted_space H'' R'']
[smooth_ring I'' R'']
(φ : R' →+* R'')
(hφ : smooth I' I'' ⇑φ) :
cont_mdiff_map I I' N R' ⊤ →+* cont_mdiff_map I I'' N R'' ⊤
For a manifold N and a smooth homomorphism φ between smooth rings R', R'', the
'left-composition-by-φ' ring homomorphism from C^∞⟮I, N; I', R'⟯ to C^∞⟮I, N; I'', R''⟯.
noncomputable
def
smooth_map.restrict_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)
[ring R]
[topological_space R]
[charted_space H' R]
[smooth_ring I' R]
{U V : topological_space.opens N}
(h : U ≤ V) :
cont_mdiff_map I I' ↥V R ⊤ →+* cont_mdiff_map I I' ↥U R ⊤
For a "smooth ring" R and open sets U ⊆ V in N, the "restriction" ring homomorphism from
C^∞⟮I, V; I', R⟯ to C^∞⟮I, U; I', R⟯.
Equations
- smooth_map.restrict_ring_hom I I' R h = {to_fun := λ (f : cont_mdiff_map I I' ↥V R ⊤), ⟨⇑f ∘ set.inclusion h, _⟩, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
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 fun_like.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 ⊤), ⟨r • ⇑f, _⟩}
@[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_1 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 fun_like.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.
@[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 ⊤), ⟨r • ⇑f, _⟩}, 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 ⊤), ⟨λ (x : N), ⇑f x • ⇑g x, _⟩}
@[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 := _}