Renumbering of a piece family

The geometric Step 3 PieceFamily.realize depends on a piece family only through its pieces (as closed sets), their exponents and the order of their labels. This module defines the relation under which the run is shown invariant in Hironaka/Resolution/Algebraic/Monomial/Geometric/RealizeCongr.lean: the relation MonomialState.Rel ρ σ D P of Hironaka/Resolution/Algebraic/Monomial/Restrict/Rename.lean lifted to piece families. Φ.Rel ρ σ Φ' says that Φ' is Φ renumbered: the live components of Φ are re-embedded by the strictly monotone ρ (so that the order of the component indices, which numbers the new components of a blow-up through rank, is kept), the labels by the strictly monotone σ (Kollár's choice reads label tuples lexicographically, which an order embedding of labels preserves), with the same pieces and exponents, and the nerve of Φ' the image of the nerve of Φ; Φ' may carry further dead components (empty pieces) and unused labels.

The two uses: the deletion of empty members of a boundary (an empty member has no components, so the surviving components keep their relative order and the labels re-embed; Hironaka/Resolution/Algebraic/MarkedOrderReduction/SmoothStep3.lean), and the independence of the run from the enumeration of the components whenever the two enumerations are order-compatible. A congruence tolerating arbitrary permutations of the components is not proved; nothing needs it. Not in the sources: Kollár's E^j are indexed by a fixed ordered set and the question does not arise.

structure Hironaka.Monomial.PieceFamily.Rel {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (ρ σ : ℕ → ℕ) (Φ' : PieceFamily X) : Prop

Φ' is Φ renumbered by ρ on components and σ on labels: both strictly monotone on the live ranges and landing below Φ''s counters, the same pieces and exponents, the labels through σ, and the nerve of Φ' the image of the nerve of Φ (so every further component of Φ' is dead). The relation MonomialState.Rel on piece families.

• mono : StrictMonoOn ρ (Set.Iio Φ.nextComp)

  ρ is strictly monotone on the live components of Φ.

• lt (c : ℕ) : c < Φ.nextComp → ρ c < Φ'.nextComp

  ρ lands below Φ''s component counter.

• piece_eq (c : ℕ) : c < Φ.nextComp → Φ'.piece (ρ c) = Φ.piece c

  The pieces are the same closed sets.

• a_eq (c : ℕ) : c < Φ.nextComp → Φ'.a (ρ c) = Φ.a c

  The exponents are the same.

• label_eq (c : ℕ) : c < Φ.nextComp → Φ'.label (ρ c) = σ (Φ.label c)

  The labels are renamed by σ.

• σmono : StrictMonoOn σ (Set.Iio Φ.nextLabel)

  σ is strictly monotone on the labels of Φ.

• σlt (ℓ : ℕ) : ℓ < Φ.nextLabel → σ ℓ < Φ'.nextLabel

  σ lands below Φ''s label counter.

• nerve_eq : Φ'.nerve = Finset.image (Finset.image ρ) Φ.nerve

  The nerve of Φ' is the image of the nerve of Φ.

theorem Hironaka.Monomial.PieceFamily.Rel.refl {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) : Φ.Rel id id Φ

The identity renumbering.