The fine split of a chain shape at the stalk

[Kol07, Definition–Lemma 110] writes I = M(I) · N(I) with M(I) the monomial part 𝒪(−∑ cᵢ Eⁱ) and N(I) the nonmonomial part, whose cosupport contains no Eⁱ; the library has the split (monomialPart_mul_nonmonomialPart) and the vanishing of ord N(I) along the members (ord_nonmonomialPart_eq_zero). The proof of the statement CP3 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) needs the split read in chain coordinates at a point p: if K_p = (∏ z_{c j}^{b_{c j}}) · C with C the chain part (the K-shape or the un-isolated form), then N(K)_p = C. Two facts make this a cancellation:

• stalkIdeal_monomialPart_eq_span_prod — the stalk of M(K) at p is the monomial in the coordinates of the members through p, with exponents the orders of K at their generic points ([Kol07, Definition 47]; stalkIdeal_monomial, finprod_stalk_eq_of_specializes; members not through p contribute the unit ideal);
• eq_of_span_prod_pow_mul_eq — in a regular local ring with a regular system z, if two monomials in the coordinates z (c j), whose ideals (z (c j)) are prime, times ideals lying in none of those primes agree, the exponents and the cofactors agree (compare exponent by exponent: cancel the common power, the remaining monomial in the other coordinates lies outside the prime, Ideal.span_singleton_mul_right_inj).

The nonmonomial part lies in no member's prime because its order at the member's generic point is 0 ([Kol07, Definition–Lemma 110]; hence the hypothesis that the ideal is nonzero everywhere), and the chain part contains the first equation z_{σ 0} of the chain, a coordinate off the members (notMem_span_singleton_of_ne); with r = 0 the K-shape is the unit ideal. stalkIdeal_nonmonomialPart_eq_of_eq_span_mul is the common core; stalkIdeal_nonmonomialPart_of_kShape and stalkIdeal_nonmonomialPart_of_iShape are its instances. The chain coordinates are those of [Kol07, Definition 24]. These identities are not in the literature. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Step3 and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Step1.

theorem Hironaka.Resolution.notMem_span_singleton_of_ne {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.IsRegularSystemOfParameters z) {i j : Fin n} (hij : i ≠ j) : z i ∉ Ideal.span {z j}

A coordinate of a regular system lies outside the prime of another coordinate: AlgebraicGeometry.notMem_span_singleton_of_ne read on IsRegularSystemOfParameters.

theorem Hironaka.Resolution.ne_zero_of_isRegularSystemOfParameters {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.IsRegularSystemOfParameters z) (i : Fin n) : z i ≠ 0

A coordinate of a regular system is nonzero.

theorem Hironaka.Resolution.prod_pow_notMem_span_singleton {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.IsRegularSystemOfParameters z) {ι : Type u_2} [Fintype ι] [DecidableEq ι] {c : ι → Fin n} (hc : Function.Injective c) (e : ι → ℕ) (j₀ : ι) (hprime : (Ideal.span {z (c j₀)}).IsPrime) : ∏ j ∈ Finset.univ.erase j₀, z (c j) ^ e j ∉ Ideal.span {z (c j₀)}

A monomial in the coordinates other than z (c j₀) lies outside the prime (z (c j₀)).

theorem Hironaka.Resolution.le_of_span_prod_pow_mul_eq {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.IsRegularSystemOfParameters z) {ι : Type u_2} [Fintype ι] {c : ι → Fin n} (hc : Function.Injective c) (hprime : ∀ (j : ι), (Ideal.span {z (c j)}).IsPrime) (e₁ e₂ : ι → ℕ) {N₁ N₂ : Ideal R} (h₁ : ∀ (j : ι), ¬N₁ ≤ Ideal.span {z (c j)}) (h : Ideal.span {∏ j : ι, z (c j) ^ e₁ j} * N₁ = Ideal.span {∏ j : ι, z (c j) ^ e₂ j} * N₂) (j : ι) : e₂ j ≤ e₁ j

One direction of the exponent comparison: a larger exponent on one side would put the other side's cofactor into the prime.

theorem Hironaka.Resolution.eq_of_span_prod_pow_mul_eq {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.IsRegularSystemOfParameters z) {ι : Type u_2} [Fintype ι] {c : ι → Fin n} (hc : Function.Injective c) (hprime : ∀ (j : ι), (Ideal.span {z (c j)}).IsPrime) (e₁ e₂ : ι → ℕ) {N₁ N₂ : Ideal R} (h₁ : ∀ (j : ι), ¬N₁ ≤ Ideal.span {z (c j)}) (h₂ : ∀ (j : ι), ¬N₂ ≤ Ideal.span {z (c j)}) (h : Ideal.span {∏ j : ι, z (c j) ^ e₁ j} * N₁ = Ideal.span {∏ j : ι, z (c j) ^ e₂ j} * N₂) : e₁ = e₂ ∧ N₁ = N₂

Uniqueness of the monomial factor: two factorizations (monomial) · N with the cofactors in no coordinate prime have the same exponents and the same cofactor.

theorem Hironaka.Resolution.monomialOf_eq_prod_of_forall_mem_range {R : Type u_1} [CommRing R] {n : ℕ} (z : Fin n → R) {ι : Type u_2} [Fintype ι] {c : ι → Fin n} (hc : Function.Injective c) {b : Fin n → ℕ} (hb : ∀ (κ : Fin n), b κ ≠ 0 → κ ∈ Set.range c) : monomialOf z b = ∏ j : ι, z (c j) ^ b (c j)

A monomial with exponents supported on the range of an injection is the product over the domain of the injection.

theorem Hironaka.Resolution.stalkIdeal_monomialPart_eq_span_prod {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n₀ : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n₀ f] {E : X.DivisorFamily} (hE : E.IsSnc) (K : X.IdealSheafData) {p : ↥X} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk p)} {c : { j : E.ι // p ∈ (E.component j).support } → Fin n} (hcmem : ∀ (j : { j : E.ι // p ∈ (E.component j).support }), (E.component ↑j).stalkIdeal p = Ideal.span {z (c j)}) (η : { j : E.ι // p ∈ (E.component j).support } → ↥X) (hη : ∀ (j : { j : E.ι // p ∈ (E.component j).support }), η j ∈ (E.component ↑j).support.genericPoints) (hηp : ∀ (j : { j : E.ι // p ∈ (E.component j).support }), η j ⤳ p) : (BMO.monomialPart K E).stalkIdeal p = Ideal.span {∏ j : { j : E.ι // p ∈ (E.component j).support }, z (c j) ^ (K.ord (η j)).toNat}

[Kol07, Definition–Lemma 110] at the stalk: the stalk of the monomial part at p is the monomial in the coordinates of the members through p, with the orders at their generic points as exponents.

theorem Hironaka.Resolution.stalkIdeal_nonmonomialPart_eq_of_eq_span_mul {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n₀ : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n₀ f] {E : X.DivisorFamily} (hE : E.IsSnc) {K : X.IdealSheafData} (hK0 : K.IsNonzeroEverywhere) {p : ↥X} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk p)} {c : { j : E.ι // p ∈ (E.component j).support } → Fin n} {r : ℕ} {σ : Fin (r + 1) → Fin n} {a : Fin (r + 1) → Fin n → ℕ} (hc : ChainCoordsFree E p z c σ a) {b : Fin n → ℕ} (hb : ∀ (κ : Fin n), b κ ≠ 0 → κ ∈ Set.range c) {C : Ideal ↑(X.presheaf.stalk p)} (hC : ∀ (j : { j : E.ι // p ∈ (E.component j).support }), ¬C ≤ Ideal.span {z (c j)}) (hK : K.stalkIdeal p = Ideal.span {monomialOf z b} * C) : (BMO.nonmonomialPart K E).stalkIdeal p = C

The common core of the fine split in chain coordinates: the nonmonomial part of an ideal whose stalk is a monomial in the members' coordinates times an ideal lying in no member's prime is that ideal.

theorem Hironaka.Resolution.stalkIdeal_nonmonomialPart_of_kShape {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n₀ : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n₀ f] {E : X.DivisorFamily} (hE : E.IsSnc) {K : X.IdealSheafData} (hK0 : K.IsNonzeroEverywhere) {p : ↥X} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk p)} {c : { j : E.ι // p ∈ (E.component j).support } → Fin n} {r : ℕ} {σ : Fin (r + 1) → Fin n} {a : Fin (r + 1) → Fin n → ℕ} {b : Fin n → ℕ} (hc : ChainCoordsFree E p z c σ a) (hb : ∀ (κ : Fin n), b κ ≠ 0 → κ ∈ Set.range c) (hK : K.stalkIdeal p = Ideal.span {monomialOf z b} * chainKIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) : (BMO.nonmonomialPart K E).stalkIdeal p = chainKIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)

The fine split of [Kol07, Definition–Lemma 110] at the stalk: the nonmonomial part of a K-shape is its chain part.

theorem Hironaka.Resolution.stalkIdeal_nonmonomialPart_of_iShape {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n₀ : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n₀ f] {E : X.DivisorFamily} (hE : E.IsSnc) {I : X.IdealSheafData} (hI0 : I.IsNonzeroEverywhere) {p : ↥X} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk p)} {c : { j : E.ι // p ∈ (E.component j).support } → Fin n} {r : ℕ} {σ : Fin (r + 1) → Fin n} {a : Fin (r + 1) → Fin n → ℕ} {b : Fin n → ℕ} (hc : ChainCoordsFree E p z c σ a) (hb : ∀ (κ : Fin n), b κ ≠ 0 → κ ∈ Set.range c) (hI : I.stalkIdeal p = Ideal.span {monomialOf z b} * chainIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) : (BMO.nonmonomialPart I E).stalkIdeal p = chainIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)

The fine split at the stalk for the un-isolated form: the nonmonomial part of an I-shape is its chain part.