Algebraic structures over smooth functions #
In this file, we define instances of algebraic structures over smooth functions.
Equations
Group structure #
In this section we show that smooth functions valued in a Lie group inherit a group structure under pointwise multiplication.
Equations
Equations
- smooth_map_monoid = {mul := semigroup.mul smooth_map_semigroup, mul_assoc := _, one := 1, one_mul := _, mul_one := _}
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 := _}
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 := _}
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.
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 := _}
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 := _}
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.
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.
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' := _}
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 𝕜
.
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 := _}