The geometric Step 3 does not depend on the enumeration of the components

The input family ofDivisorFamily E a e σ of Hironaka/Resolution/Algebraic/Monomial/Geometric/Pieces.lean enumerates the irreducible components of the members of E by σ : Fin k ≃ Components E. Kollár's Step 3 ([Kol07, 111, Step 3]) does not depend on that enumeration: its choices are made on faces compared by their label tuples and sums, never by the numbering of the pieces. Two enumerations of the same components give the same input family up to a permutation of the pieces, and the permutation is a refinement along the identity in the sense of Hironaka/Resolution/Algebraic/Monomial/Geometric/Refinement.lean (refinesAlong_id_ofDivisorFamily): the same label count, labels and exponents through the relabelling σ₁⁻¹ ∘ σ₂, every piece inside (indeed equal to) its parent, every parent the union of its unique child, and no two children of one parent. The functoriality of the geometric Step 3 under smooth surjections (realize_pullback_of_surjective of Hironaka/Resolution/Algebraic/Monomial/Geometric/PullbackRun.lean) at h = 𝟙 X then identifies the two runs (realize_ofDivisorFamily_indep; the pull-back along the identity is the sequence itself). Also here: two exponent functions agreeing at the generic points of the members give the same input family (ofDivisorFamily_congr: ofDivisorFamily reads its exponents there only). Not in the sources. Used in Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step3Functorial.lean to show that the third step of BMO_{n,m} is well defined.

theorem Hironaka.Monomial.PieceFamily.ofDivisorFamily_congr_of_forall {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {L k' : ℕ} (a a' : ↥X → ℕ) (e : E.ι ≃o Fin L) (σ : Fin k' ≃ Components E) (h : ∀ (c : Components E), a ↑c.snd = a' ↑c.snd) : ofDivisorFamily E a e σ = ofDivisorFamily E a' e σ

Two exponent functions agreeing at the generic points of the members give the same input family.

theorem Hironaka.Monomial.PieceFamily.ofDivisorFamily_congr {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) {E : X.DivisorFamily} {L k' : ℕ} (a a' : ↥X → ℕ) (e : E.ι ≃o Fin L) (σ : Fin k' ≃ Components E) (h : ∀ (c : Components E), a ↑c.snd = a' ↑c.snd) : ofDivisorFamily E a e σ = ofDivisorFamily E a' e σ

Two exponent functions agreeing at the generic points of the members give the same input family: ofDivisorFamily reads its exponents there only. The structure morphism f is present because the statements about the input family of a triple over k are all made over its structure morphism; the proof does not need it, the equality being one of definitions on any scheme (ofDivisorFamily_congr_of_forall).

noncomputable def Hironaka.Monomial.PieceFamily.relabel {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {k₁ k₂ : ℕ} (σ₁ : Fin k₁ ≃ Components E) (σ₂ : Fin k₂ ≃ Components E) (c : ℕ) : ℕ

The relabelling of the pieces between two enumerations of the components: the piece c of the second enumeration is the piece σ₁⁻¹ (σ₂ c) of the first (and 0 off the range).

Equations

• Hironaka.Monomial.PieceFamily.relabel σ₁ σ₂ c = if h : c < k₂ then ↑(σ₁.symm (σ₂ ⟨c, h⟩)) else 0

theorem Hironaka.Monomial.PieceFamily.relabel_of_lt {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {k₁ k₂ : ℕ} (σ₁ : Fin k₁ ≃ Components E) (σ₂ : Fin k₂ ≃ Components E) {c : ℕ} (hc : c < k₂) : relabel σ₁ σ₂ c = ↑(σ₁.symm (σ₂ ⟨c, hc⟩))

theorem Hironaka.Monomial.PieceFamily.relabel_lt {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {k₁ k₂ : ℕ} (σ₁ : Fin k₁ ≃ Components E) (σ₂ : Fin k₂ ≃ Components E) {c : ℕ} (hc : c < k₂) : relabel σ₁ σ₂ c < k₁

theorem Hironaka.Monomial.PieceFamily.apply_relabel {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {k₁ k₂ : ℕ} (σ₁ : Fin k₁ ≃ Components E) (σ₂ : Fin k₂ ≃ Components E) {c : ℕ} (hc : c < k₂) (h : relabel σ₁ σ₂ c < k₁) : σ₁ ⟨relabel σ₁ σ₂ c, h⟩ = σ₂ ⟨c, hc⟩

theorem Hironaka.Monomial.PieceFamily.ofDivisorFamily_piece_of_lt' {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {L : ℕ} (a : ↥X → ℕ) (e : E.ι ≃o Fin L) {k : ℕ} (σ : Fin k ≃ Components E) {c : ℕ} (hc : c < k) : (ofDivisorFamily E a e σ).piece c = TopologicalSpace.Closeds.closure {↑(σ ⟨c, hc⟩).snd}

theorem Hironaka.Monomial.PieceFamily.ofDivisorFamily_label_of_lt' {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {L : ℕ} (a : ↥X → ℕ) (e : E.ι ≃o Fin L) {k : ℕ} (σ : Fin k ≃ Components E) {c : ℕ} (hc : c < k) : (ofDivisorFamily E a e σ).label c = ↑(e (σ ⟨c, hc⟩).fst)

theorem Hironaka.Monomial.PieceFamily.ofDivisorFamily_a_of_lt' {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {L : ℕ} (a : ↥X → ℕ) (e : E.ι ≃o Fin L) {k : ℕ} (σ : Fin k ≃ Components E) {c : ℕ} (hc : c < k) : (ofDivisorFamily E a e σ).a c = a ↑(σ ⟨c, hc⟩).snd

theorem Hironaka.Monomial.PieceFamily.piece_relabel {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {k₁ k₂ : ℕ} (σ₁ : Fin k₁ ≃ Components E) (σ₂ : Fin k₂ ≃ Components E) {L : ℕ} (a : ↥X → ℕ) (e : E.ι ≃o Fin L) {c : ℕ} (hc : c < k₂) : (ofDivisorFamily E a e σ₁).piece (relabel σ₁ σ₂ c) = (ofDivisorFamily E a e σ₂).piece c

The piece of the relabelled index is the piece itself.

theorem Hironaka.Monomial.PieceFamily.refinesAlong_id_ofDivisorFamily {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {k₁ k₂ : ℕ} (σ₁ : Fin k₁ ≃ Components E) (σ₂ : Fin k₂ ≃ Components E) {L : ℕ} (a : ↥X → ℕ) (e : E.ι ≃o Fin L) : (ofDivisorFamily E a e σ₂).RefinesAlong (CategoryTheory.CategoryStruct.id X) (relabel σ₁ σ₂) (ofDivisorFamily E a e σ₁)

The input family of one enumeration of the components refines the input family of another along 𝟙 X through the relabelling σ₁⁻¹ ∘ σ₂: the same label count, labels and exponents through the relabelling, each piece equal to its parent, each parent the union of its unique child, and no two children of one parent.

theorem Hironaka.Monomial.PieceFamily.realize_ofDivisorFamily_indep {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] [AlgebraicGeometry.QuasiCompact f] {E : X.DivisorFamily} {n m : ℕ} (hE : E.IsSnc) (hn : ∃ n' ≤ n, AlgebraicGeometry.SmoothOfRelativeDimension n' f) {L k₁ k₂ : ℕ} (a : ↥X → ℕ) (e : E.ι ≃o Fin L) (σ₁ : Fin k₁ ≃ Components E) (σ₂ : Fin k₂ ≃ Components E) (hV₁ : (ofDivisorFamily E a e σ₁).IsValid n m) (hV₂ : (ofDivisorFamily E a e σ₂).IsValid n m) : (ofDivisorFamily E a e σ₁).realize n m hV₁ = (ofDivisorFamily E a e σ₂).realize n m hV₂

The geometric Step 3 does not depend on the enumeration of the components: for two enumerations of the components of E (the same label isomorphism) the realised runs coincide, by realize_pullback_of_surjective at h = 𝟙 X with the identity refinement refinesAlong_id_ofDivisorFamily and pullback_id.