Taylor expansion and Krull's intersection theorem, in the form needed #
Kollár's proof of [Kol07, Proposition 94] takes "the Taylor expansion
f(x₁+b₁, …, xₙ+bₙ) = f + ∑ᵢ bᵢ ∂f/∂xᵢ + ½ ∑ᵢⱼ bᵢbⱼ ∂²f/∂xᵢ∂xⱼ + ⋯" modulo 𝔪^{s+1} and lets
s → ∞ by Krull's intersection theorem (recalled in [Kol07, Definition 55]). This file
provides what that proof needs (Hironaka/Algebra/Local/Prop94.lean):
- the iterated partial derivatives
∂^α = ∏ᵢ ∂ᵢ^{αᵢ}onMvPolynomial (Fin n) A(pderivPow) and the exact multivariate Taylor formula for polynomials over aℚ-algebra,P(g + b) = ∑_α (1/α!) (∂^α P)(g) b^α, by the monomial computation∂^α X^β = β!/(β-α)! X^{β-α}and the binomial theorem; - truncation and substitution in
K⟦X⟧and the Taylor formula modulo𝔪^{s+1}for power series, with its one-direction form (a shift of a single coordinate); - Krull's intersection theorem in closed form,
I = ⋂ₛ (I + 𝔪^s), used also inHironaka/Algebra/Local/PowerSeriesEndomorphism.leanandHironaka/Algebra/Local/CoordsOver.lean.
Iterated partial derivatives of polynomials #
The coordinate derivations of MvPolynomial (Fin n) A commute (the polynomial analogue of
MvPowerSeries.pderiv_pderiv_comm).
∂ᵢ as an A-linear endomorphism of MvPolynomial (Fin n) A.
Equations
Instances For
The iterated partial derivative ∂^α = ∏ᵢ ∂ᵢ^{αᵢ} of a multi-index α, on polynomials (the
higher derivatives of the Taylor expansion in the proof of [Kol07, Proposition 94]).
Equations
- IsLocalRing.pderivPow α = Finset.univ.noncommProd (fun (i : Fin n) => IsLocalRing.pderivEnd i ^ α i) ⋯
Instances For
∂^α X^β = (∏ᵢ βᵢ!/(βᵢ-αᵢ)!) X^{β-α} (zero unless α ≤ β).
The Taylor formula for a monomial: (g + b)^β = ∑_{α ≤ β} (1/α!) (∂^α X^β)(g) b^α, the
binomial theorem in each variable.
The multivariate Taylor formula (Kollár's "take the Taylor expansion" in the proof of
[Kol07, Proposition 94]; Włodarczyk's "the Taylor formula for n unknowns" in the proof of
[Wlo05, Lemma 2.9.6]): for a polynomial P over a ℚ-algebra and g, b in a ℚ-algebra S,
P(g + b) = ∑_α (1/α!) (∂^α P)(g) b^α, the sum over the multi-indices α ≤ d for any bound d
on the exponents of P.
The Taylor formula in Kollár's form: P(X + b) = ∑_α (1/α!) (∂^α P) b^α for P ∈ A[X],
b ∈ Aⁿ.
Iterated partial derivatives and 𝔪-adic estimates in K⟦X⟧ #
∂ᵢ = pderiv K i as a K-linear endomorphism of K⟦X⟧.
Equations
Instances For
The iterated partial derivative ∂^α on K⟦X⟧.
Equations
- IsLocalRing.pderivPowSeries α = Finset.univ.noncommProd (fun (i : Fin n) => IsLocalRing.pderivEnd' i ^ α i) ⋯
Instances For
∂^α on K⟦X⟧ restricts to ∂^α on polynomials.
A coordinate partial lowers the 𝔪-adic order by at most one (Kollár's step
∂^α f ∈ 𝔪^{s+1-|α|} in the proof of [Kol07, Proposition 94]; the K⟦X⟧ form of
RegularCoords.D_maximalIdeal_pow).
∂^α lowers the 𝔪-adic order by at most |α|.
b^α ∈ 𝔪^{|α|} for bᵢ ∈ 𝔪.
f ≡ truncTotal (s+1) f (mod 𝔪^{s+1}).
Xᵢ ↦ Xᵢ + bᵢ is a substitution when bᵢ ∈ 𝔪.
The substitution Xᵢ ↦ Xᵢ + bᵢ maps 𝔪^{s+1} into 𝔪^{s+1}.
The multi-indices of total degree ≤ s (the index set of Kollár's Taylor sum modulo
𝔪^{s+1}).
Equations
- IsLocalRing.degreeLE n s = {α ∈ Finset.Iic (Finsupp.equivFunOnFinite.symm fun (x : Fin n) => s) | Finsupp.degree α ≤ s}
Instances For
The Taylor formula modulo 𝔪^{s+1} (the proof of [Kol07, Proposition 94], in truncated
form): for bᵢ ∈ 𝔪, f(X + b) ≡ ∑_{|α| ≤ s} (1/α!) (∂^α f) b^α (mod 𝔪^{s+1}).
The one-direction Taylor formula (the converse direction of the proof of
[Kol07, Proposition 94]): f(X₁ + λb, X₂, …) ≡ ∑_{j ≤ s} λ^j (b^j/j!) ∂₁^j f (mod 𝔪^{s+1}) for
b ∈ 𝔪, λ ∈ ℚ, along any coordinate i.
Krull's intersection theorem in closed form #
Krull's intersection theorem in the form I = ⋂ₛ (I + 𝔪^s) recalled in
[Kol07, Definition 55] and used ("letting s go to infinity") in the proof of
[Kol07, Proposition 94]: in a Noetherian local ring, f ∈ I + 𝔪^s for all s implies f ∈ I.
Krull's intersection theorem in closed form: I = ⋂ₛ (I + 𝔪^s).