The algebra of one blow-up along a chain stratum

The commutative algebra of the statement CP4 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP4): what happens to a chain form under the blow-up of a chain stratum, stated in a domain R — the local ring 𝒪_{B,q} of the blow-up at a point q of the exceptional divisor — with a fixed element ε, the exceptional coordinate of the chart.

• The ε-orders. After the chart substitution the i-th generator of a chain form is ε^{E_i} · (ε-free part) with E_i = e₀ + ∑_{i' < i} e_{i'} + δ_i (epsOrder), where e₀ and e_i are the ε-orders of the top monomial and of the level monomials, and δ_i ∈ {0, 1} records whether the i-th chain equation is an equation of the centre (span_mul_chainIdeal_pow_eq).
• The division by ε. When every E_i ≥ 1, (ε · A) : (ε) = A in a domain (colon_span_singleton_mul_self), and when moreover (E_i) is non-decreasing — this is where the admissibility condition (★) of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedAdmissibleStratum enters — the telescoping ε^{E_i − 1} = ε^{E_0 − 1} ∏_{i' < i} ε^{E_{i'+1} − E_{i'}} (sum_filter_lt_tsub) exhibits ε⁻¹π^*K as a chain form with the level monomials M'_i = ε^{E_{i+1} − E_i} N_i and the top monomial ε^{E_0 − 1} m₀ (colon_span_mul_chainIdeal_pow; colon_span_mul_chainKIdeal_pow for the K-shape, whose last equation is 1).
• Saturation (the strict transforms): (J : ε^∞) = P for a prime P ∌ ε with J ⊆ P ⊆ (J : ε^t) (iSup_colon_pow_span_singleton_eq_of_isPrime), and (J : ε^∞) = 𝒪 when a power of ε lies in J (iSup_colon_pow_eq_top_of_pow_mem: in the chart of a chain equation f_l the strict transform of Γ is missed).
• Units drop from chain forms (chainIdeal_isUnit_mul: the ratio coordinates of the members whose strict transform misses q).
• Coordinate primes. A monomial in a regular system of parameters lies in the prime (z_k : k ∈ t) iff one of its coordinates with positive exponent is in t (monomialOf_mem_span_image_iff), whence the characterisation of K ≤ Z as the cumulative condition (span_mul_chainKIdeal_le_stratum_iff).
• A chain equation that is a unit makes the un-isolated chain form and the K-shape coincide (chainIdeal_eq_chainKIdeal_of_isUnit).

The chart is that of [Kol07, Definition 60] (the local coordinates in which the blow-up is monomial). The identities are elementary and not taken from the literature; the scheme-level statements are in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP4Chart, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP4NewCoords and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP4.

Monomials

theorem Hironaka.Resolution.monomialOf_mul {R : Type u_1} [CommRing R] {n : ℕ} (u v : Fin n → R) (a : Fin n → ℕ) : monomialOf (fun (k : Fin n) => u k * v k) a = monomialOf u a * monomialOf v a

A monomial in a pointwise product of two coordinate families is the product of the monomials.

theorem Hironaka.Resolution.monomialOf_ite_mem {R : Type u_1} [CommRing R] {n : ℕ} (ε : R) (C : Finset (Fin n)) (a : Fin n → ℕ) : monomialOf (fun (k : Fin n) => if k ∈ C then ε else 1) a = ε ^ ∑ k ∈ C, a k

The monomial in the family which is ε on C and 1 off C is ε to the total exponent on C.

theorem Hironaka.Resolution.isUnit_monomialOf {R : Type u_1} [CommRing R] {n : ℕ} {u : Fin n → R} (hu : ∀ (k : Fin n), IsUnit (u k)) (a : Fin n → ℕ) : IsUnit (monomialOf u a)

A monomial in units is a unit.

theorem Hironaka.Resolution.isUnit_prod_of_forall_isUnit {R : Type u_1} [CommRing R] {ι : Type u_2} (s : Finset ι) {u : ι → R} (hu : ∀ (i : ι), IsUnit (u i)) : IsUnit (∏ i ∈ s, u i)

A product of units is a unit.

Chain generators after the chart substitution

theorem Hironaka.Resolution.span_singleton_mul_span_range {R : Type u_1} [CommRing R] {ι : Type u_2} (x : R) (g : ι → R) : Ideal.span {x} * Ideal.span (Set.range g) = Ideal.span (Set.range fun (i : ι) => x * g i)

span {x} · span (range g) = span (range (x · g)).

theorem Hironaka.Resolution.chainIdeal_isUnit_mul {R : Type u_1} [CommRing R] {r : ℕ} (φ M : Fin r → R) {u : Fin r → R} (hu : ∀ (i : Fin r), IsUnit (u i)) : (chainIdeal φ fun (i : Fin r) => u i * M i) = chainIdeal φ M

Units multiplying the level monomials do not change the chain ideal.

theorem Hironaka.Resolution.chainKIdeal_isUnit_mul {R : Type u_1} [CommRing R] {r : ℕ} (φ M : Fin (r + 1) → R) {u : Fin (r + 1) → R} (hu : ∀ (i : Fin (r + 1)), IsUnit (u i)) : (chainKIdeal φ fun (i : Fin (r + 1)) => u i * M i) = chainKIdeal φ M

Units multiplying the level monomials do not change the K-shape.

theorem Hironaka.Resolution.chainGen_pow_mul {R : Type u_1} [CommRing R] {r : ℕ} (ε : R) (δ e : Fin r → ℕ) (φ N : Fin r → R) (i : Fin r) : chainGen (fun (i : Fin r) => ε ^ δ i * φ i) (fun (i : Fin r) => ε ^ e i * N i) i = ε ^ (∑ i' : Fin r with i' < i, e i' + δ i) * chainGen φ N i

The i-th chain generator after the substitution f_i ↦ ε^{δ_i} φ_i, M_i ↦ ε^{e_i} N_i carries ε to the power ∑_{i' < i} e_{i'} + δ_i.

theorem Hironaka.Resolution.chainGen_pow_mul_left {R : Type u_1} [CommRing R] {r : ℕ} (ε : R) (e : Fin r → ℕ) (φ N : Fin r → R) (i : Fin r) : chainGen φ (fun (i : Fin r) => ε ^ e i * N i) i = (ε ^ ∑ i' : Fin r with i' < i, e i') * chainGen φ N i

The i-th chain generator with level monomials ε^{e_i} N_i carries ε^{∑_{i' < i} e_{i'}}.

def Hironaka.Resolution.epsOrder {r : ℕ} (e₀ : ℕ) (e δ : Fin r → ℕ) (i : Fin r) : ℕ

The ε-order E_i = e₀ + ∑_{i' < i} e_{i'} + δ_i of the i-th pulled-back chain generator (e₀ the ε-order of the top monomial, e_{i'} those of the level monomials, δ_i that of the i-th chain equation).

Equations

• Hironaka.Resolution.epsOrder e₀ e δ i = e₀ + ∑ i' : Fin r with i' < i, e i' + δ i

theorem Hironaka.Resolution.span_mul_chainIdeal_pow_eq {R : Type u_1} [CommRing R] {r : ℕ} (ε m₀ : R) (e₀ : ℕ) (δ e : Fin r → ℕ) (φ N : Fin r → R) : (Ideal.span {ε ^ e₀ * m₀} * chainIdeal (fun (i : Fin r) => ε ^ δ i * φ i) fun (i : Fin r) => ε ^ e i * N i) = Ideal.span (Set.range fun (i : Fin r) => ε ^ epsOrder e₀ e δ i * (m₀ * chainGen φ N i))

The pulled-back chain form is generated by ε^{E_i} · m₀ · (∏_{i' < i} N_{i'}) φ_i.

theorem Hironaka.Resolution.colon_span_singleton_mul_self {R : Type u_1} [CommRing R] [IsDomain R] {ε : R} (hε : ε ≠ 0) (J : Ideal R) : Submodule.colon (Ideal.span {ε} * J) ↑(Ideal.span {ε}) = J

In a domain, (ε · J) : (ε) = J for ε ≠ 0.

theorem Hironaka.Resolution.sum_filter_lt_tsub {r : ℕ} (E D : Fin (r + 1) → ℕ) (hmono : ∀ (i : Fin r), E i.castSucc ≤ E i.succ) (hD : ∀ (i : Fin r), D i.castSucc = E i.succ - E i.castSucc) (i : Fin (r + 1)) : ∑ i' : Fin (r + 1) with i' < i, D i' = E i - E 0

The telescoping sum of the increments of a non-decreasing sequence on Fin (r + 1).

theorem Hironaka.Resolution.zero_le_of_forall_castSucc_le_succ {r : ℕ} (E : Fin (r + 1) → ℕ) (hmono : ∀ (i : Fin r), E i.castSucc ≤ E i.succ) (i : Fin (r + 1)) : E 0 ≤ E i

A non-decreasing sequence on Fin (r + 1) is bounded below by its first value.

theorem Hironaka.Resolution.colon_span_mul_chainIdeal_pow {R : Type u_1} [CommRing R] {r : ℕ} [IsDomain R] {ε : R} (hε : ε ≠ 0) (m₀ : R) (e₀ : ℕ) (δ e : Fin (r + 1) → ℕ) (φ N : Fin (r + 1) → R) (hpos : 1 ≤ epsOrder e₀ e δ 0) (hmono : ∀ (i : Fin r), epsOrder e₀ e δ i.castSucc ≤ epsOrder e₀ e δ i.succ) (D : Fin (r + 1) → ℕ) (hD : ∀ (i : Fin r), D i.castSucc = epsOrder e₀ e δ i.succ - epsOrder e₀ e δ i.castSucc) : Submodule.colon (Ideal.span {ε ^ e₀ * m₀} * chainIdeal (fun (i : Fin (r + 1)) => ε ^ δ i * φ i) fun (i : Fin (r + 1)) => ε ^ e i * N i) ↑(Ideal.span {ε}) = Ideal.span {ε ^ (epsOrder e₀ e δ 0 - 1) * m₀} * chainIdeal φ fun (i : Fin (r + 1)) => ε ^ D i * N i

The division by ε, the algebraic core of CP4: in a domain, when the ε-orders E_i of the pulled-back chain generators are ≥ 1 and non-decreasing (the content of the admissibility condition (★)), the colon by (ε) of the pulled-back chain form is again a chain form: the same equations φ, level monomials ε^{E_{i+1} − E_i} N_i (recorded as D) and top monomial ε^{E_0 − 1} m₀ — the telescoping ε^{E_i − 1} = ε^{E_0 − 1} ∏_{i' < i} ε^{E_{i'+1} − E_{i'}}.

theorem Hironaka.Resolution.update_pow_mul_last {R : Type u_1} [CommRing R] {r : ℕ} (ε : R) (δ : Fin (r + 1) → ℕ) (φ : Fin (r + 1) → R) : Function.update (fun (i : Fin (r + 1)) => ε ^ δ i * φ i) (Fin.last r) 1 = fun (i : Fin (r + 1)) => ε ^ Function.update δ (Fin.last r) 0 i * Function.update φ (Fin.last r) 1 i

The K-shape substitution: the last equation 1 is untouched.

theorem Hironaka.Resolution.colon_span_mul_chainKIdeal_pow {R : Type u_1} [CommRing R] {r : ℕ} [IsDomain R] {ε : R} (hε : ε ≠ 0) (m₀ : R) (e₀ : ℕ) (δ e : Fin (r + 1) → ℕ) (φ N : Fin (r + 1) → R) (hpos : 1 ≤ epsOrder e₀ e (Function.update δ (Fin.last r) 0) 0) (hmono : ∀ (i : Fin r), epsOrder e₀ e (Function.update δ (Fin.last r) 0) i.castSucc ≤ epsOrder e₀ e (Function.update δ (Fin.last r) 0) i.succ) (D : Fin (r + 1) → ℕ) (hD : ∀ (i : Fin r), D i.castSucc = epsOrder e₀ e (Function.update δ (Fin.last r) 0) i.succ - epsOrder e₀ e (Function.update δ (Fin.last r) 0) i.castSucc) : Submodule.colon (Ideal.span {ε ^ e₀ * m₀} * chainKIdeal (fun (i : Fin (r + 1)) => ε ^ δ i * φ i) fun (i : Fin (r + 1)) => ε ^ e i * N i) ↑(Ideal.span {ε}) = Ideal.span {ε ^ (epsOrder e₀ e (Function.update δ (Fin.last r) 0) 0 - 1) * m₀} * chainKIdeal φ fun (i : Fin (r + 1)) => ε ^ D i * N i

The division by ε for the K-shape: the colon by (ε) of the pulled-back K-shape is the K-shape with the new monomials, the ε-orders being those with δ_r = 0 for the last generator (which carries no equation).

Saturation by a coordinate

theorem Hironaka.Resolution.iSup_colon_pow_span_singleton_eq_of_isPrime {R : Type u_1} [CommRing R] {J P : Ideal R} (hP : P.IsPrime) {ε : R} (hε : ε ∉ P) (hJP : J ≤ P) {t : ℕ} (hPJ : ∀ x ∈ P, x * ε ^ t ∈ J) : ⨆ (i : ℕ), Submodule.colon J ↑(Ideal.span {ε} ^ i) = P

(J : ε^∞) = P for a prime P ∌ ε with J ⊆ P and P · ε^t ⊆ J: the strict transform of a coordinate subspace through the centre.

theorem Hironaka.Resolution.iSup_colon_pow_eq_top_of_pow_mem {R : Type u_1} [CommRing R] {J : Ideal R} {ε : R} {t : ℕ} (hJ : ε ^ t ∈ J) : ⨆ (i : ℕ), Submodule.colon J ↑(Ideal.span {ε} ^ i) = ⊤

(J : ε^∞) = 𝒪 when a power of ε lies in J (the charts of the chain equations f_l, where the exceptional coordinate is a pulled-back equation of the strict transform's centre).

theorem Hironaka.Resolution.iSup_colon_pow_span_singleton_mul_pow {R : Type u_1} [CommRing R] {w ε : R} (hw : Prime w) (hε : ε ∉ Ideal.span {w}) (t : ℕ) : ⨆ (i : ℕ), Submodule.colon (Ideal.span {w * ε ^ t}) ↑(Ideal.span {ε} ^ i) = Ideal.span {w}

((w ε^t) : ε^∞) = (w) for a prime element w not dividing ε (the strict transform of a member through the centre).

Monomials in coordinate primes

theorem Hironaka.Resolution.monomialOf_mem_span_image_iff {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.maximalIdeal R = Ideal.span (Set.range z)) (hn : ↑n = ringKrullDim R) (t : Finset (Fin n)) (a : Fin n → ℕ) : monomialOf z a ∈ Ideal.span (z '' ↑t) ↔ ∃ k ∈ t, a k ≠ 0

A monomial in a regular system of parameters lies in the coordinate prime (z_k : k ∈ t) iff one of its coordinates with positive exponent lies in t.

theorem Hironaka.Resolution.monomialOf_mem_span_image_union_iff {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.maximalIdeal R = Ideal.span (Set.range z)) (hn : ↑n = ringKrullDim R) {r : ℕ} {σ : Fin (r + 1) → Fin n} (T : Finset (Fin (r + 1))) (s : Finset (Fin n)) {a : Fin n → ℕ} (ha : ∀ (k : Fin n), a k ≠ 0 → k ∉ Set.range σ) : monomialOf z a ∈ Ideal.span (z '' ↑(Finset.image σ T ∪ s)) ↔ monomialOf z a ∈ Ideal.span (z '' ↑s)

A monomial supported off the range of σ lies in the coordinate prime of σ '' T ∪ s iff it lies in the coordinate prime of s.

theorem Hironaka.Resolution.span_mul_chainKIdeal_le_stratum_iff {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.IsRegularSystemOfParameters z) {r : ℕ} (σ : Fin (r + 1) → Fin n) (hσ : Function.Injective σ) (s : Finset (Fin n)) (hs : ∀ (i : Fin (r + 1)), σ i ∉ s) (b : Fin n → ℕ) (a : Fin (r + 1) → Fin n → ℕ) (hb : ∀ (k : Fin n), b k ≠ 0 → k ∉ Set.range σ) (ha : ∀ (i : Fin (r + 1)) (k : Fin n), a i k ≠ 0 → k ∉ Set.range σ) {l : ℕ} (hl : l ≤ r) : (Ideal.span {monomialOf z b} * chainKIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) ≤ Ideal.span (z ∘ σ '' {i : Fin (r + 1) | ↑i < l}) ⊔ Ideal.span (z '' ↑s) ↔ monomialOf z b * ∏ i : Fin (r + 1) with ↑i < l, monomialOf z (a i) ∈ Ideal.span (z '' ↑s)

The characterisation of K ≤ Z: the K-shape lies in the ideal of the chain stratum iff the monomial M⁰ · M₀ ⋯ M_{l−1} lies in (z_s) — the CUMULATIVE condition, weaker than the admissibility condition (★) and not automatic; (★) implies it.

The ε-orders of an admissible or terminal-normal stratum

def Hironaka.Resolution.stratumCoords {n r : ℕ} (σ : Fin (r + 1) → Fin n) (s : Finset (Fin n)) (l : ℕ) : Finset (Fin n)

The coordinates of the chain stratum (f_i : i < l) + (e_j : j ∈ s).

Equations

• Hironaka.Resolution.stratumCoords σ s l = Finset.image σ {i : Fin (r + 1) | ↑i < l} ∪ s

theorem Hironaka.Resolution.mem_stratumCoords_iff {n r : ℕ} (σ : Fin (r + 1) → Fin n) (s : Finset (Fin n)) (hσ : Function.Injective σ) (hs : ∀ (i : Fin (r + 1)), σ i ∉ s) (l : ℕ) (i : Fin (r + 1)) : σ i ∈ stratumCoords σ s l ↔ ↑i < l

A chain coordinate lies among the stratum's coordinates iff its level is below l.

theorem Hironaka.Resolution.sum_stratumCoords_eq {n r : ℕ} (σ : Fin (r + 1) → Fin n) (s : Finset (Fin n)) (l : ℕ) (c : Fin n → ℕ) (hc : ∀ (k : Fin n), c k ≠ 0 → k ∉ Set.range σ) : ∑ k ∈ stratumCoords σ s l, c k = ∑ k ∈ s, c k

The total exponent over the stratum's coordinates of an exponent vector supported off the chain is its total exponent over s.

theorem Hironaka.Resolution.span_image_comp_sup_eq {n r : ℕ} (σ : Fin (r + 1) → Fin n) (s : Finset (Fin n)) {R : Type u_1} [CommRing R] (z : Fin n → R) (l : ℕ) : Ideal.span (z ∘ σ '' {i : Fin (r + 1) | ↑i < l}) ⊔ Ideal.span (z '' ↑s) = Ideal.span (z '' ↑(stratumCoords σ s l))

The stratum's ideal is the coordinate prime of its coordinates.

theorem Hironaka.Resolution.epsOrder_zero {r : ℕ} (e₀ : ℕ) (e δ : Fin (r + 1) → ℕ) : epsOrder e₀ e δ 0 = e₀ + δ 0

The ε-order of the i-th generator, unfolded at 0.

theorem Hironaka.Resolution.epsOrder_succ {r : ℕ} (e₀ : ℕ) (e δ : Fin (r + 1) → ℕ) (i : Fin r) : epsOrder e₀ e δ i.succ + δ i.castSucc = epsOrder e₀ e δ i.castSucc + e i.castSucc + δ i.succ

The ε-orders of consecutive generators differ by e_i + δ_{i+1} − δ_i.

theorem Hironaka.Resolution.epsOrder_mono_of {r : ℕ} (e₀ : ℕ) (e δ : Fin (r + 1) → ℕ) (h : ∀ (i : Fin r), δ i.castSucc ≤ e i.castSucc + δ i.succ) (i : Fin r) : epsOrder e₀ e δ i.castSucc ≤ epsOrder e₀ e δ i.succ

Monotonicity of the ε-orders from the level condition δ_i ≤ e_i + δ_{i+1}.

A chain equation that is a unit

theorem Hironaka.Resolution.prod_filter_lt_last_eq_mul {R : Type u_1} [CommRing R] {r : ℕ} (M : Fin (r + 1) → R) (i₀ : Fin (r + 1)) : ∏ i : Fin (r + 1) with i < Fin.last r, M i = (∏ i : Fin (r + 1) with i < i₀, M i) * ∏ i : Fin (r + 1) with i < Fin.last r ∧ ¬i < i₀, M i

The monomial ∏_{i < r} M_i of the K-shape's last generator is a multiple of the monomial ∏_{i < i₀} M_i of any earlier generator.

theorem Hironaka.Resolution.chainIdeal_eq_chainKIdeal_of_isUnit {R : Type u_1} [CommRing R] {r : ℕ} (φ M : Fin (r + 1) → R) {i₀ : Fin (r + 1)} (hu : IsUnit (φ i₀)) : chainIdeal φ M = chainKIdeal φ M

When one of the chain equations is a unit, the un-isolated chain form and the K-shape coincide — both are generated by the generators below that level and the monomial of that level.