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]
[smooth_manifold_with_corners I N]
{G : Type u_7}
[has_add G]
[topological_space G]
[has_continuous_add 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]
[smooth_manifold_with_corners I N]
{G : Type u_7}
[has_mul G]
[topological_space G]
[has_continuous_mul G]
[charted_space H' G]
[has_smooth_mul 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]
[smooth_manifold_with_corners I N]
{G : Type u_7}
[monoid G]
[topological_space G]
[charted_space H' G]
[smooth_manifold_with_corners I' 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]
[smooth_manifold_with_corners I N]
{G : Type u_7}
[add_monoid G]
[topological_space G]
[charted_space H' G]
[smooth_manifold_with_corners I' 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]
[smooth_manifold_with_corners I N]
{G : Type u_7}
[add_semigroup G]
[topological_space G]
[has_continuous_add 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]
[smooth_manifold_with_corners I N]
{G : Type u_7}
[semigroup G]
[topological_space G]
[has_continuous_mul 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]
[smooth_manifold_with_corners I N]
{G : Type u_7}
[monoid G]
[topological_space G]
[has_continuous_mul 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 := _}
@[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]
[smooth_manifold_with_corners I N]
{G : Type u_7}
[add_monoid G]
[topological_space G]
[has_continuous_add 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]
[smooth_manifold_with_corners I N]
{G : Type u_7}
[comm_monoid G]
[topological_space G]
[has_continuous_mul 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 := _, 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]
[smooth_manifold_with_corners I N]
{G : Type u_7}
[add_comm_monoid G]
[topological_space G]
[has_continuous_add 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]
[smooth_manifold_with_corners I N]
{G : Type u_7}
[group G]
[topological_space G]
[topological_group G]
[charted_space H' G]
[smooth_manifold_with_corners I' 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 := _, inv := λ (f : C^⊤⟮I, N; I', G⟯), {to_fun := λ (x : N), (⇑f x)⁻¹, times_cont_mdiff_to_fun := _}, div := div_inv_monoid.div._default monoid.mul smooth_map_group._proof_6 monoid.one smooth_map_group._proof_7 smooth_map_group._proof_8 (λ (f : C^⊤⟮I, N; I', G⟯), {to_fun := λ (x : N), (⇑f x)⁻¹, times_cont_mdiff_to_fun := _}), div_eq_mul_inv := _, 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]
[smooth_manifold_with_corners I N]
{G : Type u_7}
[add_group G]
[topological_space G]
[topological_add_group G]
[charted_space H' G]
[smooth_manifold_with_corners I' G]
[lie_add_group 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]
[smooth_manifold_with_corners I N]
{G : Type u_7}
[add_comm_group G]
[topological_space G]
[topological_add_group 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]
[smooth_manifold_with_corners I N]
{G : Type u_7}
[comm_group G]
[topological_space G]
[topological_group 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 := _, inv := group.inv smooth_map_group, div := group.div smooth_map_group, div_eq_mul_inv := _, 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]
[smooth_manifold_with_corners I N]
{R : Type u_7}
[semiring R]
[topological_space R]
[topological_semiring 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 := _, add_comm := _, mul := monoid.mul smooth_map_monoid, mul_assoc := _, one := monoid.one smooth_map_monoid, one_mul := _, mul_one := _, 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]
[smooth_manifold_with_corners I N]
{R : Type u_7}
[ring R]
[topological_space R]
[topological_ring 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 := _, neg := add_comm_group.neg smooth_map_add_comm_group, sub := add_comm_group.sub smooth_map_add_comm_group, sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := semiring.mul smooth_map_semiring, mul_assoc := _, one := semiring.one smooth_map_semiring, one_mul := _, mul_one := _, 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]
[smooth_manifold_with_corners I N]
{R : Type u_7}
[comm_ring R]
[topological_space R]
[topological_ring 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 := _, neg := add_comm_group.neg smooth_map_add_comm_group, sub := add_comm_group.sub smooth_map_add_comm_group, sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := semiring.mul smooth_map_semiring, mul_assoc := _, one := semiring.one smooth_map_semiring, one_mul := _, mul_one := _, 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]
[smooth_manifold_with_corners I N]
{V : Type u_3}
[normed_group V]
[normed_space 𝕜 V] :
@[instance]
def
smooth_map_semimodule
{𝕜 : 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]
[smooth_manifold_with_corners I N]
{V : Type u_3}
[normed_group V]
[normed_space 𝕜 V] :
Equations
- smooth_map_semimodule = semimodule.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]
[smooth_manifold_with_corners I 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]
[smooth_manifold_with_corners I 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_13, 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]
[smooth_manifold_with_corners I 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]
[smooth_manifold_with_corners I 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 := _}