Algebraic operations on smooth maps

This file complements Mathlib's algebraic structures on spaces of smooth maps with the pointwise evaluation of finite sums, with the iterated derivatives of a difference of C^n maps between normed spaces, with the pullback of smooth functions along a smooth map, and with the transport of pointwise identities between scalar-valued smooth functions to identities in the algebra of smooth functions. It also bundles the coordinate functions of a basis of a finite-dimensional space as smooth functions.

Main definitions

• Module.Basis.smoothCoord: the i-th coordinate function of a basis, as a smooth function.

Main results

• ContMDiffMap.coe_sum: the coercion of a finite sum of smooth maps is the sum of the coercions.
• ContMDiffMap.algebraMap_apply: the scalars of the algebra of C^n functions are the constant functions.
• ContMDiffMap.iteratedFDeriv_sub_apply: the iterated derivatives of order at most n of a difference of C^n maps are the differences of their iterated derivatives.
• ContMDiffMap.compRightAlgHom: precomposition with a smooth map φ : N → M, as an algebra homomorphism C^n⟮I, M; 𝓘(𝕜, A), A⟯ →ₐ[𝕜] C^n⟮J, N; 𝓘(𝕜, A), A⟯.
• ContMDiffMap.evalAlgHom: evaluation at a point, as an algebra homomorphism C^n⟮I, M; 𝓘(𝕜, A), A⟯ →ₐ[𝕜] A.
• ContMDiffMap.eq_zero_of_forall_mem_ker_evalAlgHom_smul_top: the points of M separate the scalar C^n functions.
• Diffeomorph.compRightAlgEquiv: precomposition with a diffeomorphism, as an algebra isomorphism.
• TauCeti.sub_algebraMap_eq_sum_mul_sub_algebraMap: the bundled form of a pointwise factorization of g - g x in the algebra of smooth functions.

@[simp]

theorem ContMDiffMap.coe_sum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {N : Type u_4} [TopologicalSpace N] [ChartedSpace H N] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {n : WithTop ℕ∞} {G : Type u_7} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H' G] [ContMDiffAdd I' n G] {ι : Type u_8} (s : Finset ι) (f : ι → ContMDiffMap I I' N G n) : ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)

The coercion of a finite sum of smooth maps into a commutative additive Lie group is the pointwise sum.

@[simp]

theorem ContMDiffMap.algebraMap_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {N : Type u_4} [TopologicalSpace N] [ChartedSpace H N] {n : WithTop ℕ∞} {A : Type u_5} [NormedRing A] [NormedAlgebra 𝕜 A] [ContMDiffRing (modelWithCornersSelf 𝕜 A) n A] (c : 𝕜) (x : N) : ((algebraMap 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 A) N A n)) c) x = (algebraMap 𝕜 A) c

The image of a scalar c in the algebra of C^n functions is the constant function with value algebraMap 𝕜 A c.

theorem ContMDiffMap.iteratedFDeriv_sub_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} (u v : ContMDiffMap (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n) {i : ℕ} (hi : ↑i ≤ n) (z : E) : iteratedFDeriv 𝕜 i (⇑(u - v)) z = iteratedFDeriv 𝕜 i (⇑u) z - iteratedFDeriv 𝕜 i (⇑v) z

The iterated derivatives of order at most n of a difference of C^n maps between normed spaces are the differences of their iterated derivatives.

def ContMDiffMap.compRightAlgHom (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} (A : Type u_11) [NormedRing A] [NormedAlgebra 𝕜 A] [ContMDiffRing (modelWithCornersSelf 𝕜 A) n A] (φ : ContMDiffMap J I N M n) : ContMDiffMap I (modelWithCornersSelf 𝕜 A) M A n →ₐ[𝕜] ContMDiffMap J (modelWithCornersSelf 𝕜 A) N A n

Precomposition with a C^n map φ : N → M, as an algebra homomorphism from the C^n functions on M to the C^n functions on N: the pullback f ↦ f ∘ φ of functions along φ. This is the smooth analogue of ContinuousMap.compRightAlgHom.

@[simp]

theorem ContMDiffMap.compRightAlgHom_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} (A : Type u_11) [NormedRing A] [NormedAlgebra 𝕜 A] [ContMDiffRing (modelWithCornersSelf 𝕜 A) n A] (φ : ContMDiffMap J I N M n) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 A) M A n) : (compRightAlgHom 𝕜 A φ) f = f.comp φ

@[simp]

theorem ContMDiffMap.compRightAlgHom_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (A : Type u_11) [NormedRing A] [NormedAlgebra 𝕜 A] [ContMDiffRing (modelWithCornersSelf 𝕜 A) n A] : compRightAlgHom 𝕜 A id = AlgHom.id 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 A) M A n)

theorem ContMDiffMap.compRightAlgHom_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {E'' : Type u_8} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H'' : Type u_9} [TopologicalSpace H''] {K : ModelWithCorners 𝕜 E'' H''} {P : Type u_10} [TopologicalSpace P] [ChartedSpace H'' P] {n : WithTop ℕ∞} (A : Type u_11) [NormedRing A] [NormedAlgebra 𝕜 A] [ContMDiffRing (modelWithCornersSelf 𝕜 A) n A] (φ : ContMDiffMap J I N M n) (ψ : ContMDiffMap K J P N n) : compRightAlgHom 𝕜 A (φ.comp ψ) = (compRightAlgHom 𝕜 A ψ).comp (compRightAlgHom 𝕜 A φ)

def ContMDiffMap.evalAlgHom {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {A : Type u_11} [NormedRing A] [NormedAlgebra 𝕜 A] [ContMDiffRing (modelWithCornersSelf 𝕜 A) n A] (x : M) : ContMDiffMap I (modelWithCornersSelf 𝕜 A) M A n →ₐ[𝕜] A

Evaluation at a point x : M, as an algebra homomorphism from the C^n functions on M to their values. This is the algebra version of ContMDiffMap.evalRingHom.

@[simp]

theorem ContMDiffMap.evalAlgHom_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (A : Type u_11) [NormedRing A] [NormedAlgebra 𝕜 A] [ContMDiffRing (modelWithCornersSelf 𝕜 A) n A] (x : M) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 A) M A n) : (evalAlgHom x) f = f x

theorem ContMDiffMap.eq_zero_of_forall_mem_ker_evalAlgHom_smul_top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n) (hf : ∀ (x : M), f ∈ RingHom.ker (evalAlgHom x) • ⊤) : f = 0

The points of M separate the scalar C^n functions: a function lying in ker (ev x) • C^n(M, 𝕜) for every point x is zero.

def Diffeomorph.compRightAlgEquiv (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} (A : Type u_8) [NormedRing A] [NormedAlgebra 𝕜 A] [ContMDiffRing (modelWithCornersSelf 𝕜 A) n A] (φ : Diffeomorph J I N M n) : ContMDiffMap I (modelWithCornersSelf 𝕜 A) M A n ≃ₐ[𝕜] ContMDiffMap J (modelWithCornersSelf 𝕜 A) N A n

Precomposition with a C^n diffeomorphism φ : N → M, as an algebra isomorphism from the C^n functions on M to the C^n functions on N, with inverse the precomposition with φ⁻¹.

theorem Diffeomorph.coe_compRightAlgEquiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} (A : Type u_8) [NormedRing A] [NormedAlgebra 𝕜 A] [ContMDiffRing (modelWithCornersSelf 𝕜 A) n A] (φ : Diffeomorph J I N M n) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 A) M A n) : ⇑((compRightAlgEquiv 𝕜 A φ) f) = ⇑f ∘ ⇑φ

@[simp]

theorem Diffeomorph.compRightAlgEquiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} (A : Type u_8) [NormedRing A] [NormedAlgebra 𝕜 A] [ContMDiffRing (modelWithCornersSelf 𝕜 A) n A] (φ : Diffeomorph J I N M n) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 A) M A n) (x : N) : ((compRightAlgEquiv 𝕜 A φ) f) x = f (φ x)

@[simp]

theorem Diffeomorph.compRightAlgEquiv_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} (A : Type u_8) [NormedRing A] [NormedAlgebra 𝕜 A] [ContMDiffRing (modelWithCornersSelf 𝕜 A) n A] (φ : Diffeomorph J I N M n) (f : ContMDiffMap J (modelWithCornersSelf 𝕜 A) N A n) (x : M) : ((compRightAlgEquiv 𝕜 A φ).symm f) x = f (φ.symm x)

theorem TauCeti.sub_algebraMap_eq_sum_mul_sub_algebraMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {ι : Type u_5} [Fintype ι] (x : M) (g : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n) (a c : ι → ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n) (h : ∀ (y : M), g y - g x = ∑ i : ι, (a i) y * ((c i) y - (c i) x)) : g - (algebraMap 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n)) (g x) = ∑ i : ι, a i * (c i - (algebraMap 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n)) ((c i) x))

Hadamard's identity in the algebra of smooth functions. A pointwise factorization of g - g x through the functions c i, with coefficients a i, is an identity between the bundled smooth maps themselves, the constants appearing as the images of algebraMap.

This is the pointwise-to-bundled transport: the hypothesis speaks of values, the conclusion of elements of C^n⟮I, M; 𝕜⟯, and the two are related by evaluation being a ring homomorphism.

noncomputable def Module.Basis.smoothCoord {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ι : Type u_3} (b : Basis ι 𝕜 E) (i : ι) : ContMDiffMap (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 𝕜) E 𝕜 ↑⊤

The i-th coordinate function of a basis b of a finite-dimensional space, as a smooth function.

@[simp]

theorem Module.Basis.smoothCoord_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ι : Type u_3} (b : Basis ι 𝕜 E) (i : ι) (x : E) : (b.smoothCoord i) x = (b.coord i) x