The monomial split, V: an invertible ideal sheaf supported on the family is a monomial

The uniqueness clause of [Kol07, Definition–Lemma 110] in the form used for the transforms (Hironaka/Resolution/Algebraic/MarkedOrderReduction/Transform.lean), which is the form of BM08, (5.2) ("N(I) is divisible by no such prime ideal"): an invertible ideal sheaf K whose support lies in the support of the normal-crossings family E equals its monomial part. Its nonmonomial part N is invertible, supported on E, and of order 0 along every component; if N ≠ 𝒪_X, a generic point ξ of supp N lies on some component D of some E^i with generic point η, N_ξ = (g) with g a non-unit, z_c ∤ g (else N_η ≠ 𝒪_{X,η}), and 𝔪_ξ = √(g) (the only minimal prime over (g) is the prime of the generic point ξ itself, by the minimal-prime dictionary of Hironaka/Resolution/Algebraic/Snc/DictionaryGenericPoints.lean), so g ∣ z_c^n; a divisor of a power of the prime z_c not divisible by z_c is a unit, a contradiction.

• Snc.eq_monomialPart_of_isInvertible_of_support_le: the lemma; its form on a triple is in Hironaka/Resolution/Algebraic/MarkedOrderReduction/SplitTriple.lean.

The auxiliaries on invertible sheaves and divisor families are in Hironaka/Scheme/IdealSheaf/Invertible.lean and Hironaka/Resolution/Algebraic/Snc/DictionaryGenericPoints.lean.

theorem Hironaka.BMO.Snc.eq_monomialPart_of_isInvertible_of_support_le {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] [TopologicalSpace.NoetherianSpace ↥X] (E : X.DivisorFamily) (hE : E.IsSnc) {K : X.IdealSheafData} (hK : K.IsInvertible) (hsupp : K.support ≤ E.support) : K = monomialPart K E

An invertible ideal sheaf whose support lies in the support of E is its own monomial part (the uniqueness clause of [Kol07, Definition–Lemma 110]; [BM08, (5.2)]).