The derivative ideal sheaf D(I) #
[Kol07, Definition 73]: for a scheme X over a field k (f : X ⟶ Spec k) and an ideal sheaf I,
the derivative ideal sheaf D(I) has, on each affine open U, the derivative
Ideal.derivative k (I(U)) of the ideal of sections for the k-algebra structure
f.sectionsAlgebra U (Hironaka/Algebra/RegularSmooth/SmoothAt.lean); it is packaged through
Mathlib's IdealSheafData.ofIdeals, and the compatibility with restriction to basic opens, for f
locally of finite type (derivations extend to localizations, and every derivation of a localization
is locally one of them because Ω_{Γ(U)/k} is finitely presented,
Hironaka/Algebra/Derivative/Localization.lean), is what identifies (D(I))(U) with D(I(U))
(ideal_derivative). The higher derivatives Dʳ(I) iterate (derivativeIter), and the stalks
are the derivatives of the stalks: D(I)_x = D(I_x) (stalkIdeal_derivative,
stalkIdeal_derivativeIter). Also here: the ℚ-algebra structure ℚ → k → 𝒪_{X,x} of a stalk in
characteristic zero (stalkAlgebraRat), which the coordinate structures RegularCoords need.
Used for Theorem 76 and Theorem 88 on schemes
(Hironaka/Scheme/BlowUpSequence/TransformDerivative.lean,
Hironaka/Scheme/BlowUpSequence/Theorem88Basic.lean), for maximal contact and tuning
(Hironaka/Resolution/Algebraic/MaximalContact/Invariant.lean,
Hironaka/Resolution/Algebraic/Tuning/Corollary101.lean), for D-balanced ideals
(Hironaka/Resolution/Algebraic/Balanced/Basic.lean) and throughout Hironaka/Derivative.
The ℚ-algebra structure on a stalk of a scheme over a field k of characteristic zero,
ℚ → k → 𝒪_{X,x} (through f.stalkAlgebra x); not an instance, since it depends on f. The
coordinate structures RegularCoords and the derivative ideals of Hironaka/Local need
[Algebra ℚ R].
Equations
- AlgebraicGeometry.Scheme.Hom.stalkAlgebraRat f x = ((algebraMap k ↑(X.presheaf.stalk x)).comp (algebraMap ℚ k)).toAlgebra
Instances For
The derivative ideal sheaf D(I) of I on the k-scheme X ([Kol07, (73.1)]): on an
affine open U, the derivative of I(U) for the k-algebra structure of Γ(X, U) induced by
f.
Equations
- AlgebraicGeometry.Scheme.IdealSheafData.derivative f I = AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals fun (U : ↑X.affineOpens) => Ideal.derivative k (I.ideal U)
Instances For
The higher derivative ideal sheaves ([Kol07, (73.2)]): D⁰(I) = I,
D^{r+1}(I) = D(Dʳ(I)).
Equations
Instances For
On every affine open, (D(I))(U) ⊆ D(I(U)) (Mathlib's ideal_ofIdeals_le); equality holds
for f locally of finite type (ideal_derivative).
The gluing, for f locally of finite type #
For f locally of finite type, Γ(X, U) is a finitely presented k-algebra on every affine
U (a field is Noetherian), so Ω_{Γ(X, U)/k} is finitely presented.
The family U ↦ D(I(U)) is compatible with restriction to basic opens: Γ(X, D(s)) is the
localization of Γ(X, U) at s (Mathlib's isLocalization_basicOpen), I(D(s)) = I(U)_s
(map_ideal_basicOpen), and D(I(U)_s) = D(I(U))_s (derivative_map).
For f locally of finite type, the derivative ideal sheaf has (D(I))(U) = D(I(U)) on every
affine open ([Kol07, (73.1)]): the compatible family U ↦ D(I(U)) is itself an ideal sheaf,
hence the largest one below it.
Stalks #
The stalk of D(I) at x is the derivative of the stalk I_x in the k-algebra 𝒪_{X,x}:
on an affine U ∋ x the stalk is the localization of Γ(X, U) at the prime of x (Mathlib's
isLocalization_stalk), and D(I(U))_x = D(I(U)_x) by derivative_map.
Dʳ(I)_x = Dʳ(I_x).