Torsion-freeness of the chart presentation #
Let A be a commutative ring, a ∈ A, g : Fin k → A, and suppose the list
[a, g₀, …, g_{k-1}] is weakly regular on A: a is a nonzerodivisor of A and each gⱼ is a
nonzerodivisor of A/(a, g₀, …, g_{j-1}) (Mathlib's RingTheory.Sequence.IsWeaklyRegular, whose
definition is exactly this colon condition along List.take). In M = A[Y₀, …, Y_{k-1}] let
J = ⟨a Yᵢ − gᵢ⟩ be the presentation ideal of the affine blow-up algebra
(Hironaka.Scheme.BlowUp.Presentation). Then a f ∈ J implies f ∈ J, so a and its powers are
nonzerodivisors on M/J. This is the statement the Stacks Project proves for H₁-regular
sequences through the Koszul complex [TSPA, Tag 0BIQ], and the reason Hauser's presentation of a
chart ring by a regular sequence has no torsion — the only linear relations among the generators
are the trivial ones [Hau14, Theorem 4.20 (b)]; the proof below is elementary and never leaves
M. It is used to identify the chart rings of the blow-up of a smooth scheme along a regular
sequence of coordinates as quotients of polynomial rings.
The peeling induction. With J_j = ⟨a Yᵢ − gᵢ : i < j⟩ and Q_j = (a, g₀, …, g_{j-1}) ⊆ A,
two identities of ideals of M: J_{j+1} = J_j + ⟨a Yⱼ − gⱼ⟩, and J_j + ⟨a⟩ = Q_j M
(aYᵢ − gᵢ ∈ (a, gᵢ)M; conversely gᵢ = aYᵢ − (aYᵢ − gᵢ)). Base j = 0: J₀ = 0 and a f = 0
forces f = 0 coefficientwise. Step: from a f = h + (aYⱼ − gⱼ) q with h ∈ J_j we get
gⱼ q = h + a Yⱼ q − a f ∈ J_j + ⟨a⟩ = Q_j M, i.e. gⱼ · coeff_m(q) ∈ Q_j for every monomial m
(MvPolynomial.mem_map_C_iff); the regularity of gⱼ modulo Q_j gives coeff_m(q) ∈ Q_j, so
q ∈ Q_j M = J_j + ⟨a⟩, q = h' + a q'; substituting, a (f − (aYⱼ − gⱼ) q') ∈ J_j, the
induction hypothesis gives f − (aYⱼ − gⱼ) q' ∈ J_j, and f ∈ J_{j+1}. The order with a
first is what the induction uses (a = x, g₀ = xy in ℚ[x, y] is a counterexample to the
statement without it).
The partial presentation ideals and their base ideals #
J_j = ⟨a Yᵢ − gᵢ : i < j⟩.
Equations
- AlgebraicGeometry.affineBlowUpAlgebra.partialPresentationIdeal a g j = Ideal.span ((fun (i : Fin k) => MvPolynomial.C a * MvPolynomial.X i - MvPolynomial.C (g i)) '' {i : Fin k | ↑i < j})
Instances For
The identity J_j + ⟨a⟩ = Q_j M.
The regularity hypotheses, extracted from IsWeaklyRegular #
The j-th clause of weak regularity, in colon form: gⱼ c ∈ Q_j ⟹ c ∈ Q_j.
The peeling induction #
The presentation ideal is saturated with respect to a: a f ∈ J implies f ∈ J
[TSPA, Tag 0BIQ]; [Hau14, Theorem 4.20 (b)].
a is a nonzerodivisor on A[Y]/J.
The powers of a are nonzerodivisors on A[Y]/J.