The monomial split, I: monomials of a normal-crossings family at a point

The monomial and nonmonomial parts of [Kol07, Definition–Lemma 110] (Hironaka/Resolution/Algebraic/MarkedOrderReduction/MonomialPart.lean) are products over the irreducible components of the members of a family with normal crossings. This module computes them at a point of a scheme smooth over a field, in Kollár's coordinates ([Kol07, Definition 24]): at x, a member through x has stalk (z_c) for one parameter z_c of a regular system of parameters of 𝒪_{X,x}, exactly one of its irreducible components passes through x (its reduced ideal has the same stalk (z_c), the unique minimal prime over the prime (z_c)), and every other component has the unit stalk. Hence the stalk of 𝒪_X(−∑_D a_D D) at x is the principal ideal generated by the monomial ∏_c z_c^{a_c} over the members through x, a nonzerodivisor of the domain 𝒪_{X,x}, which gives the invertibility of the monomial ideals.

• stalkIdeal_monomial: the stalk of a monomial in algebraic form; the two evaluations of a member's inner product are finprod_stalk_eq_of_specializes and finprod_stalk_eq_one_of_notMem (Hironaka/Resolution/Algebraic/Snc/ComponentStalks.lean);
• Snc.stalkIdeal_monomial_eq_span (a principal ideal generated by a nonzero element) and Snc.isInvertible_monomial (every monomial ideal of a normal-crossings family on a smooth Noetherian scheme is invertible).

The parameter algebra, the generic points of the components and the regular-subscheme forms used here are in Hironaka/Scheme/Snc/ParameterAlgebra.lean, Hironaka/Resolution/Algebraic/Snc/DictionaryGenericPoints.lean, Hironaka/Resolution/Algebraic/Snc/DictionaryRegular.lean and Hironaka/Resolution/Algebraic/Snc/ComponentStalks.lean. The statements on a triple are in Hironaka/Resolution/Algebraic/MarkedOrderReduction/SplitTriple.lean.

The components of a member at a point

theorem Hironaka.BMO.stalkIdeal_monomial {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (hfin : ∀ (i : E.ι), (E.component i).support.genericPoints.Finite) (a : ↥X → ℕ) (x : ↥X) : (E.monomial a).stalkIdeal x = ∏ i : E.ι, ∏ᶠ (η : ↥X) (_ : η ∈ (E.component i).support.genericPoints), (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal x ^ a η

The stalk of 𝒪_X(−∑_D a_D D) at x is the product over the members and their components of the powers of the components' stalks.

The general setting: a normal-crossings family E on a scheme X smooth over k (regular stalks), the scheme Noetherian where the components have to be finitely many. The statements on triples are the instances of this setting at T.X.left ↘ Spec k, T.E, T.I (SplitTriple.lean); the smooth-pull-back and base-change identities apply it on the source with T.E.comap h.

The stalk of a monomial

theorem Hironaka.BMO.Snc.stalkIdeal_monomial_eq_span {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) (hE : E.IsSnc) [TopologicalSpace.NoetherianSpace ↥X] (a : ↥X → ℕ) (x : ↥X) : ∃ (g : ↑(X.presheaf.stalk x)), g ≠ 0 ∧ (E.monomial a).stalkIdeal x = Ideal.span {g}

The stalk of a monomial of a normal-crossings family at x is the principal ideal of a nonzero element: the product over the members through x of z_c^{a} in Kollár's coordinates, a nonzero element of the domain 𝒪_{X,x}. This is the local form of the invertibility of M(I).

theorem Hironaka.BMO.Snc.isInvertible_monomial {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) (hE : E.IsSnc) [TopologicalSpace.NoetherianSpace ↥X] (a : ↥X → ℕ) : (E.monomial a).IsInvertible

Every monomial ideal of a normal-crossings family on a smooth Noetherian scheme is invertible (the invertibility of M(I) in [Kol07, Definition–Lemma 110]).