The loop on a smooth Y: the invariant through the rounds #
The empty succession for a smooth Y (bed_eq_nil_of_smooth,
Hironaka.Resolution.Algebraic.Wlo05.EmbeddedNilCore; [Wlo05, 4.6]: at a smooth point of Y the
invariant is already terminal) is proved by induction on the number of remaining components, with
the invariant Invariant T C on the loop's state (T, C):
- the boundary is empty; the ideal is the product of the members of
C; every member ofCis the reduced ideal of the closure of a generic point of the ideal's support; the members have pairwise disjoint supports; and the ideal is regular stalkwise (the stalk of the ambient at a point of the support modulo the ideal's stalk is a regular local ring — the smoothness ofY, read on the stalks, which survives the removal of components).
Given the CORE LEMMA — for such a triple with a nonempty ideal the first centre of the run of
BMO_1 contains a generic point of the ideal's support (Core; proved in
Hironaka.Resolution.Algebraic.Wlo05.EmbeddedNilCore) — one round of the loop at stage 0 removes
at least one component and preserves the invariant (invariant_isolated_of_cons; the colon by the
absorbed components is the product of the remaining ones, colon_prod_filter), and the loop's
length is 0 (length_bedAux_eq_zero_of_invariant). The terminal round, on the unit ideal, is
empty (length_bedAux_eq_zero_of_eq_top). The initial state satisfies the invariant by
Hironaka.Resolution.Algebraic.Wlo05.EmbeddedNilSmooth.
The loop's invariant on a state (X, I, E, C) — the boundary is empty, the ideal is the
product of the members of C, each member is the reduced ideal of the closure of a generic point
of the ideal's support, the members have pairwise disjoint supports, and the ideal is regular
stalkwise. Stated on the data (I, E, C) over the ambient X (not on the marked triple), so that a
round of the loop — whose isolated triple has the SAME ambient scheme only definitionally — is a
change away.
- mem (c : X.IdealSheafData) : c ∈ C → ∃ η ∈ I.support.genericPoints, c = AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})
- pairwise : (↑C).Pairwise fun (a b : X.IdealSheafData) => Disjoint a.support b.support
- regular (x : ↥X) : x ∈ I.support → IsRegularLocalRing (↑(X.presheaf.stalk x) ⧸ I.stalkIdeal x)
Instances For
The core lemma of the smooth case, as a hypothesis — for a marked triple of mark 1 with
empty boundary whose ideal is regular stalkwise and not the unit ideal, the run of BMO_1 starts
with a blow-up whose centre contains a generic point of the ideal's support (the maximal-contact
descent of the round of order 1 ends at a component of Y itself).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The members of C are radical: each is the vanishing ideal of its support.
The support of the ideal is the union of the supports of the members.
A point of the support lies in the support of some member.
The component of a generic point of the support is a member of C.
The ideal is not the unit ideal when C is nonempty.
The ideal is the unit ideal when C is empty.
A generic point of a member's support lies in the ideal's support.
One round at stage 0 preserves the invariant #
The isolated ideal at stage 0 is the product of the remaining members — the colon of the
product over C by the reduced ideal of the absorbed members (colon_prod_filter).
The product over a sub-finset is at least the product over the finset.
The stalk of a product of members with pairwise disjoint supports at a point of one member's support is that member's stalk.
Removing members preserves the invariant — the product over a sub-finset F ⊆ C with the
same boundary satisfies the invariant: its support is the union of the remaining members'
supports, a generic point of I's support in it stays generic (the support shrinks), and the stalk
of the product at a point of a remaining member is the stalk of I there.
One round at stage 0 preserves the invariant — for a run S = cons X D rest (the subst
form, for the run bmoOneRun T hm through hrun), the isolated triple with the remaining members
satisfies the invariant: the absorbed members are those contained in D
(filter_centerContains_cons_zero), the boundary is unchanged, the ideal is the product of the
remaining members (isolatedAt_cons_zero_I_eq_prod), and removing members preserves the invariant
(invariant_prod_filter). The isolated triple's ambient scheme is T.X.left definitionally, hence
the change.
The loop is empty on a state satisfying the invariant #
The loop has length 0 on every state satisfying the invariant, given the core lemma — by
strong induction on the number of members: a round at stage 0 removes the absorbed components
(at least the one through the generic point the core lemma provides) and preserves the invariant;
the terminal round on the unit ideal is empty.