Algebraic structures over smooth functions #
In this file, we define instances of algebraic structures over smooth functions.
@[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] :
@[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⟯) :
@[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
@[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] :
@[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.
@[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] :
@[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
@[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' := _}
@[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] :
@[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 := npow smooth_map_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}
@[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] :
@[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 := 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 := _, gpow := div_inv_monoid.gpow._default monoid.mul smooth_map_group._proof_9 monoid.one smooth_map_group._proof_10 smooth_map_group._proof_11 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 := _}), gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, mul_left_inv := _}
@[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] :
@[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⟯) :
@[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] :
@[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 := _, gpow := group.gpow smooth_map_group, gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, mul_left_inv := _, mul_comm := _}
Ring stucture #
In this section we show that smooth functions valued in a smooth ring R inherit a ring structure
under pointwise multiplication.
@[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_semiring 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, mul_assoc := _, one := monoid.one smooth_map_monoid, one_mul := _, mul_one := _, npow := npow smooth_map_monoid, npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}
@[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 := _, gsmul := add_comm_group.gsmul smooth_map_add_comm_group, gsmul_zero' := _, gsmul_succ' := _, gsmul_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 := _}
@[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 := _, gsmul := add_comm_group.gsmul smooth_map_add_comm_group, gsmul_zero' := _, gsmul_succ' := _, gsmul_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 := _}
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.
@[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⟯) :
@[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 := _}
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_7}
[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' := _}
@[instance]
def
times_cont_mdiff_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_7}
[normed_ring A]
[normed_algebra 𝕜 A]
[smooth_ring 𝓘(𝕜, A) A] :
Equations
- times_cont_mdiff_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_12, commutes' := _, smul_def' := _}
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 𝕜.
@[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] :
@[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 := _}