mathlib documentation

geometry.manifold.algebra.smooth_functions

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] :
Equations
@[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] :
Equations
@[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 ) :
(f + g) = f + 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 ) :
(f * g) = f * 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' ) :
(f + g).comp h = f.comp h + g.comp h
@[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' ) :
(f * g).comp h = f.comp h * g.comp h
@[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] :
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] :
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] :
0 = 0
@[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] :
1 = 1

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] :
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] :
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] :
Equations
@[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] :
Equations
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
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) :
@[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) :
@[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] :
Equations
@[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] :
Equations
@[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] :
Equations
@[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] :
Equations
@[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 ) :
(f / g) = f / 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 ) :
(f - g) = f - 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] :
Equations

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] :
Equations
@[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] :
Equations
@[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] :
Equations
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
@[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) :
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) :

function.eval as a ring_hom on the ring of smooth functions.

Equations

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] :
Equations
@[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 ) :
(r f) = r f
@[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' ) :
(r g).comp h = r g.comp h
@[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] :
Equations
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] :

Coercion to a function as a linear_map.

Equations
@[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) :

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] :

Smooth constant functions as a ring_hom.

Equations
@[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] :
Equations
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] :

Coercion to a function as an alg_hom.

Equations
@[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) :

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] :
Equations
@[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' ) :
(f g).comp h = f.comp h g.comp h
@[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] :
Equations