CP1 along a sequence and its concatenation

CP1For S I E η: along the blow-up sequence S, at the FIRST stage whose centre contains the strict transform of the component c = V(closure {η}) of V(I), the marked transform of I is chain-relative monomial along that strict transform at every point of it (with respect to the total transform of E at that stage). This is the statement CP1 of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative as a predicate on one sequence: the form of Włodarczyk's Claim (ClaimFor, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedClaimAt) with the chain-relative conclusion in place of the false stalk equality. The concatenation lemma cp1For_concat: the first containing stage lies in S, or none does and the lifted generic point (exists_genericLift, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedGenericLift) hands the question to R at the end of S, the stages of the concatenation being read through the heterogeneous equalities of Hironaka.Scheme.BlowUpSequence.ConcatIndex. Used by the CP1 modules EmbeddedCP1At, EmbeddedCP1Cons, EmbeddedCP1EraseEmpty, EmbeddedCP1Step1, EmbeddedCP1Step2, and by EmbeddedCP1Absorbed.

def Hironaka.Resolution.CP1For {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (I : X.IdealSheafData) (E : X.DivisorFamily) (η : ↥X) : Prop

CP1 along a sequence: at the first stage whose centre contains the strict transform of c = V(closure {η}), the marked transform of I is chain-relative monomial along that strict transform at each of its points.

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Resolution.forall_chainRelativeAt_of_heq {Y Y' : AlgebraicGeometry.Scheme} (h : Y = Y') {E : Y.DivisorFamily} {E' : Y'.DivisorFamily} {I Γ : Y.IdealSheafData} {I' Γ' : Y'.IdealSheafData} (hE : E ≍ E') (hI : I ≍ I') (hΓ : Γ ≍ Γ') (hc : ∀ p ∈ Γ'.support, ChainRelativeAt E' I' Γ' p) (p : ↥Y) : p ∈ Γ.support → ChainRelativeAt E I Γ p

The pointwise chain form transports across an equality of stages.

theorem Hironaka.Resolution.cp1For_concat {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (S : X.BlowUpSequence) (R : S.last.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 η) (hS : CP1For S I E η) (hR : ∀ (η' : ↥S.last), GenericLift S I E 1 η (Fin.last S.length) η' → CP1For R (S.markedTransformSeq I 1 (Fin.last S.length)) (S.totalTransformSeq E (Fin.last S.length)) η') : CP1For (S.concat R) I E η

CP1 along a concatenation: if S satisfies CP1 for η, and for every lift η' of η to the end of S the rest R satisfies CP1 for η' (with the transformed data), then the concatenation satisfies CP1 for η.