The colon of the chain ideal by the chain in a regular local ring

For a regular system of parameters z of a regular local ring R, chain equations f = z ∘ σ (σ injective) and monomials M_i = ∏_k z_k^{a_{ik}} in the OTHER coordinates (a_{ik} = 0 for k in the range of σ), the two cancellation clauses of Hironaka.Resolution.Algebraic.Wlo05.ChainIdealColon hold at every level, so (chainIdeal f M) : (f) = chainKIdeal f M (chainIdeal_colon_span_eq), and with a top-level monomial factor M⁰ in the other coordinates (M⁰ · chainIdeal f M) : (f) = M⁰ · chainKIdeal f M (chainIdeal_colon_span_eq'). This is the statement CP2 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative): the isolated ideal I_n : I_{Γ̃} at the absorbing stage has the K-shape — for example (x, e a, e² y) : (x, a, y) = (x, e a, e²).

The clauses come from the parameter-subset facts of Hironaka.Scheme.Snc.ParameterSubset: the ideal (z_l : l ∈ s) of a sub-family is prime (the quotient is regular local, hence a domain), a coordinate outside s is not in it, and in R/(z_l : l ∈ s) the class of a coordinate z_k, k ∉ s, is a prime element (the quotient by it is R/(z_l : l ∈ insert k s), again a domain). The cancellation of a monomial against a later chain equation is then Mathlib's Prime.pow_dvd_of_dvd_mul_right, one prime power at a time, cancelling each power in the domain before the next (dvd_of_prod_pow_dvd_mul). The colon identity is used at the entry into the protected state (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainColon) and in the analysis of the last round (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Tools).

Cancellation of a monomial in a domain

theorem Hironaka.Resolution.dvd_of_prod_pow_dvd_mul {R : Type u_1} [CommRing R] [IsDomain R] {ι : Type u_2} (K : Finset ι) (p : ι → R) (a : ι → ℕ) (u : R) (hp : ∀ k ∈ K, a k ≠ 0 → Prime (p k) ∧ ¬p k ∣ u) (x : R) : ∏ k ∈ K, p k ^ a k ∣ x * u → ∏ k ∈ K, p k ^ a k ∣ x

In a domain, a product of prime powers ∏ p_k^{a_k} dividing x u, where no p_k with a_k ≠ 0 divides u, divides x — one power at a time (Prime.pow_dvd_of_dvd_mul_right), cancelling it before the next.

The classes of the coordinates in a quotient by a sub-family are prime

theorem Hironaka.Resolution.isDomain_quotient_span_image_finset {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) (s : Finset (Fin n)) : IsDomain (R ⧸ Ideal.span (z '' ↑s))

The quotient of a regular local ring by a sub-family of a regular system of parameters is a domain (AlgebraicGeometry.isRegularLocalRing_quotient_span_image_finset).

theorem Hironaka.Resolution.isPrime_span_image_finset {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) (s : Finset (Fin n)) : (Ideal.span (z '' ↑s)).IsPrime

The ideal of a sub-family of a regular system of parameters is prime.

theorem Hironaka.Resolution.prime_mk_of_notMem {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) (s : Finset (Fin n)) {k : Fin n} (hk : k ∉ s) : Prime ((Ideal.Quotient.mk (Ideal.span (z '' ↑s))) (z k))

In R/(z_l : l ∈ s) the class of a coordinate z_k, k ∉ s, is a prime element: the quotient by it is R/(z_l : l ∈ insert k s), a domain, and the class is nonzero.

The top-level monomial factor

theorem Hironaka.Resolution.colon_span_singleton_mul_eq {R : Type u_1} [CommRing R] [IsDomain R] {ι : Type u_2} [Nonempty ι] (m : R) (hm0 : m ≠ 0) (f : ι → R) (I : Ideal R) (hm : ∀ (j : ι) (x : R), m ∣ x * f j → m ∣ x) : Submodule.colon (Ideal.span {m} * I) ↑(Ideal.span (Set.range f)) = Ideal.span {m} * Submodule.colon I ↑(Ideal.span (Set.range f))

In a domain, for m ≠ 0 that cancels against every f_j (m ∣ x f_j → m ∣ x), the colon of m · I by (f) is m · (I : (f)) (the family f nonempty).

theorem Hironaka.Resolution.monomialOf_ne_zero {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) (b : Fin n → ℕ) : monomialOf z b ≠ 0

A monomial in the coordinates is nonzero.

theorem Hironaka.Resolution.monomialOf_dvd_of_dvd_mul {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} (b : Fin n → ℕ) (hb : ∀ k ∈ Set.range σ, b k = 0) (j : Fin (r + 1)) (x : R) (h : monomialOf z b ∣ x * z (σ j)) : monomialOf z b ∣ x

A monomial in coordinates off the range of σ cancels against every z (σ j).

The colon identity (CP2)

def Hironaka.Resolution.chainSeg {n r : ℕ} (σ : Fin (r + 1) → Fin n) (i : ℕ) : Finset (Fin n)

The coordinate indices of the chain segment f₀, …, f_i.

Equations

• Hironaka.Resolution.chainSeg σ i = Finset.image σ {j : Fin (r + 1) | ↑j ≤ i}

theorem Hironaka.Resolution.mem_chainSeg_iff {n r : ℕ} {σ : Fin (r + 1) → Fin n} {i : ℕ} {k : Fin n} : k ∈ chainSeg σ i ↔ ∃ (j : Fin (r + 1)), ↑j ≤ i ∧ σ j = k

theorem Hironaka.Resolution.image_comp_le_eq {R : Type u_1} {n r : ℕ} (z : Fin n → R) (σ : Fin (r + 1) → Fin n) (i : ℕ) : z ∘ σ '' {j : Fin (r + 1) | ↑j ≤ i} = z '' ↑(chainSeg σ i)

theorem Hironaka.Resolution.monomialOf_notMem_span_chainSeg {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} {r : ℕ} {σ : Fin (r + 1) → Fin n} {a : Fin (r + 1) → Fin n → ℕ} (ha : ∀ (i : Fin (r + 1)), ∀ k ∈ Set.range σ, a i k = 0) (hz' : IsLocalRing.maximalIdeal R = Ideal.span (Set.range z)) (hn : ↑n = ringKrullDim R) (i : Fin (r + 1)) (l : ℕ) : monomialOf z (a i) ∉ Ideal.span (z '' ↑(chainSeg σ l))

A monomial in the coordinates off the chain is not in the ideal of a chain segment.

theorem Hironaka.Resolution.clauseC {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} {r : ℕ} {σ : Fin (r + 1) → Fin n} {a : Fin (r + 1) → Fin n → ℕ} (ha : ∀ (i : Fin (r + 1)), ∀ k ∈ Set.range σ, a i k = 0) (hz' : IsLocalRing.maximalIdeal R = Ideal.span (Set.range z)) (hn : ↑n = ringKrullDim R) (i : Fin r) (y : R) (hy : monomialOf z (a i.castSucc) * y ∈ Ideal.span (z ∘ σ '' {j : Fin (r + 1) | ↑j ≤ ↑i})) : y ∈ Ideal.span (z ∘ σ '' {j : Fin (r + 1) | ↑j ≤ ↑i})

Clause (C) of Hironaka.Resolution.Algebraic.Wlo05.ChainIdealColon for chain coordinates: a monomial off the chain is a nonzerodivisor modulo a chain segment.

theorem Hironaka.Resolution.clauseB {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} {r : ℕ} {σ : Fin (r + 1) → Fin n} (hσ : Function.Injective σ) {a : Fin (r + 1) → Fin n → ℕ} (ha : ∀ (i : Fin (r + 1)), ∀ k ∈ Set.range σ, a i k = 0) (hz' : IsLocalRing.maximalIdeal R = Ideal.span (Set.range z)) (hn : ↑n = ringKrullDim R) (i : Fin r) (j : Fin (r + 1)) (hij : ↑i < ↑j) (x : R) (hx : x * (z ∘ σ) j ∈ Ideal.span (z ∘ σ '' {j' : Fin (r + 1) | ↑j' ≤ ↑i}) ⊔ Ideal.span {monomialOf z (a i.castSucc)}) : x ∈ Ideal.span (z ∘ σ '' {j' : Fin (r + 1) | ↑j' ≤ ↑i}) ⊔ Ideal.span {monomialOf z (a i.castSucc)}

Clause (B) of Hironaka.Resolution.Algebraic.Wlo05.ChainIdealColon for chain coordinates: a monomial off the chain cancels against a later chain equation modulo a chain segment.

theorem Hironaka.Resolution.chainIdeal_colon_span_eq {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 σ) {a : Fin (r + 1) → Fin n → ℕ} (ha : ∀ (i : Fin (r + 1)), ∀ k ∈ Set.range σ, a i k = 0) : Submodule.colon (chainIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) ↑(Ideal.span (Set.range (z ∘ σ))) = chainKIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)

CP2, the colon identity: in a regular local ring with a regular system of parameters z, for chain equations f = z ∘ σ and monomials M_i = ∏_k z_k^{a_{ik}} in the coordinates off the chain, the colon of the chain ideal by the chain is the K-shape: (f₀, M₀ f₁, …, (∏_{i<r} M_i) f_r) : (f₀, …, f_r) = (f₀, M₀ f₁, …, ∏_{i<r} M_i).

theorem Hironaka.Resolution.chainIdeal_colon_span_eq' {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 σ) {a : Fin (r + 1) → Fin n → ℕ} (ha : ∀ (i : Fin (r + 1)), ∀ k ∈ Set.range σ, a i k = 0) (b : Fin n → ℕ) (hb : ∀ k ∈ Set.range σ, b k = 0) : Submodule.colon (Ideal.span {monomialOf z b} * chainIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) ↑(Ideal.span (Set.range (z ∘ σ))) = Ideal.span {monomialOf z b} * chainKIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)

CP2 with the top-level monomial factor: for a top-level monomial M⁰ = ∏_k z_k^{b_k} in the coordinates off the chain, (M⁰ · chainIdeal f M) : (f) = M⁰ · chainKIdeal f M.