The vanishing ideal of a point and its cotangent space #
For a point x of a smooth real manifold M, the smooth real functions vanishing at x form an
ideal I_x of the ring C^∞⟮I, M; ℝ⟯, the kernel of evaluation at x. When x is an interior
point of a finite-dimensional Hausdorff manifold, the square of I_x, the ideal of finite sums of
products of two functions vanishing at x, consists exactly of the functions whose value and
differential both vanish at x. Consequently, at such a point, the algebraic cotangent space
I_x / I_x² is canonically the cotangent space T_x*M, the class of f going to df_x. This
identification is natural: pulling functions back along a smooth map corresponds to the transpose
of its differential, so restriction to an open set is an isomorphism, and the classes of the chart
coordinates form the dual basis of the coordinate basis. This is the scalar foundation of the
algebraic description of jets and differential operators.
Main results #
TauCeti.smoothVanishingIdeal: the ideal of smooth real functions vanishing at a point.Module.Basis.smoothVanishingIdeal_eq_span: Hadamard's lemma; on a finite-dimensional space,I_xis the ideal generated by the coordinate functions of a basis, each relative to its value atx.TauCeti.mem_smoothVanishingIdeal_pow_succ_of_iteratedFDeriv_eq_zero: Hadamard's lemma of orderm; at an interior point, a function whose chart expression has vanishing derivatives of every order at mostmlies inI_x ^ (m + 1).TauCeti.mem_smoothVanishingIdeal_sq_iff_of_isInteriorPoint: at an interior point of a finite-dimensional Hausdorff manifold,f ∈ I_x²if and only iff x = 0anddf_x = 0.TauCeti.mem_smoothVanishingIdeal_sq_iff: the same at every point of a boundaryless manifold.TauCeti.smoothCotangentEquiv: the real-linear equivalenceI_x / I_x² ≃ T_x*Msending the class offto its differential atx.TauCeti.smoothCotangentMap: the pullbackI_x / I_x² → I_y / I_y²along a smooth mapφwithφ y = x, functorial inφ. UndersmoothCotangentEquivit is the transpose ofdφ_y(TauCeti.smoothCotangentEquiv_smoothCotangentMap), so it is bijective whendφ_yis invertible (TauCeti.smoothCotangentMap_bijective).TauCeti.smoothCotangentRestrictEquiv: restriction to an open neighbourhood ofxis an isomorphism of algebraic cotangent spaces.TauCeti.smoothCotangentBasis: the basis ofI_x / I_x²dual to a chosen basis of the model space, formed by the classes of the localized chart coordinates (TauCeti.smoothCotangentBasis_eq_toCotangent).TauCeti.smoothVanishingIdeal_sq_eq_self: on a zero-dimensional manifoldI_x² = I_x.
Implementation notes #
The powers of I_x are reached by Taylor's formula in a chart. Up to a function vanishing near
x, a function whose chart expression has vanishing derivatives of order at most m at the image
of x is a finite sum of products of m + 1 localized coordinate functions vanishing at x with
smooth coefficients. A function vanishing near x is itself the product of a function vanishing
at x with any power of one minus a bump function. The square is the case m = 1: at an interior
point, the differential of f is the derivative of its chart expression. The converse inclusions
for higher powers are in TauCeti.Geometry.Manifold.Algebra.VanishingIdeal.Pow.
References #
- I. Kolář, P. W. Michor, J. Slovák, Natural operations in differential geometry, Springer, 1993, §§1.3–1.6 and §12.
The ideal of smooth real functions on M vanishing at x: the kernel of evaluation at x.
Instances For
A smooth function lies in the vanishing ideal at x exactly when it vanishes at x.
A function in the square of the vanishing ideal at x vanishes at x.
A function in the square of the vanishing ideal at x has zero differential at x.
Unlike its order-m analogue
TauCeti.iteratedFDeriv_comp_extChartAt_symm_eq_zero_of_mem_smoothVanishingIdeal_pow, this holds
at every point of every manifold, with no interior-point, finite-dimensionality or Hausdorff
hypothesis, which is what lets the differential descend to I_x / I_x² in general.
The vanishing ideal at φ y is the preimage of the vanishing ideal at y under the pullback
f ↦ f ∘ φ along a smooth map φ.
The pullback along φ of a smooth function vanishing at x = φ y vanishes at y.
The pullback I_x / I_x² → I_y / I_y² of algebraic cotangent spaces along a smooth map
φ : N → M with φ y = x, induced by f ↦ f ∘ φ. Under the identifications
smoothCotangentEquiv it is the transpose of the differential of φ at y
(TauCeti.smoothCotangentEquiv_smoothCotangentMap). The point x is a separate argument so that
the map composes along composites of smooth maps (TauCeti.smoothCotangentMap_comp).
Instances For
The pullback along φ sends the class of f to the class of f ∘ φ.
The pullback along the identity is the identity.
The pullback along a composite is the composite of the pullbacks, in the reverse order.
A smooth function vanishing on a neighbourhood of x lies in every power of the vanishing
ideal at x.
Hadamard's lemma of order m. At an interior point x, a smooth function whose chart
expression has vanishing derivatives of every order at most m at the image of x lies in
I_x ^ (m + 1).
Hadamard's lemma for the vanishing ideal. At an interior point x, a smooth function whose
value and differential vanish at x lies in the square of the vanishing ideal at x.
At an interior point x of a finite-dimensional Hausdorff real manifold, a smooth function is
a finite sum of products of smooth functions vanishing at x if and only if its value and its
differential vanish at x.
On a finite-dimensional Hausdorff boundaryless real manifold, a smooth function is a finite sum
of products of smooth functions vanishing at x if and only if its value and its differential
vanish at x.
The algebraic cotangent space of a point is the cotangent space. At an interior point x
of a finite-dimensional Hausdorff real manifold, sending a function vanishing at x to its
differential at x induces a real-linear equivalence I_x / I_x² ≃ T_x*M.
Instances For
The equivalence I_x / I_x² ≃ T_x*M sends the class of f to the differential df_x.
Coordinate differentials. If, near an interior point x, a function f vanishing at x
agrees with a linear functional ℓ of the chart coordinates, then the cotangent class of f
corresponds to ℓ. In particular, for a basis b of the model space, the classes of the
localized coordinate functions b.coord i ∘ extChartAt I x correspond to the dual basis.
The coordinate-differential basis. At an interior point x, the basis of I_x / I_x²
corresponding under smoothCotangentEquiv to the dual basis of a basis b of the model space.
Its i-th vector is the class of any function vanishing at x that agrees near x with the
localized chart coordinate b.coord i ∘ extChartAt I x - b.coord i (extChartAt I x x)
(smoothCotangentBasis_eq_toCotangent); such functions exist
(exists_toCotangent_eq_smoothCotangentBasis).
Instances For
The coordinate-differential basis corresponds under smoothCotangentEquiv to the dual basis
of b.
The i-th coordinate-differential basis vector is the class of any function vanishing at x
that agrees near x with the localized chart coordinate
b.coord i ∘ extChartAt I x - b.coord i (extChartAt I x x).
Each coordinate-differential basis vector is the class of a smooth function vanishing at x
that agrees near x with the localized chart coordinate
b.coord i ∘ extChartAt I x - b.coord i (extChartAt I x x).
Zero-dimensional manifolds. When the model space is zero, the algebraic cotangent space at every point vanishes.
When the model space is zero, the vanishing ideal at every point equals its square: every
smooth function vanishing at x is a finite sum of products of such functions.
Naturality of the cotangent identification. For a smooth map φ : N → M and interior
points y and x = φ y, the pullback of cotangent classes along φ corresponds, under
smoothCotangentEquiv, to the transpose of the differential dφ_y: the class of f at x
goes to df_x ∘ dφ_y.
If the differential of a smooth map φ at an interior point y is invertible, for instance
for a local diffeomorphism, the pullback of cotangent classes I_x / I_x² → I_y / I_y² along φ,
where x = φ y, is bijective.
Restriction to an open set. For an open set U and an interior point x of M lying in
U, restricting smooth functions from M to U induces an isomorphism of algebraic cotangent
spaces I_x(M) / I_x(M)² ≃ I_x(U) / I_x(U)².
Instances For
Restriction to an open set is the pullback of cotangent classes along the inclusion of U.
Restriction to an open set sends the class of f to the class of its restriction.
Restriction to an open set is compatible with the identifications of the algebraic cotangent
spaces with the cotangent space, the tangent spaces of U and M at x being identified by
tangentSpaceOpenEquiv.
Hadamard's lemma. On a finite-dimensional space, the smooth functions vanishing at x
form the ideal generated by the coordinate functions of b, each taken relative to its value at
x.