The exceptional sub-family under pull-back

exceptionalFamily S E (Hironaka/Resolution/Algebraic/Kol07/SncGlobalSubfamily.lean) is the sub-family of the total transform E_r consisting of the members that are not transforms of original members (originalIdx): the exceptional divisors of the sequence, in the sense of the total exceptional set of [Kol07, Definition 25]. Along a flat h : Y ⟶ X the total transform of the pulled-back family is the pull-back of the total transform (totalTransformSeq_pullback), and the original members correspond: the sub-family avoiding the transforms of a chosen set of original members pulls back to the corresponding sub-family (subfamily_originalIdx_pullback, by recursion on the sequence with the chosen set carried through the first blow-up as toLex ∘ Sum.inl; the pulled-back total transform of a cons differs from the pull-back of the total transform only by totalTransform_comap_of_flat, transported by subfamily_originalIdx_congr). At the last stage this is exceptionalFamily_pullback, with the index identification pullbackStageIdx_last absorbed into the last-stage lift pullbackLastHom (subfamily_totalTransformSeq_eq_idx). It is used for the functoriality of the boundary-clearing sequence of [Kol07, 104, Step 2.2].

theorem Hironaka.Sequence.subfamily_originalIdx_congr {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (F₁ F₂ : X.DivisorFamily) (e : F₁ = F₂) (i : Fin (S.length + 1)) {T : Type u} (x₁ : T → F₁.ι) (x₂ : T → F₂.ι) (hx : x₁ ≍ x₂) : ((S.totalTransformSeq F₁ i).subfamily fun (b : (S.totalTransformSeq F₁ i).ι) => ∀ (t : T), b ≠ S.originalIdx F₁ i (x₁ t)) = (S.totalTransformSeq F₂ i).subfamily fun (b : (S.totalTransformSeq F₂ i).ι) => ∀ (t : T), b ≠ S.originalIdx F₂ i (x₂ t)

Transport of the sub-family avoiding the transforms of marked original members along an equality of the starting families (whose index types agree definitionally in every use).

theorem Hironaka.Sequence.subfamily_originalIdx_pullback {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) {Y : AlgebraicGeometry.Scheme} (h : Y ⟶ X) [AlgebraicGeometry.Flat h] (E : X.DivisorFamily) (j : ℕ) (hj : j < S.length + 1) {T : Type u} (g : T → E.ι) : (((S.pullback h).totalTransformSeq (E.comap h) (S.pullbackStageIdx h ⟨j, hj⟩)).subfamily fun (b : ((S.pullback h).totalTransformSeq (E.comap h) (S.pullbackStageIdx h ⟨j, hj⟩)).ι) => ∀ (t : T), b ≠ (S.pullback h).originalIdx (E.comap h) (S.pullbackStageIdx h ⟨j, hj⟩) (g t)) = ((S.totalTransformSeq E ⟨j, hj⟩).subfamily fun (b : (S.totalTransformSeq E ⟨j, hj⟩).ι) => ∀ (t : T), b ≠ S.originalIdx E ⟨j, hj⟩ (g t)).comap (S.pullbackStageHom h ⟨j, hj⟩)

Along a flat h, the sub-family of the total transform at stage ⟨j, hj⟩ avoiding the transforms of the original members g t pulls back to the corresponding sub-family of the pulled-back sequence, by recursion on the sequence, the chosen members carried through the first blow-up as toLex (Sum.inl (g t)).

theorem Hironaka.Sequence.subfamily_totalTransformSeq_eq_idx {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (E : X.DivisorFamily) {i j : Fin (S.length + 1)} (e : i = j) (P : (i : Fin (S.length + 1)) → (S.totalTransformSeq E i).ι → Prop) : (S.totalTransformSeq E j).subfamily (P j) = ((S.totalTransformSeq E i).subfamily (P i)).comap (CategoryTheory.eqToHom ⋯)

Transport of a sub-family of the total transform along an equality of stage indices: the eqToHom of the stage identification is absorbed.

theorem Hironaka.Sequence.exceptionalFamily_pullback {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (h : Y ⟶ X) [AlgebraicGeometry.Flat h] (E : X.DivisorFamily) : (S.pullback h).exceptionalFamily (E.comap h) = (S.exceptionalFamily E).comap (S.pullbackLastHom h)

The exceptional sub-family of the pulled-back sequence is the inverse image of the exceptional sub-family along the last-stage lift (originalIdx commutes with pull-back, and so does the total transform, totalTransformSeq_pullback).