The monomial split on a triple

The modules Hironaka/Resolution/Algebraic/MarkedOrderReduction/Split.lean, SplitOrder.lean, SplitMain.lean, SplitSupport.lean and SplitFunctorial.lean prove [Kol07, Definition–Lemma 110] for a normal-crossings family on a scheme smooth over k (namespace Hironaka.BMO.Snc); this module instantiates them on a triple T = (X, I, E) ([Kol07, Notation 64]: X smooth of finite type over k, hence Noetherian; I nonzero on every component; E with normal crossings), in the forms used by the marked order reduction. Kollár's standing characteristic-zero hypothesis is carried as the statements carry it.

theorem Hironaka.BMO.isInvertible_monomial {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (a : ↥T.X.left → ℕ) : (T.E.monomial a).IsInvertible

Every monomial ideal of the triple's family is invertible (the invertibility of M(I) in [Kol07, Definition–Lemma 110]).

theorem Hironaka.BMO.isInvertible_monomialPart {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) : (monomialPart T.I T.E).IsInvertible

The monomial part is invertible.

theorem Hironaka.BMO.monomialPart_mul_nonmonomialPart {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) : monomialPart T.I T.E * nonmonomialPart T.I T.E = T.I

I = M(I) · N(I) ([Kol07, Definition–Lemma 110]).

theorem Hironaka.BMO.ord_nonmonomialPart_eq_zero {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (i : T.E.ι) {η : ↥T.X.left} (hη : η ∈ (T.E.component i).support.genericPoints) : (nonmonomialPart T.I T.E).ord η = 0

ord_D N(I) = 0 at every component ([Kol07, Definition–Lemma 110]: "cosupp N(I) does not contain any of the E^i", in the fine form).

theorem Hironaka.BMO.isNonzeroEverywhere_nonmonomialPart {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) : (nonmonomialPart T.I T.E).IsNonzeroEverywhere

N(I) is nonzero on every component.

theorem Hironaka.BMO.ord_monomialPart_of_mem_genericPoints {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (i : T.E.ι) {η : ↥T.X.left} (hη : η ∈ (T.E.component i).support.genericPoints) : (monomialPart T.I T.E).ord η = T.I.ord η

The exponent of M(I) at D is ord_D I.

theorem Hironaka.BMO.monomial_eq_monomialPart_of_mul_eq {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) {a : ↥T.X.left → ℕ} {N : T.X.left.IdealSheafData} (h : T.E.monomial a * N = T.I) (hN : ∀ (i : T.E.ι), ∀ η ∈ (T.E.component i).support.genericPoints, N.ord η = 0) : T.E.monomial a = monomialPart T.I T.E ∧ N = nonmonomialPart T.I T.E

The split is unique ([Kol07, Definition–Lemma 110]: "uniquely").

theorem Hironaka.BMO.monomialPart_monomial_mul {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (a : ↥T.X.left → ℕ) (J : T.X.left.IdealSheafData) (hJ : J.IsNonzeroEverywhere) : monomialPart (T.E.monomial a * J) T.E = T.E.monomial a * monomialPart J T.E

The monomial part absorbs monomials ([Kol07, 111, Step 1]).

theorem Hironaka.BMO.nonmonomialPart_monomial_mul {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (a : ↥T.X.left → ℕ) (J : T.X.left.IdealSheafData) (hJ : J.IsNonzeroEverywhere) : nonmonomialPart (T.E.monomial a * J) T.E = nonmonomialPart J T.E

The nonmonomial part ignores monomials ([Kol07, 111, Step 1]).

theorem Hironaka.BMO.nonmonomialPart_of_isEmpty {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (h : IsEmpty T.E.ι) : nonmonomialPart T.I T.E = T.I

For E = ∅, N(I) = I (the last paragraph of [Kol07, 111]).

theorem Hironaka.BMO.eq_monomialPart_of_isInvertible_of_support_le {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) {K : T.X.left.IdealSheafData} (hK : K.IsInvertible) (hsupp : K.support ≤ T.E.support) : K = monomialPart K T.E

An invertible ideal sheaf supported on E is its own monomial part ([BM08, (5.2)]: "N(I) is divisible by no such prime ideal").

theorem Hironaka.BMO.monomialPart_comap {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) {T' : AlgebraicGeometry.Triple k} (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hpb : T'.IsPullbackOf T h) : monomialPart T'.I T'.E = (monomialPart T.I T.E).comap h

M(h^* I) = h^* M(I) for a smooth h: the monomial part commutes with smooth pull-back.

theorem Hironaka.BMO.nonmonomialPart_comap {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) {T' : AlgebraicGeometry.Triple k} (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hpb : T'.IsPullbackOf T h) : nonmonomialPart T'.I T'.E = (nonmonomialPart T.I T.E).comap h

N(h^* I) = h^* N(I) for a smooth h: the nonmonomial part commutes with smooth pull-back.

theorem Hironaka.BMO.monomialPart_baseChange {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) {L : Type u} [Field L] {T' : AlgebraicGeometry.Triple L} (σ : k →+* L) (p : T'.X.left ⟶ T.X.left) (hbc : T'.IsBaseChangeOf T σ p) : monomialPart T'.I T'.E = (monomialPart T.I T.E).comap p

The monomial part commutes with change of fields ([Kol07, 34.2]).

theorem Hironaka.BMO.nonmonomialPart_baseChange {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) {L : Type u} [Field L] [CharZero L] {T' : AlgebraicGeometry.Triple L} (σ : k →+* L) (p : T'.X.left ⟶ T.X.left) (hbc : T'.IsBaseChangeOf T σ p) : nonmonomialPart T'.I T'.E = (nonmonomialPart T.I T.E).comap p

The nonmonomial part commutes with change of fields ([Kol07, 34.2]).