Logarithmic derivations in coordinates

[Kol07, 87]: in local coordinates with S = (x₁ = 0), the sheaf Der_X(−log S) of logarithmic derivations is generated by x₁ ∂₁, ∂₂, …, ∂ₙ, and D(−log S)(I) is generated by I and their values on I. Here the coordinate system is RegularCoords on a regular local ring R, with the hypotheses of Hironaka/Algebra/Local/CoordsOver.lean that the coordinate derivations ∂ᵢ are k-linear (IsLinearOver) and span the k-derivations (SpansDerivations: every k-derivation is δ = ∑ᵢ δ(xᵢ) ∂ᵢ, eq_sum_smul_pderivOver), and S = V(x_h).

• The k-derivations preserving (x_h) are the R-span of x_h ∂_h and the ∂_j, j ≠ h (preserving_span_x_eq). The generators preserve (x_h) (x_smul_pderivOver_preservesIdeal, pderivOver_preservesIdeal_of_ne, from Hironaka/Algebra/Local/LogDeriv.lean); conversely δ = ∑ᵢ δ(xᵢ) ∂ᵢ with δ(x_h) = b · x_h, so δ = b · (x_h ∂_h) + ∑_{j ≠ h} δ(x_j) ∂_j.
• Kollár's ideal D(−log (x_h))(I) over all k-derivations preserving (x_h) (Ideal.logDerivative, Hironaka/Scheme/IdealSheaf/Derivative/Logarithmic.lean) is the coordinate logarithmic derivative ideal c.Dlog h I of Hironaka/Algebra/Local/LogDeriv.lean (logDerivative_eq_Dlog), and the iterates agree (logDerivativeIter_eq_Dlogpow), just as derivative_eq_D of Hironaka/Algebra/Derivative/Basic.lean identifies D(I) with c.D I.

Used for the stalks of the logarithmic derivative sheaves on manifolds (Hironaka/Manifold/IdealSheaf/LogDerivLemmas.lean).

theorem IsLocalRing.RegularCoords.x_smul_pderivOver_preservesIdeal {k : Type u_1} [CommRing k] {R : Type u_2} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] [Algebra k R] {n : ℕ} (c : RegularCoords R n) (hk : c.IsLinearOver k) (h i : Fin n) : (c.x i • c.pderivOver hk i).PreservesIdeal (Ideal.span {c.x h})

x_i ∂_i preserves (x_h) for every i (x_smul_pderiv_mem_logDerE, Hironaka/Algebra/Local/LogDeriv.lean).

theorem IsLocalRing.RegularCoords.pderivOver_preservesIdeal_of_ne {k : Type u_1} [CommRing k] {R : Type u_2} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] [Algebra k R] {n : ℕ} (c : RegularCoords R n) (hk : c.IsLinearOver k) (h : Fin n) {j : Fin n} (hj : j ≠ h) : (c.pderivOver hk j).PreservesIdeal (Ideal.span {c.x h})

∂_j preserves (x_h) for j ≠ h (pderiv_mem_span_x_of_ne').

theorem IsLocalRing.RegularCoords.eq_sum_smul_pderivOver {k : Type u_1} [CommRing k] {R : Type u_2} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] [Algebra k R] {n : ℕ} (c : RegularCoords R n) (hk : c.IsLinearOver k) (hs : c.SpansDerivations k) (δ : Derivation k R R) : δ = ∑ i : Fin n, δ (c.x i) • c.pderivOver hk i

A k-derivation is the R-combination ∑ᵢ δ(xᵢ) ∂ᵢ of the k-linear coordinate derivations, when these span the k-derivations.

theorem IsLocalRing.RegularCoords.preserving_span_x_eq {k : Type u_1} [CommRing k] {R : Type u_2} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] [Algebra k R] {n : ℕ} (c : RegularCoords R n) (hk : c.IsLinearOver k) (hs : c.SpansDerivations k) (h : Fin n) : Derivation.preserving k (Ideal.span {c.x h}) = Submodule.span R ({c.x h • c.pderivOver hk h} ∪ (fun (j : Fin n) => c.pderivOver hk j) '' {j : Fin n | j ≠ h})

[Kol07, 87], Der_X(−log S) = ⟨x₁ ∂/∂x₁, ∂/∂x₂, …, ∂/∂xₙ⟩ in coordinates with S = (x₁ = 0): the k-derivations preserving (x_h) are the R-span of x_h ∂_h and the ∂_j, j ≠ h.

theorem IsLocalRing.RegularCoords.logDerivative_eq_Dlog {k : Type u_1} [CommRing k] {R : Type u_2} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] [Algebra k R] {n : ℕ} (c : RegularCoords R n) (hk : c.IsLinearOver k) (hs : c.SpansDerivations k) (h : Fin n) (I : Ideal R) : Ideal.logDerivative k (Ideal.span {c.x h}) I = c.Dlog h I

The ideal D(−log (x_h))(I) of [Kol07, 87] over all k-derivations preserving (x_h) is the coordinate logarithmic derivative ideal c.Dlog h I of Hironaka/Algebra/Local/LogDeriv.lean.

theorem IsLocalRing.RegularCoords.logDerivativeIter_eq_Dlogpow {k : Type u_1} [CommRing k] {R : Type u_2} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] [Algebra k R] {n : ℕ} (c : RegularCoords R n) (hk : c.IsLinearOver k) (hs : c.SpansDerivations k) (h : Fin n) (s : ℕ) (I : Ideal R) : Ideal.logDerivativeIter k (Ideal.span {c.x h}) s I = c.Dlogpow h s I

The iterates: D^s(−log (x_h))(I) = c.Dlogpow h s I.