Step 2.2 of order reduction: restricting to the hypersurface of maximal contact #
Step 2.2 of the proof of [Kol07, Theorem 103] ([Kol07, 104, Step 2.2]) starts from the triple
(X, I, E) left by Step 2.1 together with a smooth hypersurface of maximal contact H such that
H + E has simple normal crossings; it replaces I by W(I) once more, keeps the birational
transforms of the old hypersurfaces of maximal contact rather than choosing new ones, declares H
the first member E^0 of H + E, and applies the boundary-clearing functor of [Kol07, Lemma 102]
to (X, I, H + E) at that member. The resulting sequence Π : X_r → X has cosupp Π⁻¹_*(I, m)
disjoint from Π⁻¹_* H; since H is of maximal contact, the cosupport lies in Π⁻¹_* H, hence
"cosupp Π⁻¹_*(I, m) = ∅, as we wanted".
This module defines the objects of Step 2.2, of Step 2 and of the maximal-contact case of
BO_{n,m}; the theorems about them are in
Hironaka/Resolution/Algebraic/OrderReduction/Step22Basic.lean, Step22Cosupp.lean,
Step22Indep.lean and Step22Assembly.lean.
- The Step 2.2 input triple (
step22Triple). WithS₁the Step 2.1 sequence (step21Seqafter allcard E.ιrounds),X_r := S₁.last,I_r := Π⁻¹_* I,E_r := Π⁻¹_tot EandH_r := Π⁻¹_* H, this is the triple(X_r, I_r, F_r + H_r), whereF_ris the exceptional sub-family ofE_r(exceptionalFamily: the members that are not birational transforms of original members) andH_ris appended last. Kollár's(X, I, H + E)with the fullE_ris not used, because the birational transforms of the original members may fail to have normal crossings withH_raway from the cosupport, whereasF_r + H_rhas normal crossings everywhere (isSnc_exceptionalFamily_append). The transforms of the original members are disjoint fromcosupp(I_r, m)(Hironaka/Resolution/Algebraic/OrderReduction/Step21Disjoint.lean), hence from every later centre, so the two families agree wherever the normal-crossings clause of [Kol07, Definition 66] looks; the order condition for the original(I_r, E_r)is recovered inStep22Basic.lean(isOrderSeq_step22_totalTransformSeq). Kollár's "E^0 := Hfirst,j = 0" becomes the positioncard F_r.ιofH_r. - The re-tuning of Step 2.2 (
step22Functor). Kollár's "we can again replaceIbyW(I)" is made explicit: the boundary-clearing functor of [Kol07, Lemma 102] at the markmonBDClass n m jis obtained from the one at the marks(m)exactly as Step 1 obtainsBO_{n,m}from the tuned functor (OrderSeqAssignment.ofTunedClass):BD_{n,s(m),j}applied to the tuned triple(X, W_{s(m)}(I), E)whenmax-ord I = m, the empty sequence below the mark (bdClass_tunedsupplies the class obligation). The databd : ∀ m j, BDData n m jare therefore Lemma 102 at every mark, which the induction on the dimension supplies. - Step 2.2 (
step22):step22Functorat the position ofH_r, applied tostep22Triple, which lies in the boundary-clearing class (bdClass_step22Triple:dim X_r ≤ nalong the stage map,max-ord I_r ≤ m, and the position). - Step 2 (
step2Seq): Step 2.1 followed by Step 2.2 (concat). - The maximal-contact case of
BO_{n,m}(maxContactCase): on a triple ofBOClass n mwith a smooth hypersurfaceHof maximal contact for(I, m), the Step 2 sequence of the tuned triple(X, W_{s(m)}(I), E)at the marks(m)whenmax-ord I = m, and the empty sequence whenmax-ord I < m, the case split ofOrderSeqAssignment.ofTunedClass.Hstays of maximal contact for the tuned ideal becauseMC(W_s(I)) = MC(I)([Kol07, Proposition 99 (4)];retune_keeps_maxContact, used again at Step 2.2 forH_r). Its dependence onHis only through Step 2.2. The sequence has no empty blow-up, so the deletion of empty blow-ups of [Kol07, 32] is the identity on it (Step22Assembly.lean).
A smooth hypersurface of maximal contact for (I, m) is one for the tuned
(W_{s(m)}(I), s(m)): MC(W_s(I)) = MC(I) ([Kol07, Proposition 99 (4)];
isMaximalContact_W_tuningParam). The old hypersurface is kept after re-tuning, as
[Kol07, 104, Step 2.2] prescribes.
A triple of the boundary-clearing class BDClass n m j with max-ord I = m tunes into
BDClass n (s(m)) j (maxOrd_tuned, hasDimLE_tuned).
The boundary-clearing functor of [Kol07, Lemma 102] at the mark m through the re-tuning
("we can again replace I by W(I)", [Kol07, 104, Step 2.2]): BD_{n,s(m),j} on the tuned triple
when max-ord I = m, the empty sequence below the mark (OrderSeqAssignment.ofTunedClass, exactly
as Step 1 of Theorem 103).
Equations
- Hironaka.BO.step22Functor bd m j hm = ((bd (IsLocalRing.tuningParam m) j).functor k).ofTunedClass ⋯ ⋯
Instances For
The triple induced at the last stage of a smooth blow-up sequence has dim ≤ n, the stage map
being smooth of the same relative dimension (the first clause of bdClass_induced_last).
The ideal induced at the last stage of a smooth blow-up sequence of order m without empty
blow-ups has max-ord ≤ m: by [Kol07, Definition 66] at the mark, and because the sequence is
empty below it (the second clause of bdClass_induced_last).
The Step 2.2 input triple (X_r, I_r, F_r + H_r) ([Kol07, 104, Step 2.2]): the triple
induced at the end of Step 2.1, with its boundary replaced by the exceptional sub-family of E_r
followed by H_r, appended last (Kollár's "E^0 := H first" is the position card F_r.ι). Its
normal-crossings field is isSnc_exceptionalFamily_append: F_r + H_r has normal crossings
everywhere.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Step 2.2 input triple lies in the boundary-clearing class at the position of H_r
([Kol07, 104, Step 2.2]: "apply (102) to (X, I, H + E) with j = 0").
Step 2.2 ([Kol07, 104, Step 2.2]): the boundary-clearing functor at the position of H_r,
through the re-tuning (step22Functor), applied to the Step 2.2 input triple.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Step 2 of the proof of [Kol07, Theorem 103], on a triple with max-ord I ≤ m and a smooth
hypersurface of maximal contact H: Step 2.1 followed by Step 2.2 (concat).
Equations
- Hironaka.BO.step2Seq T hn hmax bd hm hH hle = (↑(Hironaka.BO.step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).concat (Hironaka.BO.step22 T hn hmax bd hm hH hle)
Instances For
BO_{n,m} in the maximal-contact case, BO^H_{n,m}(X, I, E) (Steps 1–2 of the proof of
[Kol07, Theorem 103]): for a triple of BOClass n m with a smooth hypersurface H of maximal
contact for (I, m) and the boundary-clearing data at every mark, the Step 2 sequence of the tuned
triple (X, W_{s(m)}(I), E) at the mark s(m) when max-ord I = m (Step 1; H stays of maximal
contact by retune_keeps_maxContact), and the empty sequence when max-ord I < m (the remark
after [Kol07, Theorem 68]): the case split of OrderSeqAssignment.ofTunedClass.
Equations
- Hironaka.BO.maxContactCase T hT hH hle bd = if h : T.I.maxOrd = ↑m then Hironaka.BO.step2Seq (T.tuned m ⋯) ⋯ ⋯ bd ⋯ hH ⋯ else AlgebraicGeometry.Scheme.BlowUpSequence.nil T.X.left