CP1 descends along the local cover of Theorem 105

[Kol07, Theorem 105] evaluates BO_{n,1} on a triple T through a local cover g : T'.X.left → T.X.left (a coproduct of open immersions, surjective) on whose pieces a smooth hypersurface of maximal contact exists: BO(T') = g^* BO(T), since the functor commutes with smooth morphisms ([Kol07, Theorem 103 (2)], commutesWithSmooth; [Kol07, 34.1]). The statement CP1 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative; the predicate CP1For of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1For) for the run on T at a point p of the strict transform c̃_i follows from CP1 for the pulled-back run on T' at a point q over p, for the member c' := I_{closure η'} of a suitable point η' over η (a component of g⁻¹(V(c)) through the image of q): the first containing stage is the same on both sides (the stop-rule bookkeeping of claimFor_of_pullback_cover, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedClaimCover, repeated here), the three data of the pulled-back run at that stage are the pull-backs of the data of the run along the stage lift, and the chain form descends along the stalk isomorphism of the stage lift (chainRelativeAt_of_comap_of_isIso_stalkMap). Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Step2 and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3EraseEmpty.

theorem Hironaka.Resolution.cp1For_of_pullback_cover {k : Type u} [Field k] [CharZero k] (T T' : AlgebraicGeometry.Triple k) (g : T'.X.left ⟶ T.X.left) (hg : AlgebraicGeometry.openImmersionCoprods g) (hsurj : Function.Surjective ⇑g) (hpb : T'.IsPullbackOf T g) (S : T.X.left.BlowUpSequence) (hS : S.IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I 1 T.E) {η : ↥T.X.left} (hη : η ∈ T.I.support.genericPoints) (hηE : ∀ (j : T.E.ι), η ∉ (T.E.component j).support) (hIc : T.I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) (h : ∀ (η' : ↥T'.X.left), g η' = η → η' ∈ T'.I.support.genericPoints → (∀ (j : T'.E.ι), η' ∉ (T'.E.component j).support) → T'.I.stalkIdeal η' = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η'})).stalkIdeal η' → CP1For (S.pullback g) T'.I T'.E η') : CP1For S T.I T.E η

CP1 descends along a coproduct of open immersions ([Kol07, Theorem 105]; the counterpart of claimFor_of_pullback_cover): if it holds for the pulled-back run on T' at every point η' over η that is a generic point of g⁻¹(V(c)) (with the member I(closure η')), it holds for the run on T at η. The first containing stages agree (the lifted generic points correspond, GenericLift.uniq); the three data of the pulled-back run at that stage are the pull-backs of the data of the run along the stage lift (totalTransformSeq_pullback, [Kol07, Lemma 62] iterated, the strict transform through stalkIdeal_comap_vanishingIdeal_closure_eq); and the chain form descends along the stalk isomorphism of the stage lift.