The monomial factor of the chain form

Step 1 of the proof of [Kol07, Theorem 107] runs the order reduction on the nonmonomial part N(I) and carries the monomial part M(I) along as a pullback: at stage i of the run, I_i = N(I)_i · π_i^* M(I) ([Kol07, Definition 60] for a product, markedTransformSeq_mul_comap). The chain-relative form of the statement CP1 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) at the absorbing stage is therefore established for N(I)_i and multiplied by the pulled-back monomial. This module supplies the facts that make the product a chain form:

• exists_comap_monomial_eq_monomial_stageMap — the pullback of a monomial 𝒪_X(−∑ a_D D) of an snc family along a smooth blow-up sequence whose centres have simple normal crossings with the induced families is a monomial of the induced family at every stage (the one-step form is exists_comap_monomial_eq_monomial; the corresponding statement for the monomial part is exists_comap_monomialPart_eq_monomial);
• chainRelativeAt_mul_monomial — in chain coordinates at p a monomial of E is the principal ideal (∏ z_k^{b′_k}) with b′ supported on the members' coordinates (the stalk of a monomial is the product over the members through p of the powers of their stalks, exists_stalkIdeal_monomial_eq_prod), so the product with a chain form is a chain form with the top-level exponents added (monomialOf_add);
• chainRelativeAt_markedTransformSeq_mul_monomial — the two combined along a run of order ≥ m.

Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Step1 and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainCaseA.

Algebra: exponents add

theorem Hironaka.Resolution.monomialOf_add {R : Type u_1} [CommRing R] {n : ℕ} (z : Fin n → R) (a b : Fin n → ℕ) : monomialOf z (a + b) = monomialOf z a * monomialOf z b

Exponent vectors add under the product of monomials.

The stalk of a monomial as a product over the members

theorem Hironaka.Resolution.exists_stalkIdeal_monomial_eq_prod {X : AlgebraicGeometry.Scheme} [TopologicalSpace.NoetherianSpace ↥X] (E : X.DivisorFamily) (hE : E.IsSnc) (a : ↥X → ℕ) (x : ↥X) : ∃ (b : E.ι → ℕ), (E.monomial a).stalkIdeal x = ∏ i : E.ι, (E.component i).stalkIdeal x ^ b i

The stalk at x of a monomial 𝒪_X(−∑ a_D D) of an snc family is the product over the members of powers of their stalks — the exponent of a member through x is the exponent of its one component through x, a member missing x has stalk ⊤ and exponent 0.

theorem Hironaka.Resolution.support_monomial_le {X : AlgebraicGeometry.Scheme} [TopologicalSpace.NoetherianSpace ↥X] (E : X.DivisorFamily) (a : ↥X → ℕ) : (E.monomial a).support ≤ E.support

The support of a monomial of E lies in the support of E — off E every factor is the unit ideal.

In chain coordinates

theorem Hironaka.Resolution.ChainCoords.prod_pow_stalkIdeal_eq_span {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {Γ : X.IdealSheafData} {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 → ℕ} (h : ChainCoords E Γ p z c σ a) (b : E.ι → ℕ) : ∃ (b' : Fin n → ℕ), (∀ (k : Fin n), b' k ≠ 0 → k ∈ Set.range c) ∧ ∏ j : E.ι, (E.component j).stalkIdeal p ^ b j = Ideal.span {monomialOf z b'}

In chain coordinates at p the product over the members of powers of their stalks is the principal ideal of a monomial in the coordinates: a member through p contributes z_{c j}^{b j}, a member missing p contributes ⊤ ^ b j = 1; the exponent of z_k is the sum of the b j over the members j through p with c j = k, so it is supported on range c.

The product of a chain form with a monomial

theorem Hironaka.Resolution.chainRelativeAt_mul_monomial {X : AlgebraicGeometry.Scheme} [TopologicalSpace.NoetherianSpace ↥X] {E : X.DivisorFamily} (hE : E.IsSnc) {N Γ : X.IdealSheafData} {p : ↥X} (h : ChainRelativeAt E N Γ p) (a : ↥X → ℕ) : ChainRelativeAt E (N * E.monomial a) Γ p

The monomial ingredient of CP1 (Step 1 of the proof of [Kol07, Theorem 107] carries the monomial part along as a pullback): the product of an ideal sheaf in chain form along Γ at p with a monomial of the snc family E is in chain form along Γ at p, with the monomial's exponents added to the top-level exponents.

The pull-back of a monomial along a blow-up and along a run

theorem Hironaka.Resolution.exists_comap_monomial_eq_monomial {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] [AlgebraicGeometry.IsNoetherian X] (E : X.DivisorFamily) (hE : E.IsSnc) (D : X.IdealSheafData) [AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp D.subschemeι f)] (hD : E.HasSncWith D) (a : ↥X → ℕ) : ∃ (a' : ↥D.blowUp → ℕ), (E.monomial a).comap D.blowUpπ = (E.totalTransform D).monomial a'

The pullback of a monomial 𝒪_X(−∑ a_D D) of E along the blow-up of a centre D with simple normal crossings with E is a monomial of the total transform π^{-1}_{tot} E — invertible and supported over supp E, hence on supp π^{-1}_{tot} E (a point off the exceptional divisor lies on the strict transform of the member through its image); it is then its own monomial part (eq_monomialPart_of_isInvertible_of_support_le). This is the observation in Step 1 of the proof of [Kol07, Theorem 107] that the pullbacks differ from the transforms only in their monomial part.

theorem Hironaka.Resolution.exists_comap_monomial_eq_monomial_stageMap_mk {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (hA : AlgebraicGeometry.IsNoetherian X) (S : X.BlowUpSequence) (E : X.DivisorFamily) (hsm : S.IsSmooth f) (hE : E.IsSnc) (hsnc : ∀ (i : Fin S.length), (S.totalTransformSeq E i.castSucc).HasSncWith (S.center i)) (a : ↥X → ℕ) (j : ℕ) (hj : j < S.length + 1) : ∃ (a' : ↥(S.stage ⟨j, hj⟩) → ℕ), (E.monomial a).comap (S.stageMap ⟨j, hj⟩) = (S.totalTransformSeq E ⟨j, hj⟩).monomial a'

exists_comap_monomial_eq_monomial iterated along a smooth blow-up sequence whose centres have simple normal crossings with the induced families (the snc clause of IsOrderGeSeq), in the ⟨j, hj⟩ form of the indices: the pull-back of a monomial of E to stage j is a monomial of the induced family E_j.

theorem Hironaka.Resolution.exists_comap_monomial_eq_monomial_stageMap {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] [AlgebraicGeometry.IsNoetherian X] (S : X.BlowUpSequence) (E : X.DivisorFamily) (hsm : S.IsSmooth f) (hE : E.IsSnc) (hsnc : ∀ (i : Fin S.length), (S.totalTransformSeq E i.castSucc).HasSncWith (S.center i)) (a : ↥X → ℕ) (i : Fin (S.length + 1)) : ∃ (a' : ↥(S.stage i) → ℕ), (E.monomial a).comap (S.stageMap i) = (S.totalTransformSeq E i).monomial a'

exists_comap_monomial_eq_monomial_stageMap_mk at an arbitrary stage index.

theorem Hironaka.Resolution.exists_comap_monomial_eq_monomial_of_isOrderGeSeq {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] [AlgebraicGeometry.IsNoetherian X] {S : X.BlowUpSequence} {N : X.IdealSheafData} {m : ℕ} {E : X.DivisorFamily} (hS : S.IsOrderGeSeq f N m E) (hE : E.IsSnc) (a : ↥X → ℕ) (i : Fin (S.length + 1)) : ∃ (a' : ↥(S.stage i) → ℕ), (E.monomial a).comap (S.stageMap i) = (S.totalTransformSeq E i).monomial a'

The sequence form: along a run of order ≥ m for (N, m) with snc boundary E the pullback of a monomial of E is a monomial of the induced family at every stage.

theorem Hironaka.Resolution.chainRelativeAt_markedTransformSeq_mul_monomial {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] [AlgebraicGeometry.IsNoetherian X] (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] {S : X.BlowUpSequence} {N : X.IdealSheafData} {m : ℕ} {E : X.DivisorFamily} (hS : S.IsOrderGeSeq f N m E) (hE : E.IsSnc) (a : ↥X → ℕ) (i : Fin (S.length + 1)) {Γ : (S.stage i).IdealSheafData} {p : ↥(S.stage i)} (h : ChainRelativeAt (S.totalTransformSeq E i) (S.markedTransformSeq N m i) Γ p) : ChainRelativeAt (S.totalTransformSeq E i) (S.markedTransformSeq (N * E.monomial a) m i) Γ p

Along a smooth run of order ≥ m for (N, m) with snc boundary E (IsOrderGeSeq), the chain form of the marked transform of N along Γ at a point of stage i gives the chain form of the marked transform of N · 𝒪_X(−∑ a_D D) — [Kol07, Definition 60] for a product (markedTransformSeq_mul_comap) splits off the pullback of the monomial, a monomial of the induced family absorbed into the top-level exponents.