Tools for the loop of the un-isolated ideal

The loop theorem of the statement CP6 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative; Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Loop) is a strong induction on the number of members along bedAux: at an absorbing stage the goal transports across the concatenation, the isolation identity re-establishes the invariant with the ENLARGED protected set — the transports of the protected components and the strict transforms of the newly absorbed members — and the induction hypothesis applies to the isolated triple. This module holds the bookkeeping of that step:

• heq_inf, heq_biInf — a meet, or a finite meet, of ideal sheaves transports across a cast of the ambient scheme (the casts of the concatenation and of the truncation);
• forall_chainRelativeKAt_of_heq — the K-shape along a closed subscheme transports across a cast (the bridge from the last stage of the truncation, where CP5 states the protected state, to the stage of the run);
• eq_of_take_strictTransformSeq_eq — two members with the same strict transform at the absorbing stage coincide (eq_of_strictTransformSeq_eq of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedRemaining through the identification of the last stage of the truncation): the injectivity that the separation of the members not yet absorbed needs;
• pairwise_disjoint_transported_of_absorbed — the transported protected set at the absorbing stage is pairwise disjoint (transport of the disjointness of the protected components, CP1 for the absorbed members, the disjointness of the protected state from the members across the two families);
• mem_transported_of_absorbed — every protected component and every member has its strict transform in the transported protected set or among the remaining members.

Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Loop and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP5.

theorem Hironaka.Resolution.heq_inf {Y Y' : AlgebraicGeometry.Scheme} (h : Y = Y') {a b : Y.IdealSheafData} {a' b' : Y'.IdealSheafData} (ha : a ≍ a') (hb : b ≍ b') : a ⊓ b ≍ a' ⊓ b'

A meet of two ideal sheaves transports across a cast of the ambient scheme.

theorem Hironaka.Resolution.heq_biInf {Y Y' : AlgebraicGeometry.Scheme} (h : Y = Y') {ι : Type u_1} (A : Finset ι) {f : ι → Y.IdealSheafData} {g : ι → Y'.IdealSheafData} (hfg : ∀ (a : ι), f a ≍ g a) : ⨅ a ∈ A, f a ≍ ⨅ a ∈ A, g a

A finite meet of ideal sheaves transports across a cast of the ambient scheme.

theorem Hironaka.Resolution.forall_chainRelativeKAt_of_heq {Y Y' : AlgebraicGeometry.Scheme} (h : Y = Y') {E : Y.DivisorFamily} {E' : Y'.DivisorFamily} (hE : E ≍ E') {K Γ : Y.IdealSheafData} {K' Γ' : Y'.IdealSheafData} (hK : K ≍ K') (hΓ : Γ ≍ Γ') (hs : ∀ p ∈ Γ.support, ChainRelativeKAt E K Γ p) (p : ↥Y') : p ∈ Γ'.support → ChainRelativeKAt E' K' Γ' p

The K-shape along a closed subscheme transports across a cast of the ambient scheme.

theorem Hironaka.Resolution.eq_of_take_strictTransformSeq_eq {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) {c₁ c₂ : T.X.left.IdealSheafData} (hc₁ : c₁ ∈ C) (hc₂ : c₂ ∈ C) (heq : ((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)).strictTransformSeq c₂ (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)) : c₁ = c₂

Two members with the same strict transform at the absorbing stage coincide (eq_of_strictTransformSeq_eq in the truncated form).

theorem Hironaka.Resolution.pairwise_disjoint_transported_of_absorbed {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) (Γs : Finset T.X.left.IdealSheafData) (hP : ∀ γ ∈ Γs, ProtectedState T C γ) (hdisj : (↑Γs).Pairwise fun (a b : T.X.left.IdealSheafData) => Disjoint a.support b.support) : (↑(Finset.image (fun (γ : T.X.left.IdealSheafData) => ((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq γ (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)) Γs ∪ Finset.image (fun (c : T.X.left.IdealSheafData) => ((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq c (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)) ({c ∈ C | CenterContains (bmoOneRun T hm) c (Nat.find h)}))).Pairwise fun (a b : (((bmoOneRun T hm).take (Nat.find h)).stage (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)).IdealSheafData) => Disjoint a.support b.support

The transported protected set at the absorbing stage is pairwise disjoint (transport of the disjointness of the protected components, CP1 for the absorbed members, and the disjointness of the protected state from the members across the two).

theorem Hironaka.Resolution.mem_transported_of_absorbed {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (h : ∃ (n : ℕ), HasAbsorptionAt T hm C n) (Γs : Finset T.X.left.IdealSheafData) (z : T.X.left.IdealSheafData) : z ∈ Γs ∪ C → ((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq z (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length) ∈ Finset.image (fun (γ : T.X.left.IdealSheafData) => ((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq γ (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)) Γs ∪ Finset.image (fun (c : T.X.left.IdealSheafData) => ((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq c (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)) ({c ∈ C | CenterContains (bmoOneRun T hm) c (Nat.find h)}) ∪ Finset.image (fun (c : T.X.left.IdealSheafData) => ((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq c (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)) ({c ∈ C | ¬CenterContains (bmoOneRun T hm) c (Nat.find h)})

Every protected component and every member has its strict transform at the absorbing stage in the transported protected set or among the remaining members.