The exponents of a piece family and the order of its monomial ideal

The marked monomial ideal of a realising piece family is E.monomial Φ.exponentAt in the sense of Hironaka/Resolution/Algebraic/MarkedOrderReduction/MonomialPart.lean, the exponent at a generic point of a member being the exponent of the unique piece through it. Not in the sources as statements.

• faceAt_eq_singleton_of_mem_genericPoints: exactly one piece passes through a generic point of a member, a piece of the member's label, since no other member passes (notMem_support_of_ne of Hironaka/Resolution/Algebraic/Snc/ComponentStalks.lean) and two pieces of one label are disjoint.
• monomial_exponentAt_ofDivisorFamily: the exponent function of the input family gives back the marked monomial ideal E.monomial a (monomial_congr of Hironaka/Resolution/Algebraic/MarkedOrderReduction/SplitMain.lean: a monomial ideal depends on its exponents at the generic points only, where the input family's exponent is a).
• ord_monomial_eq_total, leOrdAlong_centerOf: the order of the marked monomial ideal at a point is the sum of the exponents of the pieces through it. The stalk is a product of powers of distinct regular parameters, and the order is additive on a regular local ring containing ℚ (ordElem_mul_of_algebraRat of Hironaka/Algebra/Local/CohenIso.lean). So the order along a centre whose faces have sum ≥ m is ≥ m, condition (4′) of [Kol07, Definition 66] for the blow-ups of Step 3, Kollár's a_{j₁} + ⋯ + a_{j_r} ≥ m in [Kol07, 111, Step 3.r].

The last two results are what Hironaka/Resolution/Algebraic/Monomial/Geometric/OrderSeq.lean uses to show that the geometric Step 3 is a blow-up sequence of order ≥ m ending with max-ord < m.

The face through a generic point of a member

theorem Hironaka.Monomial.PieceFamily.faceAt_eq_singleton_of_mem_genericPoints_of_regular {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} (hE : E.IsSnc) (hΦ : Φ.Realizes E e) {j : E.ι} {η : ↥X} (hreg : IsRegularLocalRing ↑(X.presheaf.stalk η)) (hη : η ∈ (E.component j).support.genericPoints) : ∃ c < Φ.nextComp, Φ.label c = ↑(e j) ∧ η ∈ Φ.piece c ∧ Φ.faceAt η = {c} ∧ Φ.exponentAt η = Φ.a c

Exactly one piece passes through a generic point η of a member, a piece of the member's label, when the stalk at η is regular: the general form of faceAt_eq_singleton_of_mem_genericPoints below, with the regularity of the stalk as the hypothesis, for use on the blow-up.

theorem Hironaka.Monomial.PieceFamily.faceAt_eq_singleton_of_mem_genericPoints {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} (hE : E.IsSnc) (hΦ : Φ.Realizes E e) {j : E.ι} {η : ↥X} (hη : η ∈ (E.component j).support.genericPoints) : ∃ c < Φ.nextComp, Φ.label c = ↑(e j) ∧ η ∈ Φ.piece c ∧ Φ.faceAt η = {c} ∧ Φ.exponentAt η = Φ.a c

Exactly one piece passes through a generic point η of a member E^j, a piece of the label of j (the other members miss η), so the exponent at η is that piece's exponent.

The input family's exponents

theorem Hironaka.Monomial.PieceFamily.monomial_exponentAt_ofDivisorFamily {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {E : X.DivisorFamily} (hE : E.IsSnc) {L k' : ℕ} (a : ↥X → ℕ) (e' : E.ι ≃o Fin L) (σ : Fin k' ≃ Components E) : E.monomial (ofDivisorFamily E a e' σ).exponentAt = E.monomial a

The exponent function of the input family gives back the marked monomial ideal E.monomial a (one exponent per generic point of a member): at a generic point of a member the unique piece through it is its own irreducible component, whose exponent is a there.

The order of the monomial ideal at a point

theorem Hironaka.Monomial.PieceFamily.ord_prod_span_singleton_pow {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (hmul : ∀ (f g : R), IsLocalRing.ordElem (f * g) = IsLocalRing.ordElem f + IsLocalRing.ordElem g) {ι : Type u_2} (s : Finset ι) (g : ι → R) (a : ι → ℕ) : IsLocalRing.ord (∏ i ∈ s, Ideal.span {g i} ^ a i) = ∑ i ∈ s, ↑(a i) * IsLocalRing.ordElem (g i)

The order of a product of powers of principal ideals, when the order of elements is additive (a regular local ring containing ℚ).

theorem Hironaka.Monomial.PieceFamily.ord_monomial_eq_total {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} [CharZero k] [AlgebraicGeometry.QuasiCompact f] (hE : E.IsSnc) (hΦ : Φ.Realizes E e) (x : ↥X) : (E.monomial Φ.exponentAt).ord x = ↑(Φ.total (Φ.faceAt x))

The order of the marked monomial ideal at x is the sum of the exponents of the pieces through x: its stalk is ∏_{c ∈ faceAt x} z_c^{a_c} for the coordinates of the members through x, and the order is additive on the regular local ring 𝒪_{X,x} ⊇ ℚ.

theorem Hironaka.Monomial.PieceFamily.leOrdAlong_centerOf {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} [CharZero k] [AlgebraicGeometry.QuasiCompact f] (hE : E.IsSnc) (hΦ : Φ.Realizes E e) {n m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hS : (Φ.toState n m hV).IsCenter S) (hge : ∀ P ∈ S, m ≤ Φ.total P) : (E.monomial Φ.exponentAt).LeOrdAlong (Φ.centerOf S).support ↑m

When every face of the centre has sum ≥ m, the marked monomial ideal has order ≥ m along the centre (condition (4′) of [Kol07, Definition 66]; Kollár's a_{j₁} + ⋯ + a_{j_r} ≥ m in [Kol07, 111, Step 3.r]): at a generic point of Z_P the pieces of P pass, so the order is at least a(P).