The renumbering across one blow-up

When the direct state D blows up its centre S_D and the pulled-back state P blows up the centre S of N, whose faces in P are exactly the ρ-images of the faces of S_D, the renumbering Rel ρ σ D P of Hironaka/Resolution/Algebraic/Monomial/Restrict/Rename.lean extends: the new component of Q ∈ S_D goes to the new component of ρ(Q) ∈ S (extendComp), the new label of D to the new label of P (extendLabel), and Rel persists (Rel.blowUp). The order of the new components is preserved because the faces of a centre are numbered by their sorted lists of components and ρ is strictly monotone (lex_map_iff). Not in the sources; this is the step of the induction of Hironaka/Resolution/Algebraic/Monomial/Restrict/Phase.lean, and extendComp is also the renumbering along which the geometric run is pulled back in Hironaka/Resolution/Algebraic/Monomial/Geometric/PullbackRun.lean and Hironaka/Resolution/Algebraic/Monomial/Geometric/ChainRun.lean.

def Hironaka.Monomial.MonomialState.extendComp (ρ : ℕ → ℕ) (D P : MonomialState) (S_D S : Finset (Finset ℕ)) (c : ℕ) : ℕ

The renumbering of components after a blow-up: old components by ρ, the new component of the face Q of S_D to the new component of ρ(Q) in S.

Equations

• Hironaka.Monomial.MonomialState.extendComp ρ D P S_D S c = if c < D.nextComp then ρ c else {Q ∈ S_D | D.newComp S_D Q = c}.sup fun (Q : Finset ℕ) => P.newComp S (Finset.image ρ Q)

def Hironaka.Monomial.MonomialState.extendLabel (σ : ℕ → ℕ) (D P : MonomialState) (ℓ : ℕ) : ℕ

The renumbering of labels after a blow-up: old labels by σ, the new label to the new label.

Equations

• Hironaka.Monomial.MonomialState.extendLabel σ D P ℓ = if ℓ < D.nextLabel then σ ℓ else P.nextLabel

theorem Hironaka.Monomial.MonomialState.extendComp_of_lt (ρ : ℕ → ℕ) (D P : MonomialState) (S_D S : Finset (Finset ℕ)) {c : ℕ} (hc : c < D.nextComp) : extendComp ρ D P S_D S c = ρ c

theorem Hironaka.Monomial.MonomialState.extendComp_newComp (ρ : ℕ → ℕ) (D P : MonomialState) (S_D S : Finset (Finset ℕ)) {Q : Finset ℕ} (hQ : Q ∈ S_D) : extendComp ρ D P S_D S (D.newComp S_D Q) = P.newComp S (Finset.image ρ Q)

theorem Hironaka.Monomial.MonomialState.extendLabel_of_lt (σ : ℕ → ℕ) (D P : MonomialState) {ℓ : ℕ} (hℓ : ℓ < D.nextLabel) : extendLabel σ D P ℓ = σ ℓ

theorem Hironaka.Monomial.MonomialState.extendLabel_nextLabel (σ : ℕ → ℕ) (D P : MonomialState) : extendLabel σ D P D.nextLabel = P.nextLabel

theorem Hironaka.Monomial.MonomialState.image_extendComp_of_lt (ρ : ℕ → ℕ) (D P : MonomialState) (S_D S : Finset (Finset ℕ)) {T : Finset ℕ} (hT : ∀ c ∈ T, c < D.nextComp) : Finset.image (extendComp ρ D P S_D S) T = Finset.image ρ T

Ranks under the renumbering

theorem Hironaka.Monomial.MonomialState.rank_lt_rank_iff {S : Finset (Finset ℕ)} {P Q : Finset ℕ} (hP : P ∈ S) (hQ : Q ∈ S) : rank S P < rank S Q ↔ faceList P < faceList Q

theorem Hironaka.Monomial.MonomialState.exists_newComp_eq (D : MonomialState) (S_D : Finset (Finset ℕ)) {c : ℕ} (hc : D.nextComp ≤ c) (hc' : c < D.nextComp + S_D.card) : ∃ Q ∈ S_D, D.newComp S_D Q = c

The new components allocated by a blow-up are exactly nextComp, …, nextComp + |S_D| - 1.

theorem Hironaka.Monomial.MonomialState.Rel.faceList_image {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {Q : Finset ℕ} (hQ : ∀ c ∈ Q, c < D.nextComp) : faceList (Finset.image ρ Q) = List.map ρ (faceList Q)

theorem Hironaka.Monomial.MonomialState.Rel.faceList_image_lt_iff {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {Q Q' : Finset ℕ} (hQ : ∀ c ∈ Q, c < D.nextComp) (hQ' : ∀ c ∈ Q', c < D.nextComp) : faceList (Finset.image ρ Q) < faceList (Finset.image ρ Q') ↔ faceList Q < faceList Q'

theorem Hironaka.Monomial.MonomialState.Rel.image_subset_image_iff {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {A B : Finset ℕ} (hA : ∀ c ∈ A, c < D.nextComp) (hB : ∀ c ∈ B, c < D.nextComp) : Finset.image ρ A ⊆ Finset.image ρ B ↔ A ⊆ B

Images of subsets of faces compare like the subsets.

theorem Hironaka.Monomial.MonomialState.Rel.image_eq_image_iff {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {A B : Finset ℕ} (hA : ∀ c ∈ A, c < D.nextComp) (hB : ∀ c ∈ B, c < D.nextComp) : Finset.image ρ A = Finset.image ρ B ↔ A = B

theorem Hironaka.Monomial.MonomialState.lt_of_mem_center {D : MonomialState} {S_D : Finset (Finset ℕ)} (hSD : S_D ⊆ D.nerve) {Q : Finset ℕ} (hQ : Q ∈ S_D) (c : ℕ) : c ∈ Q → c < D.nextComp

theorem Hironaka.Monomial.MonomialState.image_mem_center {ρ : ℕ → ℕ} {P : MonomialState} {S S_D : Finset (Finset ℕ)} (hfilter : {x ∈ S | x ∈ P.nerve} = Finset.image (Finset.image ρ) S_D) {Q : Finset ℕ} (hQ : Q ∈ S_D) : Finset.image ρ Q ∈ S

theorem Hironaka.Monomial.MonomialState.exists_of_mem_center {ρ : ℕ → ℕ} {P : MonomialState} {S S_D : Finset (Finset ℕ)} (hfilter : {x ∈ S | x ∈ P.nerve} = Finset.image (Finset.image ρ) S_D) {Q : Finset ℕ} (hQ : Q ∈ S) (hQP : Q ∈ P.nerve) : ∃ Q₀ ∈ S_D, Finset.image ρ Q₀ = Q

A face of S lying in P's nerve is the image of a face of S_D.

theorem Hironaka.Monomial.MonomialState.lt_or_exists_newComp (D : MonomialState) (S_D : Finset (Finset ℕ)) {c : ℕ} (hc : c < D.nextComp + S_D.card) : c < D.nextComp ∨ ∃ Q ∈ S_D, D.newComp S_D Q = c

A component below the new counter is old or the new component of a face of the centre.

theorem Hironaka.Monomial.MonomialState.Rel.newComp_image_lt {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {S S_D : Finset (Finset ℕ)} (hSD : S_D ⊆ D.nerve) (hfilter : {x ∈ S | x ∈ P.nerve} = Finset.image (Finset.image ρ) S_D) {Q₁ Q₂ : Finset ℕ} (hQ₁ : Q₁ ∈ S_D) (hQ₂ : Q₂ ∈ S_D) (hlt : D.newComp S_D Q₁ < D.newComp S_D Q₂) : P.newComp S (Finset.image ρ Q₁) < P.newComp S (Finset.image ρ Q₂)

theorem Hironaka.Monomial.MonomialState.Rel.not_subset_image {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {S S_D : Finset (Finset ℕ)} (hSD : S_D ⊆ D.nerve) (hfilter : {x ∈ S | x ∈ P.nerve} = Finset.image (Finset.image ρ) S_D) (hS0 : ∀ Q ∈ S, Q.Nonempty) {T : Finset ℕ} (hT : T ∈ D.nerve) (hTS : ∀ Q₀ ∈ S_D, ¬Q₀ ⊆ T) (Q : Finset ℕ) : Q ∈ S → ¬Q ⊆ Finset.image ρ T

No face of the centre S lies inside the image of a set of old components unless it is the image of a face of S_D inside that set.

theorem Hironaka.Monomial.MonomialState.Rel.extendComp_strictMonoOn {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {S S_D : Finset (Finset ℕ)} (hSD : S_D ⊆ D.nerve) (hfilter : {x ∈ S | x ∈ P.nerve} = Finset.image (Finset.image ρ) S_D) : StrictMonoOn (extendComp ρ D P S_D S) (Set.Iio (D.nextComp + S_D.card))

theorem Hironaka.Monomial.MonomialState.Rel.extendComp_lt {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {S S_D : Finset (Finset ℕ)} (hfilter : {x ∈ S | x ∈ P.nerve} = Finset.image (Finset.image ρ) S_D) (c : ℕ) : c < D.nextComp + S_D.card → extendComp ρ D P S_D S c < P.nextComp + S.card

theorem Hironaka.Monomial.MonomialState.Rel.blowUp_a_extend {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {S S_D : Finset (Finset ℕ)} (hSD : S_D ⊆ D.nerve) (hfilter : {x ∈ S | x ∈ P.nerve} = Finset.image (Finset.image ρ) S_D) (c : ℕ) : c < D.nextComp + S_D.card → (P.blowUp S).a (extendComp ρ D P S_D S c) = (D.blowUp S_D).a c

theorem Hironaka.Monomial.MonomialState.Rel.blowUp_label_extend {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {S S_D : Finset (Finset ℕ)} (c : ℕ) : c < D.nextComp + S_D.card → (P.blowUp S).label (extendComp ρ D P S_D S c) = extendLabel σ D P ((D.blowUp S_D).label c)

theorem Hironaka.Monomial.MonomialState.Rel.extendLabel_strictMonoOn {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) : StrictMonoOn (extendLabel σ D P) (Set.Iio (D.nextLabel + 1))

theorem Hironaka.Monomial.MonomialState.Rel.extendLabel_lt {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) (ℓ : ℕ) : ℓ < D.nextLabel + 1 → extendLabel σ D P ℓ < P.nextLabel + 1

theorem Hironaka.Monomial.MonomialState.Rel.blowUp_nerve_extend {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {S S_D : Finset (Finset ℕ)} (hSD : S_D ⊆ D.nerve) (hfilter : {x ∈ S | x ∈ P.nerve} = Finset.image (Finset.image ρ) S_D) (hS0 : ∀ Q ∈ S, Q.Nonempty) : (P.blowUp S).nerve = Finset.image (Finset.image (extendComp ρ D P S_D S)) (D.blowUp S_D).nerve

The nerve rule commutes with the renumbering.

theorem Hironaka.Monomial.MonomialState.Rel.blowUp {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {S S_D : Finset (Finset ℕ)} (hSD : S_D ⊆ D.nerve) (hfilter : {x ∈ S | x ∈ P.nerve} = Finset.image (Finset.image ρ) S_D) (hS0 : ∀ Q ∈ S, Q.Nonempty) : Rel (extendComp ρ D P S_D S) (extendLabel σ D P) (D.blowUp S_D) (P.blowUp S)

The renumbering extends across a blow-up: D along its centre S_D, P along the centre S whose faces in P are the images of those of S_D.