Renumbering components and labels

The direct run of Kollár's Step 3 on a subnerve and the pulled-back run of Hironaka/Resolution/Algebraic/Monomial/Restrict.lean allocate components and labels differently (the empty blow-ups of the pulled-back run still allocate), so the two are compared through an order-preserving renumbering. Rel ρ σ D P says that the state P (the pulled-back one) is the state D (the direct one) with components renamed by ρ and labels by σ, both strictly monotone on the allocated ranges; the faces of P are exactly the images of the faces of D, with the same exponents and renamed labels, and P may have further dead components and unused labels. Everything Kollár's choice looks at is transported: face sizes and sums (Rel.total_image), label tuples (Rel.labelTuple_image, through sortedList_image: the increasing enumeration commutes with a strictly monotone map, and map_lt_map_iff: so does the lexicographic order), hence the faces of a size, (∗_s) and the choice itself (Rel.choice_eq). Not in the sources; this is the bookkeeping behind the reindexing of [Kol07, 34.1]. The relation is extended across a blow-up in Hironaka/Resolution/Algebraic/Monomial/Restrict/Extend.lean, and the real-analytic strand states its own refinement relation with it (Hironaka/Resolution/Analytic/OrderReduction/BMO/Step3Monomial/RefinesAlong.lean).

Sorted lists and the lexicographic order under strictly monotone maps

theorem Hironaka.Monomial.MonomialState.sortedList_image {s : Finset ℕ} {f : ℕ → ℕ} (hf : StrictMonoOn f ↑s) : sortedList (Finset.image f s) = List.map f (sortedList s)

The increasing enumeration of the image under a map strictly monotone on the set is the mapped enumeration.

theorem Hironaka.Monomial.MonomialState.lex_cons_cons_iff {a b : ℕ} {l l' : List ℕ} : List.Lex (fun (x1 x2 : ℕ) => x1 < x2) (a :: l) (b :: l') ↔ a < b ∨ a = b ∧ List.Lex (fun (x1 x2 : ℕ) => x1 < x2) l l'

theorem Hironaka.Monomial.MonomialState.lex_map_iff {f : ℕ → ℕ} {A : Set ℕ} (hf : StrictMonoOn f A) {l l' : List ℕ} : (∀ x ∈ l, x ∈ A) → (∀ x ∈ l', x ∈ A) → (List.Lex (fun (x1 x2 : ℕ) => x1 < x2) (List.map f l) (List.map f l') ↔ List.Lex (fun (x1 x2 : ℕ) => x1 < x2) l l')

The lexicographic order of lists is preserved by a map strictly monotone on their elements.

theorem Hironaka.Monomial.MonomialState.map_lt_map_iff {f : ℕ → ℕ} {A : Set ℕ} (hf : StrictMonoOn f A) {l l' : List ℕ} (hl : ∀ x ∈ l, x ∈ A) (hl' : ∀ x ∈ l', x ∈ A) : List.map f l < List.map f l' ↔ l < l'

theorem Hironaka.Monomial.MonomialState.map_le_map_iff {f : ℕ → ℕ} {A : Set ℕ} (hf : StrictMonoOn f A) {l l' : List ℕ} (hl : ∀ x ∈ l, x ∈ A) (hl' : ∀ x ∈ l', x ∈ A) : List.map f l ≤ List.map f l' ↔ l ≤ l'

The renumbering relation

structure Hironaka.Monomial.MonomialState.Rel (ρ σ : ℕ → ℕ) (D P : MonomialState) : Prop

Rel ρ σ D P: the state P is the state D with components renamed by ρ and labels by σ (both strictly monotone on the allocated ranges, landing below P's counters): the same dimension bound and mark, the exponents and (renamed) labels of D's components, and the faces of P exactly the images of the faces of D. P may carry further dead components and unused labels.

• n_eq : D.n = P.n
• m_eq : D.m = P.m
• mono : StrictMonoOn ρ (Set.Iio D.nextComp)
• lt (c : ℕ) : c < D.nextComp → ρ c < P.nextComp
• a_eq (c : ℕ) : c < D.nextComp → P.a (ρ c) = D.a c
• label_eq (c : ℕ) : c < D.nextComp → P.label (ρ c) = σ (D.label c)
• σmono : StrictMonoOn σ (Set.Iio D.nextLabel)
• σlt (ℓ : ℕ) : ℓ < D.nextLabel → σ ℓ < P.nextLabel
• nerve_eq : P.nerve = Finset.image (Finset.image ρ) D.nerve

theorem Hironaka.Monomial.MonomialState.Rel.refl (D : MonomialState) : Rel id id D D

theorem Hironaka.Monomial.MonomialState.Rel.injOn_of_subset {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {T : Finset ℕ} (hT : ∀ c ∈ T, c < D.nextComp) : Set.InjOn ρ ↑T

theorem Hironaka.Monomial.MonomialState.Rel.injOn_face {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {T : Finset ℕ} (hT : T ∈ D.nerve) : Set.InjOn ρ ↑T

theorem Hironaka.Monomial.MonomialState.Rel.card_image {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {T : Finset ℕ} (hT : ∀ c ∈ T, c < D.nextComp) : (Finset.image ρ T).card = T.card

theorem Hironaka.Monomial.MonomialState.Rel.total_image {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {T : Finset ℕ} (hT : ∀ c ∈ T, c < D.nextComp) : P.total (Finset.image ρ T) = D.total T

theorem Hironaka.Monomial.MonomialState.Rel.labels_image {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {T : Finset ℕ} (hT : ∀ c ∈ T, c < D.nextComp) : P.labels (Finset.image ρ T) = Finset.image σ (D.labels T)

theorem Hironaka.Monomial.MonomialState.Rel.labels_lt {D : MonomialState} {T : Finset ℕ} (hT : ∀ c ∈ T, c < D.nextComp) (ℓ : ℕ) : ℓ ∈ D.labels T → ℓ < D.nextLabel

theorem Hironaka.Monomial.MonomialState.Rel.labelTuple_image {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {T : Finset ℕ} (hT : ∀ c ∈ T, c < D.nextComp) : P.labelTuple (Finset.image ρ T) = List.map σ (D.labelTuple T)

theorem Hironaka.Monomial.MonomialState.Rel.labelTuple_le_iff {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {T T' : Finset ℕ} (hT : ∀ c ∈ T, c < D.nextComp) (hT' : ∀ c ∈ T', c < D.nextComp) : P.labelTuple (Finset.image ρ T) ≤ P.labelTuple (Finset.image ρ T') ↔ D.labelTuple T ≤ D.labelTuple T'

theorem Hironaka.Monomial.MonomialState.Rel.image_mem_nerve {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {T : Finset ℕ} (hT : T ∈ D.nerve) : Finset.image ρ T ∈ P.nerve

theorem Hironaka.Monomial.MonomialState.Rel.exists_of_mem_nerve {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {T' : Finset ℕ} (hT' : T' ∈ P.nerve) : ∃ T ∈ D.nerve, Finset.image ρ T = T'

theorem Hironaka.Monomial.MonomialState.Rel.image_mem_nerve_iff {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {T : Finset ℕ} (hT : ∀ c ∈ T, c < D.nextComp) : Finset.image ρ T ∈ P.nerve ↔ T ∈ D.nerve

theorem Hironaka.Monomial.MonomialState.Rel.faces_eq {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) (r : ℕ) : P.faces r = Finset.image (Finset.image ρ) (D.faces r)

theorem Hironaka.Monomial.MonomialState.Rel.star_iff {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) (s : ℕ) : P.Star s ↔ D.Star s

theorem Hironaka.Monomial.MonomialState.Rel.choice_eq {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) (r : ℕ) : P.choice r = Finset.image (Finset.image ρ) (D.choice r)

Kollár's choice is transported by the renumbering.

theorem Hironaka.Monomial.MonomialState.Rel.choice_eq_empty_iff {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) (r : ℕ) : P.choice r = ∅ ↔ D.choice r = ∅