The colon of a chain ideal by its chain

For a chain f₀, …, f_r and monomials M₀, …, M_{r−1} in a commutative ring, the chain ideal I = (f₀, M₀ f₁, …, (M₀ ⋯ M_{r−1}) f_r) (chainIdeal) and the K-shape K = (f₀, M₀ f₁, …, (M₀ ⋯ M_{r−2}) f_{r−1}, M₀ ⋯ M_{r−1}) (chainKIdeal; Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) satisfy K ⊆ I : (f) always (chainKIdeal_le_colon) and I : (f) = K under two cancellation clauses at every level i < r, with S_i := (f₀, …, f_i) (colon_chainIdeal_eq_chainKIdeal):

• (C) M_i is a nonzerodivisor modulo S_i: M_i y ∈ S_i → y ∈ S_i;
• (B) M_i cancels against the later chain equations modulo S_i: for j > i, x f_j ∈ S_i + (M_i) → x ∈ S_i + (M_i).

The proof is an induction on r through the quotient by f₀: I = (f₀) + M₀ I' and K = (f₀) + M₀ K' with I', K' the chain ideal and the K-shape of the tail (chainIdeal_succ, chainKIdeal_succ); from h f_j ∈ I for j ≥ 1 clause (B) at level 0 gives h = c f₀ + M₀ h', clause (C) at level 0 gives h' f_j ∈ (f₀) + I', so the class of h' lies in the colon of the tail's chain ideal in R/(f₀), which is the tail's K-shape by induction, and h ∈ (f₀) + M₀ K'. The clauses (B), (C) hold for the chain coordinates of a regular system of parameters and monomials in the remaining coordinates (Hironaka.Resolution.Algebraic.Wlo05.ChainIdealColonRegular), which is the statement CP2 of the embedded desingularization: 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 identity is elementary and not taken from the literature.

The generators and the two decompositions

def Hironaka.Resolution.chainGen {R : Type u} [CommRing R] {r : ℕ} (f M : Fin r → R) (i : Fin r) : R

The i-th generator (∏_{i' < i} M_{i'}) f_i of the chain ideal.

Equations

• Hironaka.Resolution.chainGen f M i = (∏ i' : Fin r with i' < i, M i') * f i

theorem Hironaka.Resolution.chainIdeal_eq_span_range_chainGen {R : Type u} [CommRing R] {r : ℕ} (f M : Fin r → R) : chainIdeal f M = Ideal.span (Set.range (chainGen f M))

theorem Hironaka.Resolution.chainGen_mem {R : Type u} [CommRing R] {r : ℕ} (f M : Fin r → R) (i : Fin r) : chainGen f M i ∈ chainIdeal f M

theorem Hironaka.Resolution.chainGen_zero {R : Type u} [CommRing R] {r : ℕ} (f M : Fin (r + 1) → R) : chainGen f M 0 = f 0

theorem Hironaka.Resolution.prod_filter_lt_succ {R : Type u} [CommRing R] {r : ℕ} (M : Fin (r + 2) → R) (j : Fin (r + 1)) : ∏ i' : Fin (r + 2) with i' < j.succ, M i' = M 0 * ∏ i' : Fin (r + 1) with i' < j, M i'.succ

theorem Hironaka.Resolution.chainGen_succ {R : Type u} [CommRing R] {r : ℕ} (f M : Fin (r + 2) → R) (j : Fin (r + 1)) : chainGen f M j.succ = M 0 * chainGen (Fin.tail f) (Fin.tail M) j

theorem Hironaka.Resolution.chainIdeal_succ {R : Type u} [CommRing R] {r : ℕ} (f M : Fin (r + 2) → R) : chainIdeal f M = Ideal.span {f 0} ⊔ Ideal.span {M 0} * chainIdeal (Fin.tail f) (Fin.tail M)

The chain ideal of f₀, …, f_{r+1} is (f₀) + M₀ · (chain ideal of the tail).

theorem Hironaka.Resolution.chainKIdeal_succ {R : Type u} [CommRing R] {r : ℕ} (f M : Fin (r + 2) → R) : chainKIdeal f M = Ideal.span {f 0} ⊔ Ideal.span {M 0} * chainKIdeal (Fin.tail f) (Fin.tail M)

The K-shape of f₀, …, f_{r+1} is (f₀) + M₀ · (K-shape of the tail).

theorem Hironaka.Resolution.chainKIdeal_zero {R : Type u} [CommRing R] (f M : Fin 1 → R) : chainKIdeal f M = ⊤

The K-shape of a chain of length one is the unit ideal.

The colon by the chain

theorem Hironaka.Resolution.mem_colon_span_range_iff {R : Type u} [CommRing R] {ι : Type u_1} (I : Ideal R) (f : ι → R) (x : R) : x ∈ Submodule.colon I ↑(Ideal.span (Set.range f)) ↔ ∀ (j : ι), x * f j ∈ I

Membership in the colon by the ideal of a family: x ∈ I : (f) ↔ ∀ j, x f_j ∈ I.

theorem Hironaka.Resolution.chainKIdeal_le_colon {R : Type u} [CommRing R] {r : ℕ} (f M : Fin (r + 1) → R) : chainKIdeal f M ≤ Submodule.colon (chainIdeal f M) ↑(Ideal.span (Set.range f))

The K-shape lies in the colon of the chain ideal by the chain (no hypotheses).

The two clauses and the identity

theorem Hironaka.Resolution.image_le_zero {R : Type u} {r : ℕ} (f : Fin (r + 1) → R) : f '' {j : Fin (r + 1) | ↑j ≤ 0} = {f 0}

The image of the chain under an initial segment {j ≤ 0} is {f₀}.

theorem Hironaka.Resolution.image_le_succ {R : Type u} {r : ℕ} (f : Fin (r + 2) → R) (i : ℕ) : f '' {j : Fin (r + 2) | ↑j ≤ i + 1} = insert (f 0) (Fin.tail f '' {j : Fin (r + 1) | ↑j ≤ i})

The image of the chain under {j ≤ i + 1} is f₀ together with the tail's image under {j ≤ i}.

theorem Hironaka.Resolution.chainIdeal_comp {R : Type u} [CommRing R] {S : Type u} [CommRing S] (φ : R →+* S) {r : ℕ} (f M : Fin r → R) : chainIdeal (⇑φ ∘ f) (⇑φ ∘ M) = Ideal.map φ (chainIdeal f M)

The chain ideal is compatible with ring homomorphisms.

theorem Hironaka.Resolution.chainKIdeal_comp {R : Type u} [CommRing R] {S : Type u} [CommRing S] (φ : R →+* S) {r : ℕ} (f M : Fin (r + 1) → R) : chainKIdeal (⇑φ ∘ f) (⇑φ ∘ M) = Ideal.map φ (chainKIdeal f M)

The K-shape is compatible with ring homomorphisms.

theorem Hironaka.Resolution.colon_chainIdeal_eq_chainKIdeal (r : ℕ) (R : Type u) [CommRing R] (f M : Fin (r + 1) → R) : (∀ (i : Fin r) (y : R), M i.castSucc * y ∈ Ideal.span (f '' {j : Fin (r + 1) | ↑j ≤ ↑i}) → y ∈ Ideal.span (f '' {j : Fin (r + 1) | ↑j ≤ ↑i})) → (∀ (i : Fin r) (j : Fin (r + 1)), ↑i < ↑j → ∀ (x : R), x * f j ∈ Ideal.span (f '' {j' : Fin (r + 1) | ↑j' ≤ ↑i}) ⊔ Ideal.span {M i.castSucc} → x ∈ Ideal.span (f '' {j' : Fin (r + 1) | ↑j' ≤ ↑i}) ⊔ Ideal.span {M i.castSucc}) → Submodule.colon (chainIdeal f M) ↑(Ideal.span (Set.range f)) = chainKIdeal f M

The algebraic core of CP2: under the two cancellation clauses at every level, the colon of the chain ideal by the chain is the K-shape.