The logarithmic derivative ideal sheaf: gluing, stalks, restriction, filtration

[Kol07, 87] for the sheaf D(−log S)(I) of Hironaka/Scheme/IdealSheaf/Derivative/Logarithmic.lean, on a scheme f : X ⟶ Spec k.

• Gluing (ideal_logDerivative): for f locally of finite type, (D(−log S)(I))(U) = D(−log S(U))(I(U)) on every affine open U. As for derivative of Hironaka/Scheme/IdealSheaf/Derivative/Sheaf.lean, the family U ↦ D(−log S(U))(I(U)) is compatible with restriction to basic opens (Γ(D(s)) = Γ(U)_s, S(D(s)) = S(U)_s, I(D(s)) = I(U)_s, and D(−log S(U)_s)(I(U)_s) = D(−log S(U))(I(U))_s by Ideal.logDerivative_map of Hironaka/Scheme/IdealSheaf/Derivative/LogarithmicLocalization.lean, which needs Ω_{Γ(U)/k} finitely presented and S(U) finitely generated: Γ(U) is a finitely generated k-algebra, hence Noetherian), so it is itself an ideal sheaf, the largest one below it.
• Stalks (stalkIdeal_logDerivative, stalkIdeal_logDerivativeIter): (D(−log S)(I))_x = D(−log S_x)(I_x), the logarithmic derivations of the stalk being the k-derivations of 𝒪_{X,x} preserving S_x; the same compatibility for the localization 𝒪_{X,x} = Γ(U)_𝔭.
• Restriction ([Kol07, (87.1)]; logDerivativeIter_comap_subschemeι): (D^r(−log S)(I))|_S = D^r(I|_S) as ideal sheaves on V(S), for X smooth over k. Stalkwise: the stalk of K.comap ι at z ∈ V(S) is ι^♯(K_{ι z}) (stalkIdeal_comap, Hironaka/Scheme/IdealSheaf/StalkIdeal.lean), the stalk map 𝒪_{X,ι z} → 𝒪_{V(S),z} is surjective with kernel S_{ι z} (ker_stalkMap_subschemeι, Hironaka/Scheme/Smooth/SubschemeStalk.lean), 𝒪_{X,ι z} is formally smooth over k (formallySmooth_stalk, Hironaka/Scheme/IdealSheaf/Derivative/StalkCoords.lean), and the ring-level Ideal.logDerivativeIter_map_of_surjective of Hironaka/Scheme/IdealSheaf/Derivative/LogarithmicQuotient.lean applies. Only the smoothness of X is used: the identity holds for every closed subscheme S, while Kollár states it for S smooth.
• Filtration ([Kol07, (87.2)]; logDerivativeIter_derivativeIter_le, logDerivativeIter_le_derivativeIter): D^s(−log S)(I) ⊆ D^{s−1}(−log S)(D(I)) ⊆ ⋯ ⊆ D^s(I), from D(−log S)(K) ⊆ D(K) and the monotonicity of the iterates.

Used for Theorem 88 and Corollary 89 on schemes (Hironaka/Scheme/BlowUpSequence/Theorem88Basic.lean, Hironaka/Resolution/Algebraic/Kol07/Theorem88BlowUp.lean, Hironaka/Resolution/Algebraic/Kol07/Theorem88Sequence.lean, Hironaka/Resolution/Algebraic/Kol07/Corollary89.lean, Hironaka/Scheme/BlowUpSequence/TransformLogDerivative.lean) and on manifolds (Hironaka/Manifold/IdealSheaf/LogDerivRestrict.lean).

The filtration, for any k-scheme

theorem AlgebraicGeometry.Scheme.IdealSheafData.logDerivativeIter_mono {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (S : X.IdealSheafData) (r : ℕ) {I I' : X.IdealSheafData} (h : I ≤ I') : logDerivativeIter f S r I ≤ logDerivativeIter f S r I'

theorem AlgebraicGeometry.Scheme.IdealSheafData.logDerivativeIter_succ' {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (S I : X.IdealSheafData) (r : ℕ) : logDerivativeIter f S (r + 1) I = logDerivativeIter f S r (logDerivative f S I)

theorem AlgebraicGeometry.Scheme.IdealSheafData.logDerivativeIter_le_derivativeIter {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (S I : X.IdealSheafData) (s : ℕ) : logDerivativeIter f S s I ≤ derivativeIter f s I

[Kol07, (87.2)]: D^s(−log S)(I) ⊆ D^s(I).

theorem AlgebraicGeometry.Scheme.IdealSheafData.logDerivativeIter_derivativeIter_le {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (S I : X.IdealSheafData) {s j : ℕ} (hj : j < s) : logDerivativeIter f S (s - j) (derivativeIter f j I) ≤ logDerivativeIter f S (s - (j + 1)) (derivativeIter f (j + 1) I)

[Kol07, (87.2)], one step of the filtration D^s(−log S)(I) ⊆ D^{s−1}(−log S)(D(I)) ⊆ ⋯ ⊆ D^s(I).

The gluing and the stalks, for f locally of finite type

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_fg {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (S : X.IdealSheafData) [LocallyOfFiniteType f] (U : ↑X.affineOpens) : (S.ideal U).FG

For f locally of finite type, Γ(X, U) is Noetherian on every affine U, so every ideal of sections is finitely generated.

theorem AlgebraicGeometry.Scheme.IdealSheafData.map_logDerivative_ideal_basicOpen {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (S I : X.IdealSheafData) [LocallyOfFiniteType f] (U : ↑X.affineOpens) (s : ↑(X.presheaf.obj (Opposite.op ↑U))) : Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (Ideal.logDerivative k (S.ideal U) (I.ideal U)) = Ideal.logDerivative k (S.ideal (X.affineBasicOpen s)) (I.ideal (X.affineBasicOpen s))

The family U ↦ D(−log S(U))(I(U)) is compatible with restriction to basic opens (Mathlib's isLocalization_basicOpen, map_ideal_basicOpen, and Ideal.logDerivative_map).

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_logDerivative {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (S I : X.IdealSheafData) [LocallyOfFiniteType f] (U : ↑X.affineOpens) : (logDerivative f S I).ideal U = Ideal.logDerivative k (S.ideal U) (I.ideal U)

The gluing ([Kol07, 87] for the sheaf): for f locally of finite type, (D(−log S)(I))(U) = D(−log S(U))(I(U)) on every affine open.

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_logDerivative {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (S I : X.IdealSheafData) [LocallyOfFiniteType f] (x : ↥X) : (logDerivative f S I).stalkIdeal x = Ideal.logDerivative k (S.stalkIdeal x) (I.stalkIdeal x)

The stalk of D(−log S)(I) at x is the logarithmic derivative of the stalk I_x for the k-derivations of 𝒪_{X,x} preserving S_x.

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_logDerivativeIter {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (S I : X.IdealSheafData) [LocallyOfFiniteType f] (r : ℕ) (x : ↥X) : (logDerivativeIter f S r I).stalkIdeal x = Ideal.logDerivativeIter k (S.stalkIdeal x) r (I.stalkIdeal x)

(D^r(−log S)(I))_x = D^r(−log S_x)(I_x).

Restriction to S ([Kol07, (87.1)])

theorem AlgebraicGeometry.Scheme.IdealSheafData.logDerivativeIter_comap_subschemeι {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (S I : X.IdealSheafData) (n : ℕ) [SmoothOfRelativeDimension n f] (r : ℕ) : (logDerivativeIter f S r I).comap S.subschemeι = derivativeIter (CategoryTheory.CategoryStruct.comp S.subschemeι f) r (I.comap S.subschemeι)

[Kol07, (87.1)]: (D^r(−log S)(I))|_S = D^r(I|_S) as ideal sheaves on V(S), the restriction being the inverse image along the closed immersion ι : V(S) ⟶ X. Stalkwise at z ∈ V(S): the stalk map ι^♯ : 𝒪_{X,ι z} → 𝒪_{V(S),z} is surjective with kernel S_{ι z}, and ι^♯(D^r(−log S_{ι z})(I_{ι z})) = D^r(ι^♯ I_{ι z}) because 𝒪_{X,ι z} is formally smooth over k. Only the smoothness of X is used: the identity holds for every closed subscheme S (Kollár states it for S smooth).