CP1 and sub-families of the boundary

Step 2.2 of the proof of [Kol07, Theorem 103] (item 104, Step 2.2) runs Lemma 102 on the triple (X_r, I_r, F_r + H_r) whose boundary is the exceptional sub-family F_r of the total transform E_r of the original boundary. The statement CP1 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) for that run speaks about the transforms of F_r, while CP1 along the whole run of BO_{n,1} speaks about the transforms of E_r. The two agree at the points of the component's strict transform because the missing members — the birational transforms of the original members — miss V(I_r) from the end of Step 2.1 on, hence miss c̃.

This module holds the bookkeeping. The chain form at p only sees the members through p, so an injection of index types with equal members whose complement misses p does not change it (chainRelativeAt_iff_of_embeds, the common generalisation of chainRelativeAt_of_extendsByEmpty and chainRelativeAt_subfamily_iff). Such an injection propagates along a blow-up sequence to the total transforms, with complement the transforms of the missing originals (exists_embeds_totalTransformSeq, by recursion on the sequence; the total transform is that of [Kol07, Definition 25]). CP1 carries from the sub-family to the family when those transforms miss c̃ below the first containing stage (cp1For_of_embeds; the stop rule does not involve the boundary). Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Step22 and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Step22.

theorem Hironaka.Resolution.chainRelativeAt_iff_of_embeds {X : AlgebraicGeometry.Scheme} {E₁ E₂ : X.DivisorFamily} (e : E₁.ι → E₂.ι) (he : Function.Injective e) (hcomp : ∀ (a : E₁.ι), E₂.component (e a) = E₁.component a) {p : ↥X} (hmiss : ∀ b ∉ Set.range e, p ∉ (E₂.component b).support) {I Γ : X.IdealSheafData} : ChainRelativeAt E₁ I Γ p ↔ ChainRelativeAt E₂ I Γ p

The common generalisation of chainRelativeAt_of_extendsByEmpty and chainRelativeAt_subfamily_iff: for an injection e of index types carrying the members of E₁ to members of E₂ with the same ideal sheaves, such that every member of E₂ outside its range misses p, the chain forms along Γ at p for E₁ and E₂ agree — the members through p correspond.

theorem Hironaka.Resolution.exists_embeds_totalTransformSeq {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) {E₁ E₂ : X.DivisorFamily} (e₀ : E₁.ι → E₂.ι) : Function.Injective e₀ → (∀ (a : E₁.ι), E₂.component (e₀ a) = E₁.component a) → ∀ (i : Fin (S.length + 1)), ∃ (e : (S.totalTransformSeq E₁ i).ι → (S.totalTransformSeq E₂ i).ι), Function.Injective e ∧ (∀ (b : (S.totalTransformSeq E₁ i).ι), (S.totalTransformSeq E₂ i).component (e b) = (S.totalTransformSeq E₁ i).component b) ∧ ∀ b ∉ Set.range e, ∃ a ∉ Set.range e₀, b = S.originalIdx E₂ i a

An injection of families with equal members (a sub-family) induces, at every stage of a blow-up sequence, an injection of the total transforms with equal members whose complement consists of the birational transforms of the original members outside the range (originalIdx). By recursion on the sequence, the injection carried through a blow-up as Sum.map e₀ id on the lexicographic sum.

theorem Hironaka.Resolution.cp1For_of_embeds {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (I : X.IdealSheafData) {E₁ E₂ : X.DivisorFamily} (e₀ : E₁.ι → E₂.ι) (he₀ : Function.Injective e₀) (hcomp₀ : ∀ (a : E₁.ι), E₂.component (e₀ a) = E₁.component a) {η : ↥X} (hmiss : ∀ (i : Fin S.length), (∀ l < ↑i, ¬CenterContains S (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) l) → ∀ a ∉ Set.range e₀, ∀ p ∈ (S.strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) i.castSucc).support, p ∉ ((S.totalTransformSeq E₂ i.castSucc).component (S.originalIdx E₂ i.castSucc a)).support) (h : CP1For S I E₁ η) : CP1For S I E₂ η

The family bridge of Step 2.2. CP1 for the run with the sub-family E₁ of E₂ gives CP1 with E₂, provided that at every stage below the first containing one the transforms of the members of E₂ outside E₁ miss the strict transform of c̄: the stop rule does not involve the boundary, and at the first containing stage the two total transforms have the same members through every point of c̃.