The monomial ideal of a family ignores unit members

[Kol07, Definition–Lemma 110] reads the monomial ideal 𝒪_X(−∑ c_i E^i) on the irreducible components of the members E^i; the convention [Kol07, 32] deletes empty blow-ups, whose exceptional divisors survive here as unit members of the boundary. A unit member has empty support, hence no irreducible components and the factor 1 in the product defining DivisorFamily.monomial: the monomial ideal of a family extended by unit members (ExtendsByEmpty) is the monomial ideal of the smaller family (monomial_of_extendsByEmpty), through the general product identity prod_component_of_extendsByEmpty. The consequences for the monomial and nonmonomial parts (monomialPart_of_extendsByEmpty, nonmonomialPart_of_extendsByEmpty) are in Hironaka/Resolution/Algebraic/MarkedOrderReduction/UpToUnits.lean. This module imports both MonomialPart.lean (the monomial ideal) and Hironaka.Scheme.BlowUpSequence.PullbackEraseEmpty (ExtendsByEmpty), neither of which imports the other.

theorem AlgebraicGeometry.Scheme.DivisorFamily.prod_component_of_extendsByEmpty {X : Scheme} {α : Type u_1} [CommMonoid α] {E' E : X.DivisorFamily} (hext : ExtendsByEmpty E' E) (G : X.IdealSheafData → α) (hG : G ⊤ = 1) : ∏ j : E.ι, G (E.component j) = ∏ i : E'.ι, G (E'.component i)

A product over the members of a family extended by unit members, of a function equal to 1 on the unit ideal, is the product over the members of the smaller family.

theorem AlgebraicGeometry.Scheme.DivisorFamily.monomial_of_extendsByEmpty {X : Scheme} {E' E : X.DivisorFamily} (hext : ExtendsByEmpty E' E) (a : ↥X → ℕ) : E.monomial a = E'.monomial a

The monomial ideal of a family ignores unit members ([Kol07, Definition–Lemma 110] with the convention [Kol07, 32]): the unit ideal has empty support, hence no irreducible components and the factor 1.