Two ring-level corners of the chain form

Two elementary facts about the chain ideal (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) used in the proof of the statement CP1 of the embedded desingularization, the local form of the ideal at the absorbing stage:

• A prime containing the chain form contains the chain. A prime ideal containing M⁰ · chainIdeal f M and none of the monomials M⁰, M_i contains every chain equation f_i (span_range_le_of_mul_chainIdeal_le_prime): the generator (∏_{i'<i} M_{i'}) f_i lies in the prime and its monomial factor does not. Geometrically, another component's strict transform through a point of Γ̃ would contain Γ̃ near the point — impossible for strict transforms of distinct components (the disjointness clause of the protected state); used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Absorbed.
• The hypersurface case. In a local ring, an ideal inside a principal prime (g), g ∈ 𝔪, that contains an element outside 𝔪² equals (g) (eq_span_singleton_of_le_of_exists_notMem_sq): the element is g y with y a unit. This is the local form at the absorbing stage when the absorbed component is a hypersurface (the chain has length one, J_p = (g), no monomial); used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainCaseA.

theorem Hironaka.Resolution.prod_notMem_of_forall_notMem {R : Type u_1} [CommRing R] {P : Ideal R} (hP : P.IsPrime) {ι : Type u_2} (s : Finset ι) (g : ι → R) (hg : ∀ i ∈ s, g i ∉ P) : ∏ i ∈ s, g i ∉ P

A finite product of elements outside a prime ideal is outside it.

theorem Hironaka.Resolution.span_range_le_of_mul_chainIdeal_le_prime {R : Type u_1} [CommRing R] {P : Ideal R} (hP : P.IsPrime) {r : ℕ} (f M : Fin r → R) (hM : ∀ (i : Fin r), M i ∉ P) (m₀ : R) (hm₀ : m₀ ∉ P) (h : Ideal.span {m₀} * chainIdeal f M ≤ P) : Ideal.span (Set.range f) ≤ P

A prime containing M⁰ · chainIdeal f M and none of the monomials contains every chain equation.

theorem Hironaka.Resolution.eq_span_singleton_of_le_of_exists_notMem_sq {R : Type u_1} [CommRing R] [IsLocalRing R] {g : R} (hg : g ∈ IsLocalRing.maximalIdeal R) {J : Ideal R} (hJ : J ≤ Ideal.span {g}) (hx : ∃ x ∈ J, x ∉ IsLocalRing.maximalIdeal R ^ 2) : J = Ideal.span {g}

The hypersurface case: in a local ring, an ideal inside (g), g ∈ 𝔪, containing an element outside 𝔪² is (g).

theorem Hironaka.Resolution.chainIdeal_one_eq_span {R : Type u_1} [CommRing R] (g : R) (M : Fin 1 → R) : chainIdeal (fun (x : Fin 1) => g) M = Ideal.span {g}

The chain ideal of a chain of length one is the principal ideal of its equation.