The realise congruence

The geometric Step 3 PieceFamily.realize is invariant under a renumbering of the piece family (PieceFamily.Rel ρ σ Φ Φ' of Hironaka/Resolution/Algebraic/Monomial/Geometric/Congruence.lean): the same pieces and exponents, the components re-embedded by the strictly monotone ρ, the labels by the strictly monotone σ. Not in the sources; Kollár's Step 3 reads label tuples lexicographically and face sums, and puts the new divisor last, so an order-preserving renumbering cannot change the run. The proof has a combinatorial half and a geometric half.

• Combinatorial half, the lockstep of the two runs (RunRel). The relation MonomialState.Rel is preserved by a blow-up (Rel.blowUp of Hironaka/Resolution/Algebraic/Monomial/Restrict/Extend.lean, with the renumbering extended by extendComp/extendLabel), and Kollár's choice is transported (Rel.choice_eq). The runs of Step 3 on two related states therefore proceed in lockstep: at each step the centre of the renumbered state is the image of the centre of the original one under the current renumbering, and the renumbering extends. RunRel ρ σ D P L L' ρ' σ' D' P' records this chain (the pattern of phase_restrict with the subnerve equal to the whole nerve); step3_runRel runs it along Step 3, and step3_rel is the summary: an order embedding ρ' extending ρ with (step3 P).2 = (step3 D).2.map (image (image ρ')) and Rel ρ' σ' between the final states.
• Geometric half, the fold. Along the lockstep the two piece families keep the same pieces (PieceEq): the old pieces become their strict transforms under the same centre (the centre of a finset of faces is the vanishing ideal of the union of their face sets, PieceEq.centerOf), the new pieces are the preimages of the same face sets, and the counters, labels and exponents of the families are those of the states (Agrees). The two folds then produce the same blow-up sequence (realizeAux_runRel). The two tails live over the blow-ups at the two centres, which are equal but not syntactically so; the transport along that equality is by the cast* lemmas below, each proved by subst (nothing about the schemes is used).

Nothing geometric enters: realize is a function of the state and of the pieces as closed sets, so the congruence holds for piece families on any scheme. It is used in Hironaka/Resolution/Algebraic/MarkedOrderReduction/SmoothStep3.lean for the deletion of empty boundary members.

The lockstep of two runs related by a renumbering

inductive Hironaka.Monomial.MonomialState.RunRel (ρ σ : ℕ → ℕ) : MonomialState → MonomialState → List (Finset (Finset ℕ)) → List (Finset (Finset ℕ)) → (ρ' σ' : ℕ → ℕ) → MonomialState → MonomialState → Prop

The lockstep of two runs (the pattern of phase_restrict): from the states D, P related by Rel ρ σ, the lists L (on D) and L' (on P) proceed centre by centre, each centre of P the image of the centre of D under the current renumbering, the renumbering extended by extendComp/extendLabel at each blow-up, ending at the states D', P' with the renumbering ρ', σ'.

• nil (ρ σ : ℕ → ℕ) (D P : MonomialState) : RunRel ρ σ D P [] [] ρ σ D P
• cons {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) (S : Finset (Finset ℕ)) (hSD : S ⊆ D.nerve) (hS0 : ∀ Q ∈ S, Q.Nonempty) {L L' : List (Finset (Finset ℕ))} {ρ' σ' : ℕ → ℕ} {D' P' : MonomialState} (hL : RunRel (extendComp ρ D P S (Finset.image (Finset.image ρ) S)) (extendLabel σ D P) (D.blowUp S) (P.blowUp (Finset.image (Finset.image ρ) S)) L L' ρ' σ' D' P') : RunRel ρ σ D P (S :: L) (Finset.image (Finset.image ρ) S :: L') ρ' σ' D' P'

theorem Hironaka.Monomial.MonomialState.RunRel.cons' {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) (S : Finset (Finset ℕ)) (hSD : S ⊆ D.nerve) (hS0 : ∀ Q ∈ S, Q.Nonempty) {S' : Finset (Finset ℕ)} (hS' : S' = Finset.image (Finset.image ρ) S) {L L' : List (Finset (Finset ℕ))} {ρ' σ' : ℕ → ℕ} {D' P' : MonomialState} (hL : RunRel (extendComp ρ D P S S') (extendLabel σ D P) (D.blowUp S) (P.blowUp S') L L' ρ' σ' D' P') : RunRel ρ σ D P (S :: L) (S' :: L') ρ' σ' D' P'

RunRel.cons with the image centre given up to an equation.

theorem Hironaka.Monomial.MonomialState.RunRel.append {ρ σ ρ₁ σ₁ ρ₂ σ₂ : ℕ → ℕ} {D P D₁ P₁ D₂ P₂ : MonomialState} {L₁ L₁' L₂ L₂' : List (Finset (Finset ℕ))} (h₁ : RunRel ρ σ D P L₁ L₁' ρ₁ σ₁ D₁ P₁) (h₂ : RunRel ρ₁ σ₁ D₁ P₁ L₂ L₂' ρ₂ σ₂ D₂ P₂) : RunRel ρ σ D P (L₁ ++ L₂) (L₁' ++ L₂') ρ₂ σ₂ D₂ P₂

The lockstep composes.

theorem Hironaka.Monomial.MonomialState.RunRel.filter_image_eq {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {S : Finset (Finset ℕ)} (hSD : S ⊆ D.nerve) : {x ∈ Finset.image (Finset.image ρ) S | x ∈ P.nerve} = Finset.image (Finset.image ρ) S

The faces of the image centre lie in the nerve of the renumbered state.

theorem Hironaka.Monomial.MonomialState.RunRel.image_nonempty' {ρ : ℕ → ℕ} {S : Finset (Finset ℕ)} (hS0 : ∀ Q ∈ S, Q.Nonempty) (Q : Finset ℕ) : Q ∈ Finset.image (Finset.image ρ) S → Q.Nonempty

The images of nonempty faces are nonempty.

theorem Hironaka.Monomial.MonomialState.RunRel.rel_end {ρ σ ρ' σ' : ℕ → ℕ} {D P D' P' : MonomialState} {L L' : List (Finset (Finset ℕ))} (hr : RunRel ρ σ D P L L' ρ' σ' D' P') (h : Rel ρ σ D P) : Rel ρ' σ' D' P'

The renumbering persists along the lockstep (Rel.blowUp at every step).

theorem Hironaka.Monomial.MonomialState.RunRel.agree {ρ σ ρ' σ' : ℕ → ℕ} {D P D' P' : MonomialState} {L L' : List (Finset (Finset ℕ))} (hr : RunRel ρ σ D P L L' ρ' σ' D' P') (c : ℕ) : c < D.nextComp → ρ' c = ρ c

The final renumbering agrees with the initial one on the initial components.

theorem Hironaka.Monomial.MonomialState.RunRel.agree_label {ρ σ ρ' σ' : ℕ → ℕ} {D P D' P' : MonomialState} {L L' : List (Finset (Finset ℕ))} (hr : RunRel ρ σ D P L L' ρ' σ' D' P') (ℓ : ℕ) : ℓ < D.nextLabel → σ' ℓ = σ ℓ

The final label renumbering agrees with the initial one on the initial labels.

theorem Hironaka.Monomial.MonomialState.RunRel.map_eq {ρ σ ρ' σ' : ℕ → ℕ} {D P D' P' : MonomialState} {L L' : List (Finset (Finset ℕ))} (hr : RunRel ρ σ D P L L' ρ' σ' D' P') : L' = List.map (fun (S : Finset (Finset ℕ)) => Finset.image (Finset.image ρ') S) L

The renumbered run is the image of the run under the final renumbering (which agrees with every intermediate one on the components then present).

The lockstep along a phase and along Step 3

theorem Hironaka.Monomial.MonomialState.phase_runRel (r : ℕ) (P : MonomialState) (hsP : ∀ s < r, P.Star s) (D : MonomialState) (ρ σ : ℕ → ℕ) : Rel ρ σ D P → ∀ (hsD : ∀ s < r, D.Star s), ∃ (ρ' : ℕ → ℕ) (σ' : ℕ → ℕ), RunRel ρ σ D P (phase r D hsD).2 (phase r P hsP).2 ρ' σ' (phase r D hsD).1 (phase r P hsP).1

A phase of Step 3 on two states related by a renumbering proceeds in lockstep (phase_restrict with the subnerve the whole nerve).

theorem Hironaka.Monomial.MonomialState.phases_runRel (k r : ℕ) (P : MonomialState) (hsP : ∀ s < r, P.Star s) (D : MonomialState) (ρ σ : ℕ → ℕ) : Rel ρ σ D P → ∀ (hsD : ∀ s < r, D.Star s), ∃ (ρ' : ℕ → ℕ) (σ' : ℕ → ℕ), RunRel ρ σ D P (phases k r D hsD).2 (phases k r P hsP).2 ρ' σ' (phases k r D hsD).1 (phases k r P hsP).1

The phases r, …, r + k − 1 in lockstep.

theorem Hironaka.Monomial.MonomialState.step3_runRel {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) : ∃ (ρ' : ℕ → ℕ) (σ' : ℕ → ℕ), RunRel ρ σ D P D.step3.2 P.step3.2 ρ' σ' D.step3.1 P.step3.1

Step 3 on two states related by a renumbering proceeds in lockstep.

theorem Hironaka.Monomial.MonomialState.step3_rel {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) : ∃ (ρ' : ℕ → ℕ) (σ' : ℕ → ℕ), (∀ c < D.nextComp, ρ' c = ρ c) ∧ (∀ ℓ < D.nextLabel, σ' ℓ = σ ℓ) ∧ Rel ρ' σ' D.step3.1 P.step3.1 ∧ P.step3.2 = List.map (fun (S : Finset (Finset ℕ)) => Finset.image (Finset.image ρ') S) D.step3.2

The run on a renumbered state is the image of the run, under a renumbering ρ' extending ρ (and σ' extending σ), with the final states again related.

Families following states

structure Hironaka.Monomial.PieceFamily.Agrees {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (D : MonomialState) (m : ℕ) : Prop

The counters, labels and exponents of a piece family are those of a state (with the mark m): the invariant that lets the state-level renumbering drive the geometric fold.

• nextComp_eq : Φ.nextComp = D.nextComp

  The component counter.

• nextLabel_eq : Φ.nextLabel = D.nextLabel

  The label counter.

• label_eq : Φ.label = D.label

  The labels.

• a_eq : Φ.a = D.a

  The exponents.

• m_eq : D.m = m

  The mark.

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

A family agrees with its own state.

theorem Hironaka.Monomial.PieceFamily.Agrees.blowUpPieces {X : AlgebraicGeometry.Scheme} {Φ : PieceFamily X} {D : MonomialState} {m : ℕ} (h : Φ.Agrees D m) (S : Finset (Finset ℕ)) : (Φ.blowUpPieces S m).Agrees (D.blowUp S) m

The agreement passes through a blow-up: blowUpPieces and MonomialState.blowUp use the same formulas for the counters, labels and exponents.

Families with the same pieces along a renumbering

def Hironaka.Monomial.PieceFamily.PieceEq {X : AlgebraicGeometry.Scheme} (ρ : ℕ → ℕ) (Φ Φ' : PieceFamily X) : Prop

The pieces of Φ' at the renumbered indices are the pieces of Φ.

Equations

• Hironaka.Monomial.PieceFamily.PieceEq ρ Φ Φ' = ∀ c < Φ.nextComp, ρ c < Φ'.nextComp ∧ Φ'.piece (ρ c) = Φ.piece c

theorem Hironaka.Monomial.PieceFamily.PieceEq.faceSet {X : AlgebraicGeometry.Scheme} {ρ : ℕ → ℕ} {Φ Φ' : PieceFamily X} (h : PieceEq ρ Φ Φ') {T : Finset ℕ} (hT : ∀ c ∈ T, c < Φ.nextComp) : Φ'.faceSet (Finset.image ρ T) = Φ.faceSet T

The face set of the image of a set of live components is the face set of the set.

theorem Hironaka.Monomial.PieceFamily.PieceEq.faceIdeal {X : AlgebraicGeometry.Scheme} {ρ : ℕ → ℕ} {Φ Φ' : PieceFamily X} (h : PieceEq ρ Φ Φ') {T : Finset ℕ} (hT : ∀ c ∈ T, c < Φ.nextComp) : Φ'.faceIdeal (Finset.image ρ T) = Φ.faceIdeal T

The face ideal of the image of a live face is the face ideal of the face.

theorem Hironaka.Monomial.PieceFamily.PieceEq.centerOf {X : AlgebraicGeometry.Scheme} {ρ : ℕ → ℕ} {Φ Φ' : PieceFamily X} (h : PieceEq ρ Φ Φ') (hinj : Set.InjOn ρ (Set.Iio Φ.nextComp)) {S : Finset (Finset ℕ)} (hS : ∀ Q ∈ S, ∀ c ∈ Q, c < Φ.nextComp) : Φ'.centerOf (Finset.image (Finset.image ρ) S) = Φ.centerOf S

The centre of the image of a finset of live faces is the centre of the finset.

Transport along an equality of centres

def Hironaka.Monomial.PieceFamily.castFamily {X : AlgebraicGeometry.Scheme} {Z Z' : X.IdealSheafData} (hZ : Z = Z') (Ψ : PieceFamily Z.blowUp) : PieceFamily Z'.blowUp

A piece family on the blow-up at Z, read on the blow-up at Z' = Z.

Equations

• Hironaka.Monomial.PieceFamily.castFamily hZ Ψ = hZ ▸ Ψ

def Hironaka.Monomial.PieceFamily.castCloseds {X : AlgebraicGeometry.Scheme} {Z Z' : X.IdealSheafData} (hZ : Z = Z') (C : TopologicalSpace.Closeds ↥Z.blowUp) : TopologicalSpace.Closeds ↥Z'.blowUp

A closed set of the blow-up at Z, read on the blow-up at Z' = Z.

Equations

• Hironaka.Monomial.PieceFamily.castCloseds hZ C = hZ ▸ C

def Hironaka.Monomial.PieceFamily.castSeq {X : AlgebraicGeometry.Scheme} {Z Z' : X.IdealSheafData} (hZ : Z = Z') (T : Z.blowUp.BlowUpSequence) : Z'.blowUp.BlowUpSequence

A blow-up sequence of the blow-up at Z, read on the blow-up at Z' = Z.

Equations

• Hironaka.Monomial.PieceFamily.castSeq hZ T = hZ ▸ T

theorem Hironaka.Monomial.PieceFamily.cons_castSeq {X : AlgebraicGeometry.Scheme} {Z Z' : X.IdealSheafData} (hZ : Z = Z') (T : Z.blowUp.BlowUpSequence) : AlgebraicGeometry.Scheme.BlowUpSequence.cons X Z' (castSeq hZ T) = AlgebraicGeometry.Scheme.BlowUpSequence.cons X Z T

theorem Hironaka.Monomial.PieceFamily.realizeAux_castFamily {X : AlgebraicGeometry.Scheme} {Z Z' : X.IdealSheafData} (hZ : Z = Z') (Ψ : PieceFamily Z.blowUp) (m : ℕ) (L : List (Finset (Finset ℕ))) : (castFamily hZ Ψ).realizeAux m L = castSeq hZ (Ψ.realizeAux m L)

theorem Hironaka.Monomial.PieceFamily.castFamily_nextComp {X : AlgebraicGeometry.Scheme} {Z Z' : X.IdealSheafData} (hZ : Z = Z') (Ψ : PieceFamily Z.blowUp) : (castFamily hZ Ψ).nextComp = Ψ.nextComp

theorem Hironaka.Monomial.PieceFamily.castFamily_nextLabel {X : AlgebraicGeometry.Scheme} {Z Z' : X.IdealSheafData} (hZ : Z = Z') (Ψ : PieceFamily Z.blowUp) : (castFamily hZ Ψ).nextLabel = Ψ.nextLabel

theorem Hironaka.Monomial.PieceFamily.castFamily_label {X : AlgebraicGeometry.Scheme} {Z Z' : X.IdealSheafData} (hZ : Z = Z') (Ψ : PieceFamily Z.blowUp) : (castFamily hZ Ψ).label = Ψ.label

theorem Hironaka.Monomial.PieceFamily.castFamily_a {X : AlgebraicGeometry.Scheme} {Z Z' : X.IdealSheafData} (hZ : Z = Z') (Ψ : PieceFamily Z.blowUp) : (castFamily hZ Ψ).a = Ψ.a

theorem Hironaka.Monomial.PieceFamily.castFamily_piece {X : AlgebraicGeometry.Scheme} {Z Z' : X.IdealSheafData} (hZ : Z = Z') (Ψ : PieceFamily Z.blowUp) (c : ℕ) : (castFamily hZ Ψ).piece c = castCloseds hZ (Ψ.piece c)

theorem Hironaka.Monomial.PieceFamily.castCloseds_strictTransformCloseds {X : AlgebraicGeometry.Scheme} {Z Z' : X.IdealSheafData} (hZ : Z = Z') (C : TopologicalSpace.Closeds ↥X) : castCloseds hZ (strictTransformCloseds Z C) = strictTransformCloseds Z' C

theorem Hironaka.Monomial.PieceFamily.castCloseds_preimage {X : AlgebraicGeometry.Scheme} {Z Z' : X.IdealSheafData} (hZ : Z = Z') (C : TopologicalSpace.Closeds ↥X) : castCloseds hZ (C.preimage ⋯) = C.preimage ⋯

theorem Hironaka.Monomial.PieceFamily.Agrees.castFamily {X : AlgebraicGeometry.Scheme} {Z Z' : X.IdealSheafData} (hZ : Z = Z') {Ψ : PieceFamily Z.blowUp} {D : MonomialState} {m : ℕ} (h : Ψ.Agrees D m) : (PieceFamily.castFamily hZ Ψ).Agrees D m

The transported family agrees with the same state.

The piece correspondence passes through a blow-up

theorem Hironaka.Monomial.PieceFamily.PieceEq.blowUpPieces {X : AlgebraicGeometry.Scheme} {ρ : ℕ → ℕ} {Φ Φ' : PieceFamily X} {D P : MonomialState} {m : ℕ} (hpe : PieceEq ρ Φ Φ') (hΦ : Φ.Agrees D m) (hΦ' : Φ'.Agrees P m) {S : Finset (Finset ℕ)} (hS : ∀ Q ∈ S, ∀ c ∈ Q, c < Φ.nextComp) (hZ : Φ'.centerOf (Finset.image (Finset.image ρ) S) = Φ.centerOf S) : PieceEq (MonomialState.extendComp ρ D P S (Finset.image (Finset.image ρ) S)) (Φ.blowUpPieces S m) (castFamily hZ (Φ'.blowUpPieces (Finset.image (Finset.image ρ) S) m))

Along the lockstep, the two transported families keep the same pieces: the old pieces are the strict transforms of the same pieces under the same centre, the new pieces the preimages of the same face sets, at the indices matched by extendComp.

The fold

theorem Hironaka.Monomial.PieceFamily.realizeAux_runRel {ρ σ ρ' σ' : ℕ → ℕ} {D P D' P' : MonomialState} {L L' : List (Finset (Finset ℕ))} (hr : MonomialState.RunRel ρ σ D P L L' ρ' σ' D' P') {X : AlgebraicGeometry.Scheme} (Φ Φ' : PieceFamily X) (m : ℕ) : Φ.Agrees D m → Φ'.Agrees P m → PieceEq ρ Φ Φ' → Φ.realizeAux m L = Φ'.realizeAux m L'

Along the lockstep, the two folds produce the same blow-up sequence, by one induction on RunRel: the centres agree (PieceEq.centerOf), the transported families keep the same pieces (PieceEq.blowUpPieces) and follow the blown-up states (Agrees.blowUpPieces), and the tails are identified through the equality of the centres.

theorem Hironaka.Monomial.PieceFamily.realize_congr_of_rel {X : AlgebraicGeometry.Scheme} {Φ Φ' : PieceFamily X} {ρ σ : ℕ → ℕ} {n m : ℕ} (h : Φ.Rel ρ σ Φ') (hV : Φ.IsValid n m) (hV' : Φ'.IsValid n m) : Φ.realize n m hV = Φ'.realize n m hV'

The geometric Step 3 is invariant under a renumbering of the piece family. The states are related by MonomialState.Rel, Step 3 runs in lockstep (step3_runRel), and the fold follows (realizeAux_runRel).