The isolation identity at the absorbing stage

The statement CP6 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) re-establishes the invariant I = I_Γ ⊓ K of the un-isolated ideal at the isolation step of the loop: at the first absorbing stage n = Nat.find h of a round, the transform K_n of the ideal of the loop is I_abs ⊓ (K_n : I_abs), where I_abs is the reduced ideal of the union of the absorbed strict transforms and K_n : I_abs the isolated ideal (isolatedTriple T hm C n, Hironaka.Resolution.Algebraic.Wlo05.Embedded). This module proves that identity and its bookkeeping:

• stageTriple_I — the ideal of the stage triple is the mark-1 transform along the truncated run (the mark is 1 by hm);
• the one-blow-up bridge strictTransform_biInf_of_pairwise_disjoint and the pairwise disjointness of the transported family pairwise_disjoint_strictTransformSeq_support (the ideal of a disjoint union along one blow-up);
• vanishingIdeal_absorbed_eq_biInf — I_abs is the intersection of the absorbed strict transforms (each integral by isIntegral_take_strictTransformSeq_of_mem); isolatedTriple_I_eq_colon_biInf — the isolated ideal is the colon by that intersection;
• the isolation identity markedTransformSeq_take_eq_biInf_inf_colon (and its form with the ideal of the isolated triple, markedTransformSeq_take_eq_biInf_inf_isolatedTriple_I): stalkwise, at a point of an absorbed c̃ the transform is in chain form along c̃ (CP1, chainRelativeAt_of_absorbed), so it is c̃_p ⊓ (K_n : c̃)_p by the intersection form (stalkIdeal_eq_inf_colon_of_chainRelativeAt), and I_abs has the stalk of c̃ there (the absorbed transforms are pairwise disjoint, CP1); off the absorbed transforms I_abs is 𝒪 and the colon is K_n itself.

With the transport of the intersection form along the run (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Stage under the protected states of CP5), the isolation step of the loop becomes a rewrite: (⨅ Γ̃) ⊓ K_n = (⨅ Γ̃) ⊓ (⨅ c̃) ⊓ (K_n : I_abs). This is the isolation of the proof of [Wlo05, Theorem 4.7.1], proved from the chain form. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Loop, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Stage and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP5.

theorem Hironaka.Resolution.stageTriple_I {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (n : ℕ) : (stageTriple T hm n).I = ((bmoOneRun T hm).take n).markedTransformSeq T.I 1 (Fin.last ((bmoOneRun T hm).take n).length)

The ideal of the stage triple is the mark-1 transform of the loop's ideal along the truncated run (the mark is 1 by hm).

theorem Hironaka.Resolution.strictTransform_biInf_of_pairwise_disjoint {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (D : X.IdealSheafData) (Γs : Finset X.IdealSheafData) (hred : ∀ γ ∈ Γs, AlgebraicGeometry.IsReduced γ.subscheme) (hdisj : (↑Γs).Pairwise fun (a b : X.IdealSheafData) => Disjoint a.support b.support) : (⨅ γ ∈ Γs, γ).strictTransform D = ⨅ γ ∈ Γs, γ.strictTransform D

The one-blow-up bridge: the strict transform of a disjoint union of reduced closed subschemes along one blow-up is the intersection of the strict transforms (strictTransformSeq_biInf_of_pairwise_disjoint on the one-step sequence).

theorem Hironaka.Resolution.pairwise_disjoint_strictTransformSeq_support {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (S : X.BlowUpSequence) (Γs : Finset X.IdealSheafData) (hdisj : (↑Γs).Pairwise fun (a b : X.IdealSheafData) => Disjoint a.support b.support) (i : Fin (S.length + 1)) : (↑(Finset.image (fun (γ : X.IdealSheafData) => S.strictTransformSeq γ i) Γs)).Pairwise fun (a b : (S.stage i).IdealSheafData) => Disjoint a.support b.support

Pairwise disjointness of the supports of the strict transforms of a disjoint family.

theorem Hironaka.Resolution.vanishingIdeal_absorbed_eq_biInf {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (hinv : InvCE T.I T.E C) (h : ∃ (n : ℕ), HasAbsorptionAt T hm C n) : AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (⨆ c ∈ {c ∈ C | CenterContains (bmoOneRun T hm) c (Nat.find h)}, (((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq c (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)).support) = ⨅ c ∈ {c ∈ C | CenterContains (bmoOneRun T hm) c (Nat.find h)}, ((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq c (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)

The ideal of the absorbed strict transforms at the absorbing stage: the reduced ideal of their union is their intersection (each is integral, isIntegral_take_strictTransformSeq_of_mem).

theorem Hironaka.Resolution.isolatedTriple_I_eq_colon_biInf {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (hinv : InvCE T.I T.E C) (h : ∃ (n : ℕ), HasAbsorptionAt T hm C n) : (isolatedTriple T hm C (Nat.find h)).I = (((bmoOneRun T hm).take (Nat.find h)).markedTransformSeq T.I 1 (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)).colon (⨅ c ∈ {c ∈ C | CenterContains (bmoOneRun T hm) c (Nat.find h)}, ((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq c (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length))

The isolated ideal is the colon of the transform of the ideal of the loop by the intersection of the absorbed strict transforms (the definition of isolatedTriple with vanishingIdeal_absorbed_eq_biInf).

theorem Hironaka.Resolution.markedTransformSeq_take_eq_biInf_inf_colon {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (hinv : InvCE T.I T.E C) (h : ∃ (n : ℕ), HasAbsorptionAt T hm C n) : ((bmoOneRun T hm).take (Nat.find h)).markedTransformSeq T.I 1 (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length) = (⨅ c ∈ {c ∈ C | CenterContains (bmoOneRun T hm) c (Nat.find h)}, ((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq c (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)) ⊓ (((bmoOneRun T hm).take (Nat.find h)).markedTransformSeq T.I 1 (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)).colon (⨅ c ∈ {c ∈ C | CenterContains (bmoOneRun T hm) c (Nat.find h)}, ((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq c (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length))

The isolation identity, the colon form: at the first absorbing stage the transform K of the ideal of the loop is I_abs ⊓ (K : I_abs) with I_abs the ideal of the absorbed strict transforms. Stalkwise: at a point of an absorbed c̃ the transform is in chain form along c̃ (CP1), so it is c̃_p ⊓ (K : c̃)_p (the intersection form), and I_abs has the stalk of c̃ there (CP1); off the absorbed transforms I_abs is 𝒪 and the colon is K itself.

theorem Hironaka.Resolution.markedTransformSeq_take_eq_biInf_inf_isolatedTriple_I {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (hinv : InvCE T.I T.E C) (h : ∃ (n : ℕ), HasAbsorptionAt T hm C n) : ((bmoOneRun T hm).take (Nat.find h)).markedTransformSeq T.I 1 (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length) = (⨅ c ∈ {c ∈ C | CenterContains (bmoOneRun T hm) c (Nat.find h)}, ((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq c (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)) ⊓ (isolatedTriple T hm C (Nat.find h)).I

The isolation identity with the ideal of the isolated triple: K_n = I_abs ⊓ (isolatedTriple).I.