The intersection form of a chain ideal

In a regular local ring R with a regular system of parameters z, chain equations f = z ∘ σ (part of the parameters) and monomials M_i = ∏_k z_k^{a_{ik}} in the coordinates OFF the chain, the chain ideal I(f; a) = (f₀, M₀ f₁, …, (∏_{i<r} M_i) f_r) is the intersection of the chain's prime (f) with the K-shape K(f; a) = (f₀, M₀ f₁, …, ∏_{i<r} M_i) (chainIdeal_eq_span_inf_chainKIdeal) — the counterpart of the colon identity of Hironaka.Resolution.Algebraic.Wlo05.ChainIdealColonRegular (chainIdeal_colon_span_eq), and the algebra behind the un-isolated ideal I_Γ ⊓ K in the statement CP6 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative): the ideal of the loop near an isolated component is recovered from the isolated ideal K and the component's ideal.

The proof is an induction on the length of the chain through the quotient by f₀, as for the colon, with the single algebraic input that every monomial M_i is a nonzerodivisor modulo the chain's prime — a monomial in parameters outside a coordinate prime lies outside it (monomialOf_notMem_span_chainSeg, isPrime_span_image_finset). The pure form chainIdeal_eq_span_inf_chainKIdeal_of_cancel isolates that input as a hypothesis over any commutative ring; cancel_monomialOf_span_range supplies it in the regular local ring; span_mul_chainIdeal_eq_span_inf is the form with the top-level monomial M⁰, through P ∩ mA = m (P ∩ A) for m a product of parameters outside the prime P. The identities are used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP4Sheaf and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Tools.

Chain ideals over any commutative ring

theorem Hironaka.Resolution.chainIdeal_le_chainKIdeal {R : Type u} [CommRing R] {r : ℕ} (f M : Fin (r + 1) → R) : chainIdeal f M ≤ chainKIdeal f M

The chain ideal lies in the K-shape: the generators agree except the last, whose K-shape generator divides it.

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

The ideal of a chain of length r + 2 is the ideal of its head and its tail.

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

The chain of length one: the chain ideal is the ideal of its equation.

theorem Hironaka.Resolution.span_range_comp_eq_span_image_chainSeg {R : Type u} [CommRing R] {n r : ℕ} (z : Fin n → R) (σ : Fin (r + 1) → Fin n) : Ideal.span (Set.range (z ∘ σ)) = Ideal.span (z '' ↑(chainSeg σ r))

The chain's ideal is the ideal of the full chain segment (all indices ≤ r).

theorem Hironaka.Resolution.chainIdeal_eq_span_inf_chainKIdeal_of_cancel (r : ℕ) (R : Type u) [CommRing R] (f M : Fin (r + 1) → R) : (∀ (i : Fin (r + 1)) (y : R), M i * y ∈ Ideal.span (Set.range f) → y ∈ Ideal.span (Set.range f)) → chainIdeal f M = Ideal.span (Set.range f) ⊓ chainKIdeal f M

The algebraic core of the intersection form: when every monomial M i is a nonzerodivisor modulo the chain's ideal (f), the chain ideal is the intersection of (f) with the K-shape. Induction on the length through the quotient by f₀, as for the colon (colon_chainIdeal_eq_chainKIdeal).

The intersection form in a regular local ring

theorem Hironaka.Resolution.cancel_monomialOf_span_range {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.IsRegularSystemOfParameters z) {r : ℕ} {σ : Fin (r + 1) → Fin n} {a : Fin (r + 1) → Fin n → ℕ} (ha : ∀ (i : Fin (r + 1)), ∀ k ∈ Set.range σ, a i k = 0) (i : Fin (r + 1)) (y : R) (hy : monomialOf z (a i) * y ∈ Ideal.span (Set.range (z ∘ σ))) : y ∈ Ideal.span (Set.range (z ∘ σ))

A monomial in the coordinates off the chain is a nonzerodivisor modulo the chain's prime.

theorem Hironaka.Resolution.chainIdeal_eq_span_inf_chainKIdeal {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.IsRegularSystemOfParameters z) {r : ℕ} {σ : Fin (r + 1) → Fin n} {a : Fin (r + 1) → Fin n → ℕ} (ha : ∀ (i : Fin (r + 1)), ∀ k ∈ Set.range σ, a i k = 0) : (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)

The intersection form (the counterpart of the colon identity chainIdeal_colon_span_eq): in a regular local ring with a regular system of parameters z, chain equations f = z ∘ σ and monomials M_i = ∏_k z_k^{a_{ik}} in the coordinates off the chain, the chain ideal is the intersection of the chain's prime with 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.span_mul_chainIdeal_eq_span_inf {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.IsRegularSystemOfParameters z) {r : ℕ} {σ : Fin (r + 1) → Fin n} {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) : (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)

The intersection form with the top-level monomial factor M⁰ = ∏_k z_k^{b_k} in the coordinates off the chain, through P ∩ mA = m (P ∩ A) for m a product of parameters outside the prime P: M⁰ · I(f; a) = (f) ⊓ M⁰ · K(f; a).