CP1 across a first blow-up that does not contain the component

The cons case of cp1For_concat (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1For): when the first blow-up of cons X D R does not contain c̃, CP1 for the sequence follows from CP1 for its tail R at the lifted generic point, with the transforms of the data along the first blow-up — cons X D R is the concatenation of the single blow-up cons X D nil with R (the blow-up sequences of [Kol07, Definition 29]), and CP1 holds vacuously along the single blow-up. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Step22Core.

theorem Hironaka.Resolution.cp1For_cons_of_not_centerContains {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (D : X.IdealSheafData) (R : D.blowUp.BlowUpSequence) (I : X.IdealSheafData) (E : X.DivisorFamily) {η : ↥X} (hη : η ∈ I.support.genericPoints) (hηE : ∀ (j : E.ι), η ∉ (E.component j).support) (hIc : I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) (hD : ¬CenterContains (AlgebraicGeometry.Scheme.BlowUpSequence.cons X D R) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) 0) (hR : ∀ (η' : ↥D.blowUp), GenericLift (AlgebraicGeometry.Scheme.BlowUpSequence.cons X D (AlgebraicGeometry.Scheme.BlowUpSequence.nil D.blowUp)) I E 1 η (Fin.last (AlgebraicGeometry.Scheme.BlowUpSequence.cons X D (AlgebraicGeometry.Scheme.BlowUpSequence.nil D.blowUp)).length) η' → CP1For R (I.markedTransform D 1) (E.totalTransform D) η') : CP1For (AlgebraicGeometry.Scheme.BlowUpSequence.cons X D R) I E η

cp1For_concat for the single blow-up cons X D nil followed by R, which is cons X D R: when the first blow-up does not contain c̃, CP1 for the sequence follows from CP1 for its tail at the lifted generic point (the generic lift along the single blow-up), with the transforms along the first blow-up.