Order along a coordinate subspace: symbolic equals ordinary power

Kollár defines ord_Z I at the generic point of Z [Kol07, Definition 47] and remarks that "the number ord_Z I equals the multiplicity of π^* I along the exceptional divisor" (the remark following Definition 47); the chart formula for the birational transform (Hironaka/Algebra/Local/BirationalTransform.lean) applies under ord_Z I ≥ m, which is what needs m ≤ ord_P(I) ⟺ I ≤ Pᵐ for P = ⟨x₀, …, x_r⟩: the symbolic power Pᵐ R_P ∩ R equals the ordinary power Pᵐ.

The route goes through the completion: under the Cohen isomorphism Φ : K⟦X⟧ ≃ R̂ of Hironaka/Algebra/Local/CohenIso.lean (Φ(Xᵢ) = xᵢ) and I R̂ ∩ R = I of Hironaka/Algebra/Local/CompletionCoords.lean, f ∈ Pᵐ iff the series of f has weighted order ≥ m for the weights 1 on X₀, …, X_r and 0 elsewhere — the pure power-series fact ⟨X₀, …, X_r⟩ᵐ = {F | m ≤ weightedOrder F}, proved by induction on m with the division F = ∑ᵢ Xᵢ Gᵢ + F' (F' the monomials free of X₀, …, X_r). Since the weighted order is additive over a field (MvPowerSeries.weightedOrder_mul), s f ∈ Pᵐ with s ∉ P forces f ∈ Pᵐ: Pᵐ is P-primary, so Pᵐ R_P ∩ R = Pᵐ, and m ≤ ord_P I ⟺ I ≤ Pᵐ follows from le_ord_iff in R_P. No associated graded ring is used. Standard commutative algebra, not in the sources in this form; the final equivalence is used for the order along the exceptional divisor in Hironaka/Scheme/IdealSheaf/Order/Exceptional.lean.

The ideal P is chartCenter c.x r = ⟨xᵢ : i ≤ r⟩ of Hironaka/Algebra/Local/BirationalTransform.lean; it is prime by Hironaka/Algebra/Local/RegularSystem.lean.

The power-series fact: ⟨Xᵢ : i ∈ T⟩ᵐ = {F | m ≤ weightedOrder_T F}

@[reducible, inline]

abbrev IsLocalRing.indicatorWeight {n : ℕ} (T : Finset (Fin n)) : Fin n → ℕ

The indicator weights of a set T of variables: 1 on T, 0 elsewhere.

Equations

• IsLocalRing.indicatorWeight T i = if i ∈ T then 1 else 0

theorem IsLocalRing.weight_indicator_eq_zero_iff {n : ℕ} (T : Finset (Fin n)) (d : Fin n →₀ ℕ) : (Finsupp.weight (indicatorWeight T)) d = 0 ↔ ∀ i ∈ T, d i = 0

theorem IsLocalRing.indicatorWeight_le_one {n : ℕ} (T : Finset (Fin n)) (i : Fin n) : indicatorWeight T i ≤ 1

def IsLocalRing.weightedOrderIdeal {K : Type u_1} [CommRing K] {n : ℕ} (w : Fin n → ℕ) (m : ℕ) : Ideal (MvPowerSeries (Fin n) K)

The series of weighted order at least m form an ideal (0 has order ⊤; the order of a sum is at least the minimum; the order of a product is at least the sum).

Equations

• IsLocalRing.weightedOrderIdeal w m = { carrier := {F : MvPowerSeries (Fin n) K | ↑m ≤ MvPowerSeries.weightedOrder w F}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem IsLocalRing.mem_weightedOrderIdeal {K : Type u_1} [CommRing K] {n : ℕ} {w : Fin n → ℕ} {m : ℕ} {F : MvPowerSeries (Fin n) K} : F ∈ weightedOrderIdeal w m ↔ ↑m ≤ MvPowerSeries.weightedOrder w F

theorem IsLocalRing.span_X_le_weightedOrderIdeal_one {K : Type u_1} [CommRing K] {n : ℕ} [Nontrivial K] (T : Finset (Fin n)) : Ideal.span (MvPowerSeries.X '' ↑T) ≤ weightedOrderIdeal (indicatorWeight T) 1

Xᵢ, i ∈ T, has weighted order 1.

theorem IsLocalRing.span_X_pow_le_weightedOrderIdeal {K : Type u_1} [CommRing K] {n : ℕ} [Nontrivial K] (T : Finset (Fin n)) (m : ℕ) : Ideal.span (MvPowerSeries.X '' ↑T) ^ m ≤ weightedOrderIdeal (indicatorWeight T) m

⟨Xᵢ : i ∈ T⟩ᵐ ≤ {F | m ≤ weightedOrder_T F}.

theorem IsLocalRing.mem_span_X_mul_weightedOrderIdeal {K : Type u_1} [CommRing K] {n : ℕ} (T : Finset (Fin n)) (m : ℕ) (T' : Finset (Fin n)) : T' ⊆ T → ∀ (F : MvPowerSeries (Fin n) K), (∀ (d : Fin n →₀ ℕ), (MvPowerSeries.coeff d) F ≠ 0 → m + 1 ≤ (Finsupp.weight (indicatorWeight T)) d ∧ ∃ i ∈ T', d i ≠ 0) → F ∈ Ideal.span (MvPowerSeries.X '' ↑T) * weightedOrderIdeal (indicatorWeight T) m

The division step of the converse, by induction on the set T' of variables that every monomial of F involves: F = X_a G + F' with F' the monomials free of X_a; G keeps weighted order ≥ m when every monomial of F has weight ≥ m + 1.

theorem IsLocalRing.weightedOrderIdeal_le_span_X_pow {K : Type u_1} [CommRing K] {n : ℕ} (T : Finset (Fin n)) (m : ℕ) : weightedOrderIdeal (indicatorWeight T) m ≤ Ideal.span (MvPowerSeries.X '' ↑T) ^ m

{F | m ≤ weightedOrder_T F} ≤ ⟨Xᵢ : i ∈ T⟩ᵐ, by induction on m and the division step.

theorem IsLocalRing.mem_span_X_pow_iff_le_weightedOrder {K : Type u_1} [CommRing K] {n : ℕ} [Nontrivial K] (T : Finset (Fin n)) (m : ℕ) (F : MvPowerSeries (Fin n) K) : F ∈ Ideal.span (MvPowerSeries.X '' ↑T) ^ m ↔ ↑m ≤ MvPowerSeries.weightedOrder (fun (i : Fin n) => if i ∈ T then 1 else 0) F

The power-series fact: ⟨Xᵢ : i ∈ T⟩ᵐ is the set of series all of whose monomials have T-degree at least m.

Transport to R through the Cohen isomorphism

theorem IsLocalRing.isPrime_chartCenter {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (r : Fin n) : (chartCenter x r).IsPrime

P = ⟨x₀, …, x_r⟩ is prime for a regular system of parameters x (isPrime_span_image_lt for the initial segment {j | j.val < r + 1}).

theorem IsLocalRing.cohenEquiv_X {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (i : Fin n) : (cohenEquiv R x hx hn) (MvPowerSeries.X i) = (algebraMap R (AdicCompletion (maximalIdeal R) R)) (x i)

The Cohen isomorphism for the regular system of parameters x: Φ(Xᵢ) = ι(xᵢ).

theorem IsLocalRing.map_chartCenter_pow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (r : Fin n) (m : ℕ) : Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) (chartCenter x r ^ m) = Ideal.map (cohenEquiv R x hx hn) (Ideal.span (MvPowerSeries.X '' ↑{x : Fin n | x ≤ r}) ^ m)

Pᵐ R̂ = Φ(⟨X₀, …, X_r⟩ᵐ).

theorem IsLocalRing.mem_chartCenter_pow_iff_le_weightedOrder' {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (r : Fin n) (f : R) (m : ℕ) : f ∈ chartCenter x r ^ m ↔ ↑m ≤ MvPowerSeries.weightedOrder (indicatorWeight {x : Fin n | x ≤ r}) ((cohenEquiv R x hx hn).symm ((algebraMap R (AdicCompletion (maximalIdeal R) R)) f))

theorem IsLocalRing.mem_chartCenter_pow_iff_le_weightedOrder {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (r : Fin n) (f : R) (m : ℕ) : f ∈ chartCenter x r ^ m ↔ ↑m ≤ MvPowerSeries.weightedOrder (fun (i : Fin n) => if i ≤ r then 1 else 0) ((cohenEquiv R x hx hn).symm ((algebraMap R (AdicCompletion (maximalIdeal R) R)) f))

f ∈ Pᵐ iff the series of f under the Cohen isomorphism has weighted order ≥ m for the weights 1 on X₀, …, X_r and 0 elsewhere — "Pᵐ is the set of series all of whose monomials have x₀, …, x_r-degree at least m".

theorem IsLocalRing.weightedOrder_symm_algebraMap_eq_zero {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (r : Fin n) {s : R} (hs : s ∉ chartCenter x r) : MvPowerSeries.weightedOrder (fun (i : Fin n) => if i ≤ r then 1 else 0) ((cohenEquiv R x hx hn).symm ((algebraMap R (AdicCompletion (maximalIdeal R) R)) s)) = 0

s ∉ P iff the series of s has weighted order 0.

theorem IsLocalRing.mem_chartCenter_pow_of_mul_mem {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (r : Fin n) {s f : R} (hs : s ∉ chartCenter x r) {m : ℕ} (h : s * f ∈ chartCenter x r ^ m) : f ∈ chartCenter x r ^ m

Pᵐ is P-primary — s ∉ P and s f ∈ Pᵐ give f ∈ Pᵐ, because the weighted order is additive (MvPowerSeries.weightedOrder_mul) and that of s is 0.

theorem IsLocalRing.comap_map_localization_chartCenter_pow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (r : Fin n) (m : ℕ) : Ideal.comap (algebraMap R (Localization.AtPrime (chartCenter x r))) (Ideal.map (algebraMap R (Localization.AtPrime (chartCenter x r))) (chartCenter x r ^ m)) = chartCenter x r ^ m

Symbolic equals ordinary power, Pᵐ R_P ∩ R = Pᵐ (P prime by isPrime_chartCenter).

theorem IsLocalRing.le_ordAlong_chartCenter_iff {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (r : Fin n) (I : Ideal R) (m : ℕ) : ↑m ≤ ordAlong (chartCenter x r) I ↔ I ≤ chartCenter x r ^ m

m ≤ ord_P(I) ⟺ I ≤ Pᵐ, with ord_P the order along P (Hironaka/Algebra/Local/Order.lean, ordAlong; Kollár's ord_Z, [Kol07, Definition 47]), computed in R_P (P prime by isPrime_chartCenter).

instance IsLocalRing.RegularCoords.isPrime_chartCenter {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) : (chartCenter c.x r).IsPrime

P = ⟨x₀, …, x_r⟩ is prime for a coordinate structure c: the instance form of isPrime_chartCenter at c.x.