The intersection form along a sequence, with per-stage hypotheses

The statement CP6 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) follows the un-isolated ideal I = I_A ⊓ K through the blow-ups of a round: at each stage the mark-1 transform of I is the meet of the strict transforms of the protected components with the mark-1 transform of K, provided each blow-up is admissible for K along the protected components (the sheaf form of CP4, markedTransform_biInf_inf_of_admissible of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP4Sheaf). This module proves that transport with PER-STAGE hypotheses, the form that the protected states of CP5 instantiate on the run of BMO_1 (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Loop):

• markedTransformSeq_eq_biInf_inf_of_forall_stage: for I₀ = (⨅ γ ∈ Γs, γ) ⊓ K with Γs reduced and pairwise disjoint, if at every stage the ambient scheme is smooth, the boundary is snc, each transported γ̃_i is smooth and snc with it, K_i has the K-shape along γ̃_i and is admissible at the centre, and K_i ≤ Z_i, then I_i = (⨅ γ, γ̃_i) ⊓ K_i at every stage — the transport engine markedTransformSeq_eq_inf_of_forall_step on the single protected ideal P := ⨅ γ ∈ Γs, γ, with the disjoint-union bridge strictTransformSeq_biInf_of_pairwise_disjoint at every stage (its reducedness input needed at stage 0 only) and the finset form of CP4 at each blow-up on the transported family, whose pairwise disjointness is pairwise_disjoint_strictTransformSeq_support.

This statement is not in the literature.

theorem Hironaka.Resolution.markedTransformSeq_eq_biInf_inf_of_forall_stage {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (S : X.BlowUpSequence) (E : X.DivisorFamily) (K I₀ : X.IdealSheafData) (Γs : Finset X.IdealSheafData) (hred : ∀ γ ∈ Γs, AlgebraicGeometry.IsReduced γ.subscheme) (hdisj : (↑Γs).Pairwise fun (a b : X.IdealSheafData) => Disjoint a.support b.support) (hI₀ : I₀ = (⨅ γ ∈ Γs, γ) ⊓ K) (hst : ∀ (i : Fin S.length), AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp (S.stageMap i.castSucc) f)) (hE : ∀ (i : Fin S.length), (S.totalTransformSeq E i.castSucc).IsSnc) (hΓ : ∀ (i : Fin S.length), ∀ γ ∈ Γs, (S.totalTransformSeq E i.castSucc).HasSncWith (S.strictTransformSeq γ i.castSucc)) (hsm : ∀ (i : Fin S.length), ∀ γ ∈ Γs, AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp (S.strictTransformSeq γ i.castSucc).subschemeι (CategoryTheory.CategoryStruct.comp (S.stageMap i.castSucc) f))) (hK : ∀ (i : Fin S.length), ∀ γ ∈ Γs, ∀ p ∈ (S.strictTransformSeq γ i.castSucc).support, ChainRelativeKAt (S.totalTransformSeq E i.castSucc) (S.markedTransformSeq K 1 i.castSucc) (S.strictTransformSeq γ i.castSucc) p) (hZ : ∀ (i : Fin S.length), ∀ γ ∈ Γs, ∀ p ∈ (S.center i).support ⊓ (S.strictTransformSeq γ i.castSucc).support, AdmissibleChainStratumKAt (S.totalTransformSeq E i.castSucc) (S.markedTransformSeq K 1 i.castSucc) (S.strictTransformSeq γ i.castSucc) (S.center i) p) (hKZ : ∀ (i : Fin S.length), S.markedTransformSeq K 1 i.castSucc ≤ S.center i) (i : Fin (S.length + 1)) : S.markedTransformSeq I₀ 1 i = (⨅ γ ∈ Γs, S.strictTransformSeq γ i) ⊓ S.markedTransformSeq K 1 i

The intersection form along a sequence, with per-stage hypotheses: for I₀ = (⨅ γ ∈ Γs, γ) ⊓ K with Γs reduced and pairwise disjoint, if at every stage the boundary is snc, each transported γ̃_i is smooth and snc with it, K_i has the K-shape along γ̃_i and is admissible at the centre, and K_i ≤ Z_i, then at every stage I_i = (⨅ γ, γ̃_i) ⊓ K_i.