The order of an ideal at the rational points of affine space #
[Hau03, Appendix B, Exercises 3 and 4] compute the strata of constant order of f = x³ + yᵏzᵐ on
𝔸³ and of the four coordinate hyperplanes on 𝔸⁴ at the points a = (a₁, …, aₙ) ∈ 𝔸ⁿ; over an
algebraically closed field these are all the closed points. This module supplies the vocabulary
and the tools for such computations (the exercises themselves are worked out in
HironakaExamples/HauserExercisesOrderStrata.lean):
- the
K-rational pointratPoint aof𝔸ⁿ_K = Spec K[x₁, …, xₙ], the prime ideal of the polynomials vanishing ata(the kernel of evaluation ata; defined inHironaka/Scheme/Smooth/CoordinateSystem.lean, where the origin isratPoint 0); - the derivative criterion for the order at a point of
𝔸ⁿ_K(Kof characteristic zero):c ≤ ord_p I ⟺ D^{c-1}(I) ⊆ 𝔭(le_ord_specIdealSheaf_iff), from the cosupport transferc ≤ ord_x I ⟺ x ∈ V(D^{c-1} I)([Kol07, Lemma 74 (3)], [Wlo05, Lemma 2.6.2];Hironaka/Scheme/IdealSheaf/Derivative/Cosupport.lean) read at the stalk𝒪_{𝔸ⁿ,p} = K[x]_𝔭(Mathlib'sStructureSheaf.IsLocalization.to_stalk), where the derivative ideal is the localization of the derivative ideal (Hironaka/Algebra/Derivative/Localization.lean); onK[x]the derivative ideal of(f)is spanned byfand its partial derivatives (Kol07, Definition 73: the∂/∂xᵢgenerateDer_K(K[x]),derivative_span_eq), andD^r((f))by the iterated partials of order≤ r(derivativeIter_span_singleton). At a rational point this is Hauser's description of the order by the vanishing of the Taylor coefficients (Hau03, Appendix A, Exercise 1; in characteristic zero the Taylor coefficients are the partial derivatives divided by factorials):c ≤ ord_a f ⟺all partial derivatives offof order< cvanish ata(le_ord_specIdealSheaf_span_singleton_iff); - the multiplicativity of the order at a point of
𝔸ⁿ_K(the stalk is a regular local ring containingℚ, where the order of a product is the sum,ordElem_mul_of_algebraRatofHironaka/Algebra/Local/CohenIso.lean):ord_p(fg) = ord_p f + ord_p g(ord_specIdealSheaf_span_singleton_mul), andord_a xᵢ = 1or0according asaᵢ = 0or not (ord_specIdealSheaf_span_singleton_X).
The last section works [Hau03, Appendix B, Exercise 3] for f = x³ + yᵏzᵐ on 𝔸³: the locus of
order ≥ 2 and the locus of order 3 (two_le_ord_hauserEx3_iff, ord_hauserEx3_eq_three_iff).
Used for the examples (HironakaExamples/OrderStrata.lean,
HironakaExamples/HauserExercisesOrderStrata.lean,
HironakaExamples/OrderReduction/Example106.lean, HironakaExamples/MaximalContact/Example82.lean,
HironakaExamples/Sequence/CuspWitness.lean, HironakaExamples/Sequence/Remark33OrderSeq.lean).
Derivations of K[x] are generated by the partial derivatives ([Kol07, Definition 73]) #
[Kol07, Definition 73] ("the derivations ∂/∂x₁, …, ∂/∂xₙ are local generators of Der_X")
on 𝔸ⁿ: every K-derivation of K[x] is ∑ᵢ δ(xᵢ) ∂/∂xᵢ.
The ∂/∂xᵢ span Der_K(K[x]) over K[x].
[Kol07, Definition 73], D(f₁, …, f_s) = (fᵢ, ∂fᵢ/∂xⱼ), on 𝔸ⁿ: D(⟨S⟩) = ⟨S, ∂s/∂xᵢ⟩.
The iterated partial derivative ∂_{l₀} ∂_{l₁} ⋯ f along a list of indices.
Equations
- AlgebraicGeometry.pderivList l f = List.foldr (fun (i : Fin n) (g : MvPolynomial (Fin n) K) => (MvPolynomial.pderiv i) g) f l
Instances For
Dʳ((f)) is spanned by the iterated partial derivatives of f of order at most r (the
higher derivatives of [Kol07, Definition 73] on 𝔸ⁿ).
Dʳ((f)) ⊆ 𝔭 iff every iterated partial derivative of f of order ≤ r lies in 𝔭.
The stalk of 𝔸ⁿ_K at a point, as the localization of K[x] #
Dʳ(J B) = Dʳ(J) B for a localization B of A with Ω_{A/k} finitely presented
(Ideal.derivative_map of Hironaka/Algebra/Derivative/Localization.lean, iterated).
The stalk of the ideal sheaf of J ⊆ R on Spec R at 𝔭 is J R_𝔭 (specIdealSheaf of
Hironaka/Scheme/BlowUp/AffineBlowUp/Universal/Admissible.lean, Mathlib's toStalk):
stalkIdeal_ofIdealTop of Hironaka/Scheme/BlowUp/AffineBlowUp/Universal/Membership.lean in the
toStalk spelling.
The order of the ideal sheaf (f) at 𝔭 is the order (ordElem) of the image of f in the
stalk R_𝔭.
The unit ideal has order 0 everywhere.
The K-algebra structure of the stalk 𝒪_{𝔸ⁿ,p} induced by the structure morphism is
K → K[x] → K[x]_𝔭 (the stalk as an algebra over K[x] through Mathlib's toStalk).
The scalar tower K → K[x] → 𝒪_{𝔸ⁿ,p} for the structures induced by the structure morphism and
by toStalk.
The derivative criterion for the order on 𝔸ⁿ_K ([Kol07, Lemma 74 (3)] and
[Wlo05, Lemma 2.6.2], read at the stalk K[x]_𝔭): for c ≥ 1, c ≤ ord_𝔭 J iff
D^{c-1}(J) ⊆ 𝔭.
Hauser's criterion ([Hau03, Appendix A, Exercise 1], in derivative form): at a rational point
a, c ≤ ord_a f iff all partial derivatives of f of order < c vanish at a.
The order is multiplicative on 𝔸ⁿ_K, ord_𝔭(fg) = ord_𝔭 f + ord_𝔭 g: the stalk is a regular
local ring containing ℚ (ordElem_mul_of_algebraRat).
[Hau03, Appendix B, Exercise 4], the divisor Y = V(∏ xᵢ^{eᵢ}): the order of a monomial at a
rational point is the sum of the exponents of the vanishing coordinates.
[Hau03, Appendix B, Exercise 4], the union of the coordinate hyperplanes X = V(∏ xᵢ): the
order at a rational point is the number of vanishing coordinates.
[Hau03, Appendix B, Exercise 3]: f = x³ + yᵏzᵐ on 𝔸³ #
A numeral constant has zero partial derivatives (the OfNat form of
Derivation.map_natCast, for simp).
Hauser's f = x³ + yᵏzᵐ ([Hau03, Appendix B, Exercise 3]), with x = x₀, y = x₁, z = x₂.
Equations
- AlgebraicGeometry.hauserEx3Poly K k m = MvPolynomial.X 0 ^ 3 + MvPolynomial.X 1 ^ k * MvPolynomial.X 2 ^ m
Instances For
[Hau03, Appendix B, Exercise 3]: the locus of order ≥ 2 of x³ + yᵏzᵐ (k, m ≥ 1) — the
z-axis if k ≥ 2, the y-axis if m ≥ 2, and the origin.
[Hau03, Appendix B, Exercise 3]: the locus of order 3 of x³ + yᵏzᵐ (k, m ≥ 1) — the
z-axis if k ≥ 3, the y-axis if m ≥ 3, and the origin if k + m ≥ 3.