The isolated marked ideal at the absorbing stage

In the isolation passage of the proof of [Wlo05, Theorem 4.7.1], at the first stage n whose centre contains the strict transform of a component, the modified run replaces the marked ideal I_n by the colon I' := I_n : I_Γ, I_Γ the reduced ideal of the union Γ of the absorbed strict transforms, and restarts. This module reads that isolation stalkwise, in the index form of the stages of the run, under the invariant InvCE of the loop and the hypothesis ClaimKC (Włodarczyk's Claim in Kollár's setting, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedHypotheses):

• the absorbed strict transforms are pairwise disjoint (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedDisjoint), so I_Γ is their product;
• I_n = I' · I_Γ: at a point of an absorbed c̃, I_n = M(I_n) · c̃ (Włodarczyk's Claim, through Hironaka.Resolution.Algebraic.Wlo05.EmbeddedAbsorbed), I_Γ = c̃, and (M c̃ : c̃) · c̃ = M c̃; off Γ the colon is by the unit ideal;
• the monomial part is unchanged, M(I') = M(I_n): its exponents are the orders at the generic points of the components of the members of the boundary, which lie off Γ (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedNotContained);
• N(I') = 1 along Γ: M(I_n) ≤ I' at the points of Γ, so the colon I' : M(I') is the unit ideal there;
• N(I_n) ≤ N(I'): the nonmonomial support can only shrink at the isolation.

The splitting I = M(I) · N(I) is that of [Kol07, Definition–Lemma 110]. Since ClaimKC is false for the transcribed order, the theorems of this module are CONDITIONAL lemmas; the definitions (absorbIndex, absorbed, absorbedIdeal, isolatedMarkedIdeal) and the unconditional bookkeeping are used by Hironaka.Resolution.Algebraic.Wlo05.EmbeddedRemaining, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedIsolatedState, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedStep and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Remaining. The unconditional treatment of the isolated ideal is CP2 (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP2Entry) and CP6 (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Isolation).

theorem Hironaka.Resolution.mem_biSup_closeds_iff {X : AlgebraicGeometry.Scheme} {ι : Type v} (A : Finset ι) (Z : ι → TopologicalSpace.Closeds ↥X) (x : ↥X) : x ∈ ⨆ a ∈ A, Z a ↔ ∃ a ∈ A, x ∈ Z a

A point lies in the supremum of finitely many closed sets iff it lies in one of them.

noncomputable def Hironaka.Resolution.absorbIndex {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) : Fin (bmoOneRun T hm).length

The absorbing stage Nat.find h of the loop as a centre index of the run (find_lt_length).

Equations

• Hironaka.Resolution.absorbIndex T hm C h = ⟨Nat.find h, ⋯⟩

noncomputable def Hironaka.Resolution.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) : Finset T.X.left.IdealSheafData

The members absorbed at the absorbing stage — the filter in the definition of isolatedTriple.

Equations

• Hironaka.Resolution.absorbed T hm C h = {c ∈ C | Hironaka.Resolution.CenterContains (Hironaka.Resolution.bmoOneRun T hm) c (Nat.find h)}

noncomputable def Hironaka.Resolution.absorbedIdeal {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) : ((bmoOneRun T hm).stage (absorbIndex T hm C h).castSucc).IdealSheafData

Włodarczyk's I_Γ at the absorbing stage, in index form: the reduced ideal of the union of the absorbed strict transforms ([Wlo05, Theorem 4.7.1, proof]).

Equations

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

noncomputable def Hironaka.Resolution.isolatedMarkedIdeal {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) : ((bmoOneRun T hm).stage (absorbIndex T hm C h).castSucc).IdealSheafData

Włodarczyk's isolated marked ideal I_n : I_Γ at the absorbing stage, in index form ([Wlo05, Theorem 4.7.1, proof]).

Equations

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

theorem Hironaka.Resolution.absorbed_subset {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} : absorbed T hm C h ⊆ C

The absorbed members are members.

theorem Hironaka.Resolution.absorbed_spec {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} (hinv : InvCE T.I T.E C) {c : T.X.left.IdealSheafData} (hc : c ∈ absorbed T hm C h) : ∃ η ∈ T.I.support.genericPoints, c = AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η}) ∧ (∀ (i : T.E.ι), η ∉ (T.E.component i).support) ∧ T.I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η ∧ CenterContains (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) ↑(absorbIndex T hm C h) ∧ ∀ m < ↑(absorbIndex T hm C h), ¬CenterContains (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) m

The data of an absorbed member: the invariant of the loop gives its generic point η, off the boundary, at which T.I agrees with it; the stop rule gives absorption at the stage of the loop and at none before.

theorem Hironaka.Resolution.pairwise_disjoint_strictTransformSeq_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} (hinv : InvCE T.I T.E C) (hKC : ClaimKC k) : (↑(absorbed T hm C h)).Pairwise fun (a b : T.X.left.IdealSheafData) => Disjoint ((bmoOneRun T hm).strictTransformSeq a (absorbIndex T hm C h).castSucc).support ((bmoOneRun T hm).strictTransformSeq b (absorbIndex T hm C h).castSucc).support

The absorbed strict transforms are pairwise disjoint (the disjointness of [Wlo05, Theorem 4.7.1] for the loop; conditional on ClaimKC).

theorem Hironaka.Resolution.absorbedIdeal_eq_prod {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} (hinv : InvCE T.I T.E C) (hKC : ClaimKC k) : absorbedIdeal T hm C h = ∏ c ∈ absorbed T hm C h, (bmoOneRun T hm).strictTransformSeq c (absorbIndex T hm C h).castSucc

Włodarczyk's I_Γ is the product of the absorbed strict transforms (each is integral, hence the vanishing ideal of its support; pairwise disjoint). Conditional on ClaimKC.

theorem Hironaka.Resolution.stalkIdeal_absorbedIdeal_of_mem {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} (hinv : InvCE T.I T.E C) (hKC : ClaimKC k) {c : T.X.left.IdealSheafData} (hc : c ∈ absorbed T hm C h) {p : ↥((bmoOneRun T hm).stage (absorbIndex T hm C h).castSucc)} (hp : p ∈ ((bmoOneRun T hm).strictTransformSeq c (absorbIndex T hm C h).castSucc).support) : (absorbedIdeal T hm C h).stalkIdeal p = ((bmoOneRun T hm).strictTransformSeq c (absorbIndex T hm C h).castSucc).stalkIdeal p

The stalk of I_Γ at a point of an absorbed strict transform is the stalk of that strict transform. Conditional on ClaimKC.

theorem Hironaka.Resolution.markedTransformSeq_eq_isolatedMarkedIdeal_mul_absorbedIdeal {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} (hinv : InvCE T.I T.E C) (hKC : ClaimKC k) : (bmoOneRun T hm).markedTransformSeq T.I 1 (absorbIndex T hm C h).castSucc = isolatedMarkedIdeal T hm C h * absorbedIdeal T hm C h

I_n = (I_n : I_Γ) · I_Γ (the isolation of [Wlo05, Theorem 4.7.1, proof]; conditional on ClaimKC): stalkwise, at a point of an absorbed c̃, I_n = M(I_n) · c̃ and (M c̃ : c̃) · c̃ = M c̃; off Γ the colon is by the unit ideal.

theorem Hironaka.Resolution.monomialPart_isolatedMarkedIdeal {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} (hinv : InvCE T.I T.E C) (hKC : ClaimKC k) : BMO.monomialPart (isolatedMarkedIdeal T hm C h) ((bmoOneRun T hm).totalTransformSeq T.E (absorbIndex T hm C h).castSucc) = BMO.monomialPart ((bmoOneRun T hm).markedTransformSeq T.I 1 (absorbIndex T hm C h).castSucc) ((bmoOneRun T hm).totalTransformSeq T.E (absorbIndex T hm C h).castSucc)

The monomial part is unchanged by the isolation (conditional on ClaimKC): its exponents are the orders at the generic points of the components of the members of the boundary, which lie off Γ (notMem_strictTransformSeq_support_of_mem_genericPoints_component), where the colon by I_Γ changes nothing.

theorem Hironaka.Resolution.stalkIdeal_nonmonomialPart_isolatedMarkedIdeal_eq_top {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} (hinv : InvCE T.I T.E C) (hKC : ClaimKC k) {c : T.X.left.IdealSheafData} (hc : c ∈ absorbed T hm C h) {p : ↥((bmoOneRun T hm).stage (absorbIndex T hm C h).castSucc)} (hp : p ∈ ((bmoOneRun T hm).strictTransformSeq c (absorbIndex T hm C h).castSucc).support) : (BMO.nonmonomialPart (isolatedMarkedIdeal T hm C h) ((bmoOneRun T hm).totalTransformSeq T.E (absorbIndex T hm C h).castSucc)).stalkIdeal p = ⊤

The nonmonomial part of the isolated marked ideal is the unit ideal along the absorbed strict transforms (conditional on ClaimKC): at such a point M(I') = M(I_n) ≤ I' = (M(I_n) c̃ : c̃).

theorem Hironaka.Resolution.nonmonomialPart_le_nonmonomialPart_isolatedMarkedIdeal {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} (hinv : InvCE T.I T.E C) (hKC : ClaimKC k) : BMO.nonmonomialPart ((bmoOneRun T hm).markedTransformSeq T.I 1 (absorbIndex T hm C h).castSucc) ((bmoOneRun T hm).totalTransformSeq T.E (absorbIndex T hm C h).castSucc) ≤ BMO.nonmonomialPart (isolatedMarkedIdeal T hm C h) ((bmoOneRun T hm).totalTransformSeq T.E (absorbIndex T hm C h).castSucc)

The nonmonomial part can only shrink at the isolation: N(I_n) ≤ N(I_n : I_Γ) (the monomial parts agree and I_n ≤ I_n : I_Γ). Conditional on ClaimKC.