Powers of the vanishing ideal of a point and jets of smooth functions

Let I_x be the ideal of smooth real functions on a manifold M vanishing at an interior point x, and write φ = extChartAt I x for the extended chart at x. For every m, the power I_x ^ (m + 1), the ideal of finite sums of products of m + 1 functions vanishing at x, consists exactly of the smooth functions f whose chart expression f ∘ φ⁻¹ has vanishing derivatives of every order at most m at φ x. Consequently the quotient C^∞(M) / I_x ^ (m + 1) is the space of m-jets of smooth functions at x: two functions have the same class exactly when their chart expressions have the same Taylor coefficients of order at most m.

Combined with the algebraic fact that a differential operator of order at most m, in Grothendieck's sense of iterated commutators with multiplication operators, maps I_x ^ (m + 1) into I_x, this shows that such an operator on C^∞(M) is local of order m: the value (D f)(x) depends only on the m-jet of f at x. No continuity of D is assumed.

The inclusion of I_x ^ (m + 1) in the functions with vanishing m-jet holds because orders of vanishing add under multiplication. The converse is Hadamard's lemma of order m, TauCeti.mem_smoothVanishingIdeal_pow_succ_of_iteratedFDeriv_eq_zero, proved in TauCeti.Geometry.Manifold.Algebra.VanishingIdeal.Basic. The case m = 1 is TauCeti.mem_smoothVanishingIdeal_sq_iff_of_isInteriorPoint.

Main results

• TauCeti.mem_smoothVanishingIdeal_pow_succ_iff_of_isInteriorPoint: at an interior point of a finite-dimensional Hausdorff manifold, f ∈ I_x ^ (m + 1) if and only if the derivatives of order at most m of f ∘ φ⁻¹ vanish at φ x.
• TauCeti.mem_smoothVanishingIdeal_pow_succ_iff: the same at every point of a boundaryless manifold.
• TauCeti.quotient_mk_smoothVanishingIdeal_pow_succ_eq_iff: two smooth functions have the same class modulo I_x ^ (m + 1) if and only if their chart expressions have the same derivatives of order at most m at φ x.
• TauCeti.differentialOperators_apply_eq_of_iteratedFDeriv_eq: a differential operator of order at most m on C^∞(M) takes the same value at x on two functions with the same m-jet at x.

References

• I. Kolář, P. W. Michor, J. Slovák, Natural operations in differential geometry, Springer, 1993, §§1.3–1.6 and §12.
• A. Grothendieck, Éléments de géométrie algébrique IV, Quatrième partie, §16.8.

theorem TauCeti.iteratedFDeriv_comp_extChartAt_symm_eq_zero_of_mem_smoothVanishingIdeal_pow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {x : M} (hx : I.IsInteriorPoint x) {m : ℕ} {f : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤} (hf : f ∈ smoothVanishingIdeal I x ^ (m + 1)) {k : ℕ} (hk : k ≤ m) : iteratedFDeriv ℝ k (⇑f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x) = 0

A function in I_x ^ (m + 1) has a chart expression whose derivatives of order at most m vanish at the image of x.

theorem TauCeti.mem_smoothVanishingIdeal_pow_succ_iff_of_isInteriorPoint {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] {x : M} (hx : I.IsInteriorPoint x) (m : ℕ) (f : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) : f ∈ smoothVanishingIdeal I x ^ (m + 1) ↔ ∀ k ≤ m, iteratedFDeriv ℝ k (⇑f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x) = 0

The powers of the vanishing ideal. At an interior point x of a finite-dimensional Hausdorff real manifold, a smooth function is a finite sum of products of m + 1 smooth functions vanishing at x if and only if its chart expression has vanishing derivatives of every order at most m at the image of x.

theorem TauCeti.mem_smoothVanishingIdeal_pow_succ_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [BoundarylessManifold I M] (x : M) (m : ℕ) (f : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) : f ∈ smoothVanishingIdeal I x ^ (m + 1) ↔ ∀ k ≤ m, iteratedFDeriv ℝ k (⇑f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x) = 0

The powers of the vanishing ideal. On a finite-dimensional Hausdorff boundaryless real manifold, a smooth function is a finite sum of products of m + 1 smooth functions vanishing at x if and only if its chart expression has vanishing derivatives of every order at most m at the image of x.

theorem TauCeti.quotient_mk_smoothVanishingIdeal_pow_succ_eq_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] {x : M} (hx : I.IsInteriorPoint x) (m : ℕ) (f g : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) : (Ideal.Quotient.mk (smoothVanishingIdeal I x ^ (m + 1))) f = (Ideal.Quotient.mk (smoothVanishingIdeal I x ^ (m + 1))) g ↔ ∀ k ≤ m, iteratedFDeriv ℝ k (⇑f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x) = iteratedFDeriv ℝ k (⇑g ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)

Jets as quotients. At an interior point x, two smooth functions have the same class in C^∞(M) / I_x ^ (m + 1), the space of m-jets at x, if and only if their chart expressions have the same derivatives of every order at most m at the image of x.

theorem TauCeti.differentialOperators_apply_eq_of_iteratedFDeriv_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] {m : ℕ} {D : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤ →ₗ[ℝ] ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤} (hD : D ∈ differentialOperators ℝ (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) m) {x : M} (hx : I.IsInteriorPoint x) {f g : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤} (hfg : ∀ k ≤ m, iteratedFDeriv ℝ k (⇑f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x) = iteratedFDeriv ℝ k (⇑g ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)) : (D f) x = (D g) x

Differential operators factor through jets. At an interior point x, a differential operator of order at most m on C^∞(M), in the sense of iterated commutators with multiplication operators, takes the same value at x on two smooth functions whose chart expressions have the same derivatives of every order at most m at the image of x.