Piece families: the geometric state of the monomial procedure

Kollár's Step 3 ([Kol07, 111, Step 3]) runs on the combinatorial state of Hironaka/Resolution/Algebraic/Monomial/State.lean. Its realisation on a scheme carries a labelled piece family along the run: for each component index c < nextComp a closed set piece c of the ambient scheme (a nonempty disjoint union of irreducible components of the member E^{label c}, or empty when the component is dead), its label (the index of its member through an order isomorphism E.ι ≃o Fin nextLabel) and its exponent. At the input the pieces are the irreducible components of the members (ofDivisorFamily); after the blow-up of a centre S (a finset of faces) the old pieces become their strict transforms and each face P ∈ S contributes one new piece π⁻¹(Z_P) under the new label, Kollár's new divisor put last ([Kol07, Definition 65]): one smooth, possibly reducible, divisor per blow-up, its irreducible components pairwise disjoint and carrying the common exponent a(P) − m. A "component" of the state is therefore an irreducible component at the input only. This is what makes the nerve transition an equality: for E⁰ = V(y) and E¹ = V(y − x² + 1) in 𝔸² the face {E⁰, E¹} has a disconnected centre (two points) and a reducible exceptional divisor, and tracking its two components separately would break the correspondence with the combinatorial rule. Not in the sources in this form.

• PieceFamily: the data; faceSet (the intersection of the pieces of a face), nerve (the nonempty faces below nextComp with nonempty intersection), IsValid n m (the invariants of the combinatorial state for the family's data, discharged from the geometric hypotheses in Hironaka/Resolution/Algebraic/Monomial/Geometric/Nerve.lean), toState n m hV (the combinatorial state; every data field is the family's, definitionally).
• faceIdeal, centerOf: the ideal sheaves of Z_P = ⋂_{c ∈ P} piece c and Z_S = ⋃_{P ∈ S} Z_P.
• newComp, blowUpPieces: the transition, the strict transforms of the old pieces and π⁻¹(Z_P) for the new piece of P, with labels and exponents by the formulas of the combinatorial transition, so that toState (Φ.blowUpPieces S m) = (toState Φ).blowUp S is a literal equality once the nerves agree (toState_blowUpPieces_of_nerve_eq; the nerves agree by nerve_blowUpPieces of Hironaka/Resolution/Algebraic/Monomial/Geometric/Kernel.lean).
• exponentAt, faceAt: the exponent function of the marked monomial ideal E.monomial Φ.exponentAt (Hironaka/Resolution/Algebraic/MarkedOrderReduction/MonomialPart.lean) and the face of the pieces through a point.
• Realizes E e: the piece family realises the boundary E, each member being the disjoint union of its pieces.
• RefinesAlong, restrictNerve, restrictState: the refinement relation along a morphism h : Y ⟶ X and the state restricted to the faces meeting the image of h, the geometric forms of Refines and Sub of Hironaka/Resolution/Algebraic/Monomial/Restrict.lean.
• Components, ofDivisorFamily: the input piece family (the irreducible components).
• extendIso: the label isomorphism extended along the index type of the total transform.
• realizeAux, stagePieces, realize: the fold of a list of centres (the combinatorial run (step3 st).2) into a blow-up sequence, carrying the piece family; realize is the geometric Step 3, the third step of BMO_{n,m} (Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step3Input.lean).

structure Hironaka.Monomial.PieceFamily (X : AlgebraicGeometry.Scheme) : Type u

A labelled piece family on X: for each component index c < nextComp a closed set piece c, a label label c < nextLabel and an exponent a c; the values above nextComp are irrelevant (as for MonomialState).

• nextComp : ℕ

  Components are 0, …, nextComp - 1.

• nextLabel : ℕ

  Labels are 0, …, nextLabel - 1.

• piece : ℕ → TopologicalSpace.Closeds ↥X

  The closed set of a component (empty for a dead component).

• label : ℕ → ℕ

  The label of a component: the index of its member.

• a : ℕ → ℕ

  The exponent of a component.

• label_lt (c : ℕ) : c < self.nextComp → self.label c < self.nextLabel

Faces, the nerve and the state

def Hironaka.Monomial.PieceFamily.faceSet {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (T : Finset ℕ) : TopologicalSpace.Closeds ↥X

The closed set Z_T = ⋂_{c ∈ T} piece c of a set of components (⊤ = X for T = ∅).

Equations

• Φ.faceSet T = T.inf Φ.piece

theorem Hironaka.Monomial.PieceFamily.faceSet_anti {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {T T' : Finset ℕ} (h : T' ⊆ T) : Φ.faceSet T ≤ Φ.faceSet T'

theorem Hironaka.Monomial.PieceFamily.coe_faceSet {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (T : Finset ℕ) : ↑(Φ.faceSet T) = ⋂ c ∈ T, ↑(Φ.piece c)

theorem Hironaka.Monomial.PieceFamily.mem_faceSet {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {T : Finset ℕ} {x : ↥X} : x ∈ Φ.faceSet T ↔ ∀ c ∈ T, x ∈ Φ.piece c

noncomputable def Hironaka.Monomial.PieceFamily.nerve {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) : Finset (Finset ℕ)

The nerve of the piece family: the nonempty sets of components below nextComp with nonempty common intersection.

Equations

• Φ.nerve = {T ∈ (Finset.range Φ.nextComp).powerset | T.Nonempty ∧ Φ.faceSet T ≠ ⊥}

theorem Hironaka.Monomial.PieceFamily.mem_nerve {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {T : Finset ℕ} : T ∈ Φ.nerve ↔ T ⊆ Finset.range Φ.nextComp ∧ T.Nonempty ∧ Φ.faceSet T ≠ ⊥

@[reducible, inline]

abbrev Hironaka.Monomial.PieceFamily.IsValid {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (n m : ℕ) : Prop

The invariants of the combinatorial state (MonomialState.Valid) for the family's data: 1 ≤ m, faces nonempty, below nextComp, labels below nextLabel, the nerve down-closed, faces of size ≤ n with injective labels. Hironaka/Resolution/Algebraic/Monomial/Geometric/Nerve.lean discharges it from the geometric hypotheses (valid_of_realizes).

Equations

• Φ.IsValid n m = Hironaka.Monomial.MonomialState.Valid n m Φ.nextComp Φ.nextLabel Φ.label Φ.nerve

noncomputable def Hironaka.Monomial.PieceFamily.toState {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (n m : ℕ) (hV : Φ.IsValid n m) : MonomialState

The combinatorial state of a piece family: MonomialState.ofValid on the family's counters, labels, exponents and nerve, so that every data field of the state is the family's by rfl.

Equations

• Φ.toState n m hV = Hironaka.Monomial.MonomialState.ofValid n m Φ.nextComp Φ.nextLabel Φ.label Φ.a Φ.nerve hV

@[simp]

theorem Hironaka.Monomial.PieceFamily.toState_n {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {n m : ℕ} {hV : Φ.IsValid n m} : (Φ.toState n m hV).n = n

@[simp]

theorem Hironaka.Monomial.PieceFamily.toState_m {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {n m : ℕ} {hV : Φ.IsValid n m} : (Φ.toState n m hV).m = m

@[simp]

theorem Hironaka.Monomial.PieceFamily.toState_nextComp {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {n m : ℕ} {hV : Φ.IsValid n m} : (Φ.toState n m hV).nextComp = Φ.nextComp

@[simp]

theorem Hironaka.Monomial.PieceFamily.toState_nextLabel {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {n m : ℕ} {hV : Φ.IsValid n m} : (Φ.toState n m hV).nextLabel = Φ.nextLabel

@[simp]

theorem Hironaka.Monomial.PieceFamily.toState_label {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {n m : ℕ} {hV : Φ.IsValid n m} : (Φ.toState n m hV).label = Φ.label

@[simp]

theorem Hironaka.Monomial.PieceFamily.toState_a {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {n m : ℕ} {hV : Φ.IsValid n m} : (Φ.toState n m hV).a = Φ.a

@[simp]

theorem Hironaka.Monomial.PieceFamily.toState_nerve {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {n m : ℕ} {hV : Φ.IsValid n m} : (Φ.toState n m hV).nerve = Φ.nerve

def Hironaka.Monomial.PieceFamily.total {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (T : Finset ℕ) : ℕ

The sum a(T) of the exponents of a set of components (MonomialState.total on the family).

Equations

• Φ.total T = ∑ c ∈ T, Φ.a c

theorem Hironaka.Monomial.PieceFamily.toState_total {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {n m : ℕ} {hV : Φ.IsValid n m} (T : Finset ℕ) : (Φ.toState n m hV).total T = Φ.total T

Centres

noncomputable def Hironaka.Monomial.PieceFamily.faceIdeal {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (P : Finset ℕ) : X.IdealSheafData

The ideal sheaf of the closed subscheme Z_P = ⋂_{c ∈ P} piece c with its reduced structure: the sum of the vanishing ideal sheaves of the pieces (the scheme-theoretic intersection of reduced subschemes; Kollár's E^{j₁} ∩ ⋯ ∩ E^{j_r} of [Kol07, 111, Step 3.r]).

Equations

• Φ.faceIdeal P = ⨆ c ∈ P, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (Φ.piece c)

noncomputable def Hironaka.Monomial.PieceFamily.centerOf {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (S : Finset (Finset ℕ)) : X.IdealSheafData

The centre of a finset of faces Z_S = ⋃_{P ∈ S} Z_P, as the product of the ideal sheaves of the (pairwise disjoint, for a centre of the state) intersections Z_P.

Equations

• Φ.centerOf S = ∏ P ∈ S, Φ.faceIdeal P

The transition

def Hironaka.Monomial.PieceFamily.newComp {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (S : Finset (Finset ℕ)) (P : Finset ℕ) : ℕ

The new component of the face P of the centre S, numbered nextComp + rank S P as in MonomialState.newComp, so that the combinatorial and the geometric transitions allocate the same numbers.

Equations

• Φ.newComp S P = Φ.nextComp + Hironaka.Monomial.MonomialState.rank S P

theorem Hironaka.Monomial.PieceFamily.toState_newComp {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {n m : ℕ} {hV : Φ.IsValid n m} (S : Finset (Finset ℕ)) (P : Finset ℕ) : (Φ.toState n m hV).newComp S P = Φ.newComp S P

noncomputable def Hironaka.Monomial.PieceFamily.strictTransformCloseds {X : AlgebraicGeometry.Scheme} (D : X.IdealSheafData) (C : TopologicalSpace.Closeds ↥X) : TopologicalSpace.Closeds ↥D.blowUp

The strict transform of a closed set under the blow-up of X with centre D: the closure of the preimage of its part off the centre (the support of the strict transform of its vanishing ideal, coe_support_strictTransform of Hironaka/Resolution/Algebraic/Snc/DictionaryBoundary.lean).

Equations

• Hironaka.Monomial.PieceFamily.strictTransformCloseds D C = TopologicalSpace.Closeds.closure (⇑D.blowUpπ ⁻¹' (↑C \ ↑D.support))

noncomputable def Hironaka.Monomial.PieceFamily.blowUpPieces {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (S : Finset (Finset ℕ)) (m : ℕ) : PieceFamily (Φ.centerOf S).blowUp

The transition of the piece family under the blow-up of the centre S ([Kol07, Definition 65] and [Kol07, 111, Step 3.2 and 3.r]): the old pieces become their strict transforms, the face P ∈ S contributes the new piece π⁻¹(Z_P) at the index newComp S P with the new label nextLabel and the exponent a(P) − m; the label and exponent functions are those of MonomialState.blowUp.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Hironaka.Monomial.PieceFamily.blowUpPieces_nextComp {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {m : ℕ} (S : Finset (Finset ℕ)) : (Φ.blowUpPieces S m).nextComp = Φ.nextComp + S.card

@[simp]

theorem Hironaka.Monomial.PieceFamily.blowUpPieces_nextLabel {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {m : ℕ} (S : Finset (Finset ℕ)) : (Φ.blowUpPieces S m).nextLabel = Φ.nextLabel + 1

theorem Hironaka.Monomial.PieceFamily.blowUpPieces_piece_of_lt {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {m : ℕ} (S : Finset (Finset ℕ)) {c : ℕ} (hc : c < Φ.nextComp) : (Φ.blowUpPieces S m).piece c = strictTransformCloseds (Φ.centerOf S) (Φ.piece c)

theorem Hironaka.Monomial.PieceFamily.blowUpPieces_label_of_lt {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {m : ℕ} (S : Finset (Finset ℕ)) {c : ℕ} (hc : c < Φ.nextComp) : (Φ.blowUpPieces S m).label c = Φ.label c

theorem Hironaka.Monomial.PieceFamily.blowUpPieces_a_of_lt {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {m : ℕ} (S : Finset (Finset ℕ)) {c : ℕ} (hc : c < Φ.nextComp) : (Φ.blowUpPieces S m).a c = Φ.a c

theorem Hironaka.Monomial.PieceFamily.blowUpPieces_label_newComp {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {m : ℕ} (S : Finset (Finset ℕ)) (P : Finset ℕ) : (Φ.blowUpPieces S m).label (Φ.newComp S P) = Φ.nextLabel

theorem Hironaka.Monomial.PieceFamily.blowUpPieces_piece_newComp {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {m : ℕ} (S : Finset (Finset ℕ)) {P : Finset ℕ} (hP : P ∈ S) : (Φ.blowUpPieces S m).piece (Φ.newComp S P) = (Φ.faceSet P).preimage ⋯

The new piece of a face P ∈ S: the preimage π⁻¹(Z_P).

theorem Hironaka.Monomial.PieceFamily.blowUpPieces_a_newComp {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {m : ℕ} (S : Finset (Finset ℕ)) {P : Finset ℕ} (hP : P ∈ S) : (Φ.blowUpPieces S m).a (Φ.newComp S P) = Φ.total P - m

The new piece of a face P ∈ S has the exponent a(P) − m.

theorem Hironaka.Monomial.PieceFamily.toState_blowUpPieces_of_nerve_eq {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {n m : ℕ} {hV : Φ.IsValid n m} (S : Finset (Finset ℕ)) {hV' : (Φ.blowUpPieces S m).IsValid n m} (h : (Φ.blowUpPieces S m).nerve = ((Φ.toState n m hV).blowUp S).nerve) : (Φ.blowUpPieces S m).toState n m hV' = (Φ.toState n m hV).blowUp S

Every data field of the transported state other than the nerve agrees with MonomialState.blowUp by rfl (the formulas are the same); the nerve is the content of nerve_blowUpPieces in Hironaka/Resolution/Algebraic/Monomial/Geometric/Kernel.lean, and MonomialState.ext (proof fields by proof irrelevance) gives the literal equality of states.

The exponent function and the face through a point

noncomputable def Hironaka.Monomial.PieceFamily.faceAt {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (x : ↥X) : Finset ℕ

The set of components whose piece passes through x.

Equations

• Φ.faceAt x = {c ∈ Finset.range Φ.nextComp | x ∈ Φ.piece c}

theorem Hironaka.Monomial.PieceFamily.mem_faceAt {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {x : ↥X} {c : ℕ} : c ∈ Φ.faceAt x ↔ c < Φ.nextComp ∧ x ∈ Φ.piece c

noncomputable def Hironaka.Monomial.PieceFamily.exponentAt {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (x : ↥X) : ℕ

The exponent function of the marked monomial ideal E.monomial Φ.exponentAt (one exponent per generic point of a member, the convention of Hironaka/Resolution/Algebraic/MarkedOrderReduction/MonomialPart.lean): the largest exponent of a piece through x. At a generic point of a member of a realised snc boundary exactly one piece passes.

Equations

• Φ.exponentAt x = (Φ.faceAt x).sup Φ.a

Realisation of a boundary

structure Hironaka.Monomial.PieceFamily.Realizes {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (E : X.DivisorFamily) (e : E.ι ≃o Fin Φ.nextLabel) : Prop

The piece family realises the boundary E through the label isomorphism e: every member is the union of the pieces of its label, and pieces of one label are pairwise disjoint (so every irreducible component of a member lies in exactly one piece).

• support_eq (j : E.ι) : (E.component j).support = {c ∈ Finset.range Φ.nextComp | Φ.label c = ↑(e j)}.sup Φ.piece
• disjoint (c c' : ℕ) : c < Φ.nextComp → c' < Φ.nextComp → c ≠ c' → Φ.label c = Φ.label c' → Disjoint (Φ.piece c) (Φ.piece c')

structure Hironaka.Monomial.PieceFamily.RefinesAlong {X Y : AlgebraicGeometry.Scheme} (Φ' : PieceFamily Y) (h : Y ⟶ X) (ρ : ℕ → ℕ) (Φ : PieceFamily X) : Prop

The piece family Φ' on Y refines Φ along h : Y ⟶ X through the parent map ρ: the same label count, labels and exponents through ρ, every piece of Φ' inside the preimage of its parent, and the preimage of every piece of Φ the union of its children (pairwise disjoint: the children are the irreducible components of the preimage). The geometric form of MonomialState.Refines, used for smooth surjections h in Hironaka/Resolution/Algebraic/Monomial/Geometric/Refinement.lean.

• nextLabel_eq : Φ'.nextLabel = Φ.nextLabel
• lt (c : ℕ) : c < Φ'.nextComp → ρ c < Φ.nextComp
• label_eq (c : ℕ) : c < Φ'.nextComp → Φ.label (ρ c) = Φ'.label c
• a_eq (c : ℕ) : c < Φ'.nextComp → Φ.a (ρ c) = Φ'.a c
• piece_le (c : ℕ) : c < Φ'.nextComp → Φ'.piece c ≤ (Φ.piece (ρ c)).preimage ⋯
• preimage_eq (c : ℕ) : c < Φ.nextComp → (Φ.piece c).preimage ⋯ = {c' ∈ Finset.range Φ'.nextComp | ρ c' = c}.sup Φ'.piece
• disjoint (c c' : ℕ) : c < Φ'.nextComp → c' < Φ'.nextComp → c ≠ c' → ρ c = ρ c' → Disjoint (Φ'.piece c) (Φ'.piece c')

The restriction of the state along a morphism

noncomputable def Hironaka.Monomial.PieceFamily.restrictNerve {X Y : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (h : Y ⟶ X) : Finset (Finset ℕ)

The faces of the nerve whose face set meets the image of h : Y ⟶ X: the nerve of the boundary h⁻¹E when the pieces stay irreducible under h.

Equations

• Φ.restrictNerve h = {T ∈ Φ.nerve | (Φ.faceSet T).preimage ⋯ ≠ ⊥}

theorem Hironaka.Monomial.PieceFamily.mem_restrictNerve {X Y : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (h : Y ⟶ X) {T : Finset ℕ} : T ∈ Φ.restrictNerve h ↔ T ∈ Φ.nerve ∧ (Φ.faceSet T).preimage ⋯ ≠ ⊥

theorem Hironaka.Monomial.PieceFamily.restrictNerve_subset {X Y : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (h : Y ⟶ X) : Φ.restrictNerve h ⊆ Φ.nerve

theorem Hironaka.Monomial.PieceFamily.valid_restrictNerve {X Y : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (h : Y ⟶ X) {n m : ℕ} (hV : Φ.IsValid n m) : MonomialState.Valid n m Φ.nextComp Φ.nextLabel Φ.label (Φ.restrictNerve h)

The restricted data are Valid: a subfamily of a valid nerve, down-closed because a smaller face has a larger face set (faceSet_anti), whose preimage is then nonempty too.

noncomputable def Hironaka.Monomial.PieceFamily.restrictState {X Y : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (h : Y ⟶ X) (n m : ℕ) (hV : Φ.IsValid n m) : MonomialState

The state of Φ restricted along h : Y ⟶ X: MonomialState.ofValid on the family's counters, labels and exponents and the faces meeting the image of h. It is Sub the state toState (its data fields are toState's by rfl), and it is the state that a refining family on Y refines (Hironaka/Resolution/Algebraic/Monomial/Geometric/Refinement.lean).

Equations

• Φ.restrictState h n m hV = Hironaka.Monomial.MonomialState.ofValid n m Φ.nextComp Φ.nextLabel Φ.label Φ.a (Φ.restrictNerve h) ⋯

@[simp]

theorem Hironaka.Monomial.PieceFamily.restrictState_n {X Y : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (h : Y ⟶ X) {n m : ℕ} {hV : Φ.IsValid n m} : (Φ.restrictState h n m hV).n = n

@[simp]

theorem Hironaka.Monomial.PieceFamily.restrictState_m {X Y : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (h : Y ⟶ X) {n m : ℕ} {hV : Φ.IsValid n m} : (Φ.restrictState h n m hV).m = m

@[simp]

theorem Hironaka.Monomial.PieceFamily.restrictState_nextComp {X Y : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (h : Y ⟶ X) {n m : ℕ} {hV : Φ.IsValid n m} : (Φ.restrictState h n m hV).nextComp = Φ.nextComp

@[simp]

theorem Hironaka.Monomial.PieceFamily.restrictState_nextLabel {X Y : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (h : Y ⟶ X) {n m : ℕ} {hV : Φ.IsValid n m} : (Φ.restrictState h n m hV).nextLabel = Φ.nextLabel

@[simp]

theorem Hironaka.Monomial.PieceFamily.restrictState_label {X Y : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (h : Y ⟶ X) {n m : ℕ} {hV : Φ.IsValid n m} : (Φ.restrictState h n m hV).label = Φ.label

@[simp]

theorem Hironaka.Monomial.PieceFamily.restrictState_a {X Y : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (h : Y ⟶ X) {n m : ℕ} {hV : Φ.IsValid n m} : (Φ.restrictState h n m hV).a = Φ.a

@[simp]

theorem Hironaka.Monomial.PieceFamily.restrictState_nerve {X Y : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (h : Y ⟶ X) {n m : ℕ} {hV : Φ.IsValid n m} : (Φ.restrictState h n m hV).nerve = Φ.restrictNerve h

The input piece families

def Hironaka.Monomial.PieceFamily.Components {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) : Type u

The irreducible components of the members of E: the generic points of their supports (finite on a Noetherian scheme), tagged by their member.

Equations

• Hironaka.Monomial.PieceFamily.Components E = ((j : E.ι) × ↑(E.component j).support.genericPoints)

noncomputable def Hironaka.Monomial.PieceFamily.ofDivisorFamily {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) {k L : ℕ} (a : ↥X → ℕ) (e : E.ι ≃o Fin L) (σ : Fin k ≃ Components E) : PieceFamily X

The input piece family of [Kol07, 111, Step 3]: the irreducible components of the members, enumerated by σ, with the label of their member through e and the exponent a at their generic point. Each component carries its own exponent, the fine form of [Kol07, Definition–Lemma 110] (Hironaka/Resolution/Algebraic/MarkedOrderReduction/MonomialPart.lean).

Equations

• One or more equations did not get rendered due to their size.

The label isomorphism along the total transform

def Hironaka.Monomial.finSuccFun (L : ℕ) (x : Fin L ⊕ₗ PUnit.{v + 1}) : Fin (L + 1)

Fin L ⊕ₗ PUnit → Fin (L + 1): inl i ↦ castSucc i, inr () ↦ last L.

Equations

• Hironaka.Monomial.finSuccFun L x = Sum.elim Fin.castSucc (fun (x : PUnit.{?u.1 + 1}) => Fin.last L) (ofLex x)

theorem Hironaka.Monomial.finSuccFun_strictMono (L : ℕ) : StrictMono (finSuccFun L)

theorem Hironaka.Monomial.finSuccFun_surjective (L : ℕ) : Function.Surjective (finSuccFun L)

noncomputable def Hironaka.Monomial.finSuccOrderIso (L : ℕ) : Fin L ⊕ₗ PUnit.{v + 1} ≃o Fin (L + 1)

Fin L ⊕ₗ PUnit ≃o Fin (L + 1): inl i ↦ castSucc i, inr () ↦ last L.

Equations

• Hironaka.Monomial.finSuccOrderIso L = StrictMono.orderIsoOfSurjective (Hironaka.Monomial.finSuccFun L) ⋯ ⋯

noncomputable def Hironaka.Monomial.extendIso {ι : Type u} [LinearOrder ι] {L : ℕ} (e : ι ≃o Fin L) : ι ⊕ₗ PUnit.{u + 1} ≃o Fin (L + 1)

The label isomorphism extended along the index type E.ι ⊕ₗ PUnit of the total transform: the old labels through e, the exceptional divisor inr () to the new label L, added as the last divisor as in [Kol07, Definition 65].

Equations

• Hironaka.Monomial.extendIso e = (e.sumLexCongr (OrderIso.refl PUnit.{?u.1 + 1})).trans (Hironaka.Monomial.finSuccOrderIso L)

theorem Hironaka.Monomial.extendIso_inl {ι : Type u} [LinearOrder ι] {L : ℕ} (e : ι ≃o Fin L) (i : ι) : (extendIso e) (toLex (Sum.inl i)) = (e i).castSucc

theorem Hironaka.Monomial.extendIso_inr {ι : Type u} [LinearOrder ι] {L : ℕ} (e : ι ≃o Fin L) : (extendIso e) (toLex (Sum.inr PUnit.unit)) = Fin.last L

The realisation: the fold of a list of centres

noncomputable def Hironaka.Monomial.PieceFamily.realizeAux {X : AlgebraicGeometry.Scheme} : PieceFamily X → ℕ → List (Finset (Finset ℕ)) → X.BlowUpSequence

The fold of a list of centres into a blow-up sequence, carrying the piece family: structural recursion on the list, no recursion on schemes. The centre at each step is Z_S of the current family and the family is transported by blowUpPieces.

Equations

• x✝¹.realizeAux x✝ [] = AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝²
• x✝¹.realizeAux x✝ (S :: L) = AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝² (x✝¹.centerOf S) ((x✝¹.blowUpPieces S x✝).realizeAux x✝ L)

noncomputable def Hironaka.Monomial.PieceFamily.stagePieces {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (m : ℕ) (L : List (Finset (Finset ℕ))) (i : Fin ((Φ.realizeAux m L).length + 1)) : PieceFamily ((Φ.realizeAux m L).stage i)

The piece family at stage i of the fold.

Equations

• x✝¹.stagePieces x✝ [] x_7 = x✝¹
• x✝¹.stagePieces x✝ (head :: tail) ⟨0, isLt⟩ = x✝¹
• x✝¹.stagePieces x✝ (S :: L) ⟨j.succ, h⟩ = (x✝¹.blowUpPieces S x✝).stagePieces x✝ L ⟨j, ⋯⟩

@[simp]

theorem Hironaka.Monomial.PieceFamily.realizeAux_nil {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (m : ℕ) : Φ.realizeAux m [] = AlgebraicGeometry.Scheme.BlowUpSequence.nil X

@[simp]

theorem Hironaka.Monomial.PieceFamily.realizeAux_cons {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (m : ℕ) (S : Finset (Finset ℕ)) (L : List (Finset (Finset ℕ))) : Φ.realizeAux m (S :: L) = AlgebraicGeometry.Scheme.BlowUpSequence.cons X (Φ.centerOf S) ((Φ.blowUpPieces S m).realizeAux m L)

theorem Hironaka.Monomial.PieceFamily.realizeAux_length {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (m : ℕ) (L : List (Finset (Finset ℕ))) : (Φ.realizeAux m L).length = L.length

theorem Hironaka.Monomial.PieceFamily.stagePieces_nil {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (m : ℕ) (i : Fin ((Φ.realizeAux m []).length + 1)) : Φ.stagePieces m [] i = Φ

theorem Hironaka.Monomial.PieceFamily.stagePieces_cons_zero {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (m : ℕ) (S : Finset (Finset ℕ)) (L : List (Finset (Finset ℕ))) (h : 0 < (Φ.realizeAux m (S :: L)).length + 1) : Φ.stagePieces m (S :: L) ⟨0, h⟩ = Φ

theorem Hironaka.Monomial.PieceFamily.stagePieces_succ {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (m : ℕ) (S : Finset (Finset ℕ)) (L : List (Finset (Finset ℕ))) (j : ℕ) (h : j + 1 < (Φ.realizeAux m (S :: L)).length + 1) : Φ.stagePieces m (S :: L) ⟨j + 1, h⟩ = (Φ.blowUpPieces S m).stagePieces m L ⟨j, ⋯⟩

noncomputable def Hironaka.Monomial.PieceFamily.stageIso {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (m : ℕ) (E : X.DivisorFamily) : E.ι ≃o Fin Φ.nextLabel → (L : List (Finset (Finset ℕ))) → (i : Fin ((Φ.realizeAux m L).length + 1)) → ((Φ.realizeAux m L).totalTransformSeq E i).ι ≃o Fin (Φ.stagePieces m L i).nextLabel

The label isomorphism at stage i of the fold: e extended by extendIso once per blow-up.

Equations

• x✝³.stageIso x✝² x✝¹ x✝ [] x_11 = x✝
• x✝³.stageIso x✝² x✝¹ x✝ (head :: tail) ⟨0, isLt⟩ = x✝
• x✝³.stageIso x✝² x✝¹ x✝ (S :: L) ⟨j.succ, h⟩ = (x✝³.blowUpPieces S x✝²).stageIso x✝² (x✝¹.totalTransform (x✝³.centerOf S)) (Hironaka.Monomial.extendIso x✝) L ⟨j, ⋯⟩

noncomputable def Hironaka.Monomial.PieceFamily.realize {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (n m : ℕ) (hV : Φ.IsValid n m) : X.BlowUpSequence

The geometric Step 3 of [Kol07, 111]: the fold of the combinatorial run (step3 (toState Φ)).2 into a blow-up sequence of X.

Equations

• Φ.realize n m hV = Φ.realizeAux m (Φ.toState n m hV).step3.2