mathlib3 documentation

geometry.manifold.algebra.smooth_functions

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] :
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) :
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''⟯.

Equations
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''⟯.

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

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

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
@[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

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.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''⟯.

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

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

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
@[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

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