The loop's round at stage 0

The round of the loop (Hironaka.Resolution.Algebraic.Wlo05.Embedded) is built from bmoOneRun T hm; its isolated triple and remaining members are isolatedAt and remainingAt at the truncated run. To compute a round at stage 0 one needs the run's constructor: for a run cons X D rest (reached by subst from an equation bmoOneRun T hm = cons X D rest) the truncation at 0 is empty, so

• isolatedAt_cons_zero_I: the isolated ideal is T.I : I_Γ with I_Γ the reduced ideal of the union of the absorbed members;
• isolatedAt_cons_zero_E: the boundary is unchanged; remainingAt_cons_zero: the remaining members are unchanged (the strict transform at stage 0 is the ideal itself);
• filter_centerContains_cons_zero: the members absorbed at stage 0 are those contained in the first centre D (D ≤ c, CenterContains at 0 on a cons).

These are unfoldings of the definitions, used by Hironaka.Resolution.Algebraic.Wlo05.EmbeddedNilInvariant.

theorem Hironaka.Resolution.centerContains_cons_zero_iff {k : Type u} [Field k] (T : MarkedTriple k) (D : T.X.left.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (c : T.X.left.IdealSheafData) : CenterContains (AlgebraicGeometry.Scheme.BlowUpSequence.cons T.X.left D rest) c 0 ↔ D ≤ c

The stop rule at stage 0 on cons X D rest is containment in the first centre.

theorem Hironaka.Resolution.filter_centerContains_cons_zero {k : Type u} [Field k] (T : MarkedTriple k) (D : T.X.left.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (C : Finset T.X.left.IdealSheafData) : {c ∈ C | CenterContains (AlgebraicGeometry.Scheme.BlowUpSequence.cons T.X.left D rest) c 0} = {c ∈ C | D ≤ c}

The members absorbed at stage 0 of a run cons X D rest are those contained in D.

theorem Hironaka.Resolution.filter_not_centerContains_cons_zero {k : Type u} [Field k] (T : MarkedTriple k) (D : T.X.left.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (C : Finset T.X.left.IdealSheafData) : {c ∈ C | ¬CenterContains (AlgebraicGeometry.Scheme.BlowUpSequence.cons T.X.left D rest) c 0} = {c ∈ C | ¬D ≤ c}

The members not absorbed at stage 0 of a run cons X D rest are those not contained in D.

theorem Hironaka.Resolution.isolatedAt_cons_zero_I {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (D : T.X.left.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (hQ : ((AlgebraicGeometry.Scheme.BlowUpSequence.cons T.X.left D rest).take 0).IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.m T.E) (C : Finset T.X.left.IdealSheafData) : (isolatedAt T ((AlgebraicGeometry.Scheme.BlowUpSequence.cons T.X.left D rest).take 0) hQ C).I = T.I.colon (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (⨆ c ∈ C, c.support))

At stage 0 of a run cons X D rest, the isolated ideal is the colon of T.I by the reduced ideal of the union of the absorbed members.

theorem Hironaka.Resolution.isolatedAt_cons_zero_E {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (D : T.X.left.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (hQ : ((AlgebraicGeometry.Scheme.BlowUpSequence.cons T.X.left D rest).take 0).IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.m T.E) (C : Finset T.X.left.IdealSheafData) : (isolatedAt T ((AlgebraicGeometry.Scheme.BlowUpSequence.cons T.X.left D rest).take 0) hQ C).E = T.E

At stage 0 of a run cons X D rest, the boundary of the isolated triple is T.E.

theorem Hironaka.Resolution.remainingAt_cons_zero {k : Type u} [Field k] (T : MarkedTriple k) (D : T.X.left.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (C : Finset T.X.left.IdealSheafData) : remainingAt ((AlgebraicGeometry.Scheme.BlowUpSequence.cons T.X.left D rest).take 0) C = C

At stage 0 of a run cons X D rest, the remaining members are the members themselves.