Proper simple normal crossings of the final strict transform #
The proper form of clause (3) of [Wlo09, Theorem 2.0.2] for an embedded desingularization functor
bed : BEDanFamStar 𝕜: for every dimension n, every triple of the class DomBEDan and every
relatively compact open U, the final strict transform Ỹ of the value on U is non-singular and,
at every point of its cosupport, has a chart adapted to Ỹ which is a simple-normal-crossing chart
of the final exceptional family E_r in which no component's coordinate is one of the coordinates
of Ỹ (HasSncWithProper at the point's codimension). Kollár's simple normal crossings of a
subvariety with a divisor allows components of the divisor to contain the subvariety
[Kol07, Definition 24]; the output of Włodarczyk's modified algorithm is a smooth submanifold whose
coordinates are "transversal to exceptional divisors" (the proof of [Wlo09, Theorem 7.4.1]), which
is the proper form. Clause (3) of BEDanFamStar.IsEmbeddedDesing is this text without the last
conjunct; the proper form follows from it (IsEmbeddedDesing.isProperSnc in
Hironaka/Resolution/Analytic/Wlo09/ProperSncOfEmbeddedDesing.lean).
The predicate is a named Prop so that the theorems about the resolution of analytic spaces can
bind hbed : bed.IsEmbeddedDesing alone and write hbed.isProperSnc.
bed has proper simple normal crossings: for every n, every triple T of the class
DomBEDan on a manifold M modelled on 𝕜ⁿ and every relatively compact open U, with L the
value ((bed.fam n).fam T hT).seqOn U hU and
Ỹ := L.strictTransformSubspaceSeq (T|U).I (Fin.last _), E_r := L.totalTransformSeq (Fin.last _):
Ỹ is non-singular, and at every point of its cosupport
there are a codimension c, a chart φ adapted to Ỹ.cosupport with index embedding σ, and
component indices cidx making φ a simple-normal-crossing chart of E_r there, with
cidx j ∉ Set.range σ for every component j through the point (the proper conjunct;
HasSncWithProper, Snc/Proper.lean). Clause (3) of IsEmbeddedDesing is this text without the
last conjunct.
Equations
- One or more equations did not get rendered due to their size.