Refinement: the transport lemmas and the extension across a blow-up

The first clause of [Kol07, 34.1], commutation with smooth surjections, for the combinatorial Step 3: along a refinement Refines ρ Y L (Hironaka/Resolution/Algebraic/Monomial/Restrict.lean; ρ maps the components of Y onto those of L preserving labels and exponents, is injective on every face of Y, and maps the faces of Y onto the faces of L) sums, sizes and label tuples of faces are preserved (Refines.total_image, card_image, labelTuple_image) and faces lift (exists_lift_faces), so Kollár's choice on Y is the ρ-preimage of the choice on L (Refines.choice_eq) and the choice on L is the image of the choice on Y (Refines.choice_image). Across a blow-up along a centre S_Y of Y and its image S_L (with S_Y the full preimage of S_L among the faces of Y, as Kollár's choices are), ρ extends by c_{P_Y} ↦ c_{ρ(P_Y)}, the same extendComp as for restriction (Hironaka/Resolution/Algebraic/Monomial/Restrict/Extend.lean), and Refines persists (Refines.blowUp): a face of Y survives iff its image does (the components of a face over a face of the centre form a face of the centre), the new faces map onto the new faces of L, and every new face of L lifts. Not in the sources. The induction along the phases is Hironaka/Resolution/Algebraic/Monomial/Restrict/RefinePhase.lean.

theorem Hironaka.Monomial.MonomialState.image_filter_mem_image {ρ : ℕ → ℕ} {W A : Finset ℕ} (hA : A ⊆ Finset.image ρ W) : Finset.image ρ ({c ∈ W | ρ c ∈ A}) = A

The image of the part of W over A is A, when A ⊆ ρ(W).

theorem Hironaka.Monomial.MonomialState.Refines.card_image {ρ : ℕ → ℕ} {Y L : MonomialState} (h : Refines ρ Y L) {T : Finset ℕ} (hT : T ∈ Y.nerve) : (Finset.image ρ T).card = T.card

theorem Hironaka.Monomial.MonomialState.Refines.total_image {ρ : ℕ → ℕ} {Y L : MonomialState} (h : Refines ρ Y L) {T : Finset ℕ} (hT : T ∈ Y.nerve) : L.total (Finset.image ρ T) = Y.total T

theorem Hironaka.Monomial.MonomialState.Refines.labels_image {ρ : ℕ → ℕ} {Y L : MonomialState} (h : Refines ρ Y L) {T : Finset ℕ} (hT : T ∈ Y.nerve) : L.labels (Finset.image ρ T) = Y.labels T

theorem Hironaka.Monomial.MonomialState.Refines.labelTuple_image {ρ : ℕ → ℕ} {Y L : MonomialState} (h : Refines ρ Y L) {T : Finset ℕ} (hT : T ∈ Y.nerve) : L.labelTuple (Finset.image ρ T) = Y.labelTuple T

theorem Hironaka.Monomial.MonomialState.Refines.image_mem_faces {ρ : ℕ → ℕ} {Y L : MonomialState} (h : Refines ρ Y L) {r : ℕ} {T : Finset ℕ} (hT : T ∈ Y.faces r) : Finset.image ρ T ∈ L.faces r

theorem Hironaka.Monomial.MonomialState.Refines.exists_lift_faces {ρ : ℕ → ℕ} {Y L : MonomialState} (h : Refines ρ Y L) {r : ℕ} {T' : Finset ℕ} (hT' : T' ∈ L.faces r) : ∃ T ∈ Y.faces r, Finset.image ρ T = T'

theorem Hironaka.Monomial.MonomialState.Refines.star_iff {ρ : ℕ → ℕ} {Y L : MonomialState} (h : Refines ρ Y L) (s : ℕ) : L.Star s ↔ Y.Star s

theorem Hironaka.Monomial.MonomialState.Refines.choice_eq {ρ : ℕ → ℕ} {Y L : MonomialState} (h : Refines ρ Y L) (r : ℕ) : Y.choice r = {Q ∈ Y.nerve | Finset.image ρ Q ∈ L.choice r}

Kollár's choice on Y is the ρ-preimage of the choice on L.

theorem Hironaka.Monomial.MonomialState.Refines.choice_image {ρ : ℕ → ℕ} {Y L : MonomialState} (h : Refines ρ Y L) (r : ℕ) : L.choice r = Finset.image (Finset.image ρ) (Y.choice r)

The choice on L is the image of the choice on Y.

theorem Hironaka.Monomial.MonomialState.Refines.choice_nonempty_iff {ρ : ℕ → ℕ} {Y L : MonomialState} (h : Refines ρ Y L) (r : ℕ) : (Y.choice r).Nonempty ↔ (L.choice r).Nonempty

The extension across a blow-up

theorem Hironaka.Monomial.MonomialState.Refines.image_mem_center' {ρ : ℕ → ℕ} {S_Y S_L : Finset (Finset ℕ)} (hSL : S_L = Finset.image (Finset.image ρ) S_Y) {Q : Finset ℕ} (hQ : Q ∈ S_Y) : Finset.image ρ Q ∈ S_L

theorem Hironaka.Monomial.MonomialState.Refines.exists_of_mem_center' {ρ : ℕ → ℕ} {S_Y S_L : Finset (Finset ℕ)} (hSL : S_L = Finset.image (Finset.image ρ) S_Y) {Q' : Finset ℕ} (hQ' : Q' ∈ S_L) : ∃ Q ∈ S_Y, Finset.image ρ Q = Q'

theorem Hironaka.Monomial.MonomialState.Refines.nonempty_of_mem_center' {ρ : ℕ → ℕ} {Y : MonomialState} {S_Y S_L : Finset (Finset ℕ)} (hSY : S_Y ⊆ Y.nerve) (hSL : S_L = Finset.image (Finset.image ρ) S_Y) {Q' : Finset ℕ} (hQ' : Q' ∈ S_L) : Q'.Nonempty

theorem Hironaka.Monomial.MonomialState.Refines.not_subset_image_of_forall {ρ : ℕ → ℕ} {Y : MonomialState} {S_Y S_L : Finset (Finset ℕ)} (hSY : S_Y ⊆ Y.nerve) (hSL : S_L = Finset.image (Finset.image ρ) S_Y) (hpre : ∀ Q ∈ Y.nerve, Finset.image ρ Q ∈ S_L → Q ∈ S_Y) {T : Finset ℕ} (hT : T ∈ Y.nerve) (hTS : ∀ Q ∈ S_Y, ¬Q ⊆ T) (Q' : Finset ℕ) : Q' ∈ S_L → ¬Q' ⊆ Finset.image ρ T

No face of S_L lies inside the image of a face T of Y containing no face of S_Y: the components of T over such a face would form a face of S_Y inside T.

theorem Hironaka.Monomial.MonomialState.Refines.blowUp {ρ : ℕ → ℕ} {Y L : MonomialState} (h : Refines ρ Y L) {S_Y S_L : Finset (Finset ℕ)} (hSY : S_Y ⊆ Y.nerve) (hSL : S_L = Finset.image (Finset.image ρ) S_Y) (hpre : ∀ Q ∈ Y.nerve, Finset.image ρ Q ∈ S_L → Q ∈ S_Y) : Refines (extendComp ρ Y L S_Y S_L) (Y.blowUp S_Y) (L.blowUp S_L)

Refines extends across a blow-up along S_Y and its image S_L.