The input piece family, the face through a point, the centres of the fold

Three facts about the piece families of Hironaka/Resolution/Algebraic/Monomial/Geometric/Pieces.lean, not in the sources:

• ofDivisorFamily_realizes: the family of the irreducible components of the members realises E, the input of [Kol07, 111, Step 3]. A closed set of a sober space is the union of the closures of its generic points, and two irreducible components of a member through a common point coincide because the member's stalk ideal is prime (the member is a regular subscheme, [Kol07, Definition 24] (1)): the reduced components through the point are minimal primes over it, hence equal (Hironaka.Sequence.eq_of_specializes_of_isRegular of Hironaka/Resolution/Algebraic/Snc/DictionaryRegular.lean).
• faceAt_mem_nerve: the set of pieces through a point of E is a face.
• realizeAux_center: the i-th centre of the fold is the centre of the i-th listed finset of faces, read on the stage-i family, by structural recursion on the list.

The first is what makes step3Family of Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step3Input.lean a realising family; the third is how the centres of the geometric Step 3 are read off.

The face through a point

theorem Hironaka.Monomial.PieceFamily.faceAt_subset_range {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (x : ↥X) : Φ.faceAt x ⊆ Finset.range Φ.nextComp

theorem Hironaka.Monomial.PieceFamily.mem_faceSet_faceAt {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (x : ↥X) : x ∈ Φ.faceSet (Φ.faceAt x)

theorem Hironaka.Monomial.PieceFamily.faceAt_mem_nerve {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} (hΦ : Φ.Realizes E e) {x : ↥X} (hx : x ∈ E.support) : Φ.faceAt x ∈ Φ.nerve

The set of pieces through a point of E is a face of the nerve: some piece passes through the point (Realizes.support_eq).

The input piece family realises E

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

The input piece family of [Kol07, 111, Step 3], the irreducible components of the members enumerated by σ, realises E: each member is the union of its irreducible components and two irreducible components of a regular divisor are disjoint.

The centres of the fold

theorem Hironaka.Monomial.PieceFamily.realizeAux_center {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (m : ℕ) (L : List (Finset (Finset ℕ))) (i : Fin (Φ.realizeAux m L).length) : (Φ.realizeAux m L).center i = (Φ.stagePieces m L i.castSucc).centerOf (L.get (Fin.cast ⋯ i))

The i-th centre of the fold is the centre of the i-th listed finset of faces, read on the stage-i piece family.