Step 3 of order reduction: the local class, the local functor and the globalised functor #
Step 3 of the proof of [Kol07, Theorem 103] removes the assumption of a global hypersurface of
maximal contact: X is covered by open subsets X^(j) on each of which a smooth hypersurface of
maximal contact H^(j) exists, the disjoint union H^* = ∐ H^(j) ⊂ ∐ X^(j) = X^* is a smooth
hypersurface of maximal contact for the pulled-back data, Step 2 defines BO_{n,m} on
(X^*, g^* I, g^{-1} E) for the coproduct g : X^* → X of the inclusions, and the value descends
to BO_{n,m}(X, I, E) by the argument of [Kol07, Proposition 37]. The descent is
[Kol07, Theorem 105] for the class M of coproducts of open immersions, formalised as
OrderSeqAssignment.globalize in Hironaka/Resolution/Algebraic/Kol07/GlobalizeDescent.lean. This
module supplies its inputs.
BO.localClass n mis the class of local triplesLTof Theorem 105: the members ofBOClass n m(1 ≤ m,dim X ≤ n,max-ord I ≤ m) admitting a global smooth hypersurface of maximal contact (HasMaximalContact). The class of global triplesGTisBOClass n mitself. Kollár states Theorem 103 fordim X = n; the class here hasdim X ≤ n, so the results on hypersurfaces of maximal contact for triples of exact dimension (Hironaka/Resolution/Algebraic/MaximalContact/) are applied at each triple's own dimension.- The class lemmas: stability under open-immersion coproducts, closure under finite disjoint
unions (
closedUnderSigma_hasDimLE: a triple is equidimensional, so every nonempty piece of a disjoint union has the union's relative dimension, at mostn), the local covers (exists_isPullbackOf_localClass), hence hypotheses (2)(i)–(ii) of Theorem 105 asglobalizationData_localClass, and the closure of local covers under fibre products (localCoversFibreClosed_localClass), which the descent uses for the fibre productX' ×_X X'of Kollár's proof. BO.localFunctor n m bdis Step 2's functor on the local class: the value atTis the maximal-contact casemaxContactCasefor a chosen hypersurface of maximal contact (Classical.choose); it does not depend on the choice (localFunctor_seq, bymaxContactCase_indep), and it commutes with smooth surjections bymaxContactCase_pullback_of_surjective, after the chosen hypersurface on the pulled-back triple is exchanged for the pulled-back one, which is hypothesis (3) of Theorem 105.BO.functor n m bdis the unique extension of Theorem 105:OrderSeqAssignment.globalizeon these inputs, a smooth blow-up sequence functor of ordermonBOClass n m. On the local class it ismaxContactCasefor any hypersurface of maximal contact (functor_seq_localClass).
Clauses (1)–(2) of Theorem 103 for BO.functor are proved in
Hironaka/Resolution/Algebraic/OrderReduction/Step3Clauses.lean, and the data BOData n m are
assembled in Hironaka/Resolution/Algebraic/OrderReduction/Step3Data.lean.
The local triples LT_{n,m} of Step 3 of the proof of [Kol07, Theorem 103] (the class
LT of [Kol07, Theorem 105 (2)]): the members of BOClass n m admitting a global smooth
hypersurface of maximal contact (HasMaximalContact).
Equations
- Hironaka.BO.localClass n m T = (AlgebraicGeometry.Triple.BOClass n m T ∧ T.HasMaximalContact m)
Instances For
A smooth morphism from an empty scheme has every relative dimension: the defining condition is a statement about points.
dim X ≤ n is stable under open-immersion coproducts (Triple.HasDim.isPullbackOf at the
triple's own dimension).
max-ord I ≤ m is stable under open-immersion coproducts (maxOrd_comap_le_of_smooth).
The class BOClass n m is stable under open-immersion coproducts.
The local class is stable under open-immersion coproducts ([Kol07, Theorem 105 (2)];
HasMaximalContact.isPullbackOf).
dim X ≤ n is closed under finite disjoint unions (Step 3 of the proof of
[Kol07, Theorem 103]): a triple is equidimensional (Triple.smoothOfRelativeDimension), every
nonempty piece of a disjoint union is an open of it and so has the union's relative dimension d
(HasDim.isPullbackOf), and the relative dimension of a smooth morphism with nonempty source is
unique (SmoothOfRelativeDimension.eq_of_nonempty), so d is the piece's dimension, at most n;
if every piece is empty so is the union, and every relative dimension holds.
The class BOClass n m is closed under finite disjoint unions ([Kol07, Theorem 105 (2)(ii)];
Triple.closedUnderSigma_maxOrd_le for the order).
The local class is closed under finite disjoint unions ([Kol07, Theorem 105 (2)(ii)]; Step 3
of the proof of [Kol07, Theorem 103]: "H^* := ∐ H^(j) ⊂ ∐ X^(j) =: X^* is a smooth hypersurface
of maximal contact"), by Triple.closedUnderSigma_hasMaximalContact.
Every point of a triple of BOClass n m has an open neighbourhood, an open-immersion
coproduct into the triple, carrying a local triple (Step 3 of the proof of [Kol07, Theorem 103],
by [Kol07, Theorem 80 (2)]; Triple.exists_isPullbackOf_maximalContactClass at the triple's own
dimension).
Hypotheses (2)(i)–(ii) of [Kol07, Theorem 105] for M the coproducts of open immersions,
GT = BOClass n m and LT = localClass n m: the instance that Step 3 of the proof of
[Kol07, Theorem 103] feeds to Theorem 105.
The fibre triple of two local covers is in the local class (the triple over X'' = X' ×_X X'
in the proof of [Kol07, Theorem 105] is again a local triple): the projection is a base change of
an open-immersion coproduct (isStableUnderBaseChange_openImmersionCoprods) and the class is
stable along it.
Step 2's functor on the local triples (Step 3 of the proof of [Kol07, Theorem 103]: "by the
previous step BO_{n,m} is defined on (X^*, g^* I, g^{-1} E)"): the value at T is
maxContactCase for a chosen smooth hypersurface of maximal contact (Classical.choose on
HasMaximalContact); the two functor fields are isOrderSeq_maxContactCase and
noEmptyCenters_maxContactCase. The value does not depend on the choice (localFunctor_seq, by
maxContactCase_indep).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The local functor's value is maxContactCase for any smooth hypersurface of maximal contact
([Kol07, 104, Step 2.3], through maxContactCase_indep).
The local functor commutes with smooth surjections (hypothesis (3) of [Kol07, Theorem 105],
from [Kol07, 104, Step 2.3] as maxContactCase_pullback_of_surjective): on the pulled-back triple
the chosen hypersurface is exchanged for the pulled-back one (localFunctor_seq with
isSmoothDivisor_comap_of_smooth and isMaximalContact_comap_of_smooth).
Hypothesis (3) of [Kol07, Theorem 105] for M the coproducts of open immersions
(CommutesWithSmoothSurjections.commutesWithSurjectionsIn).
The order-reduction functor BO_{n,m} (Step 3 of the proof of [Kol07, Theorem 103]: "we
argue as in (37) to prove that BO_{n,m}(X^*, g^* I, g^{-1} E) descends to give
BO_{n,m}(X, I, E)"; [Kol07, Theorem 105]): the unique extension of the local functor to the
class BOClass n m commuting with surjective open-immersion coproducts,
OrderSeqAssignment.globalize on the instances above.
Equations
- Hironaka.BO.functor n m bd = Hironaka.OrderSeqAssignment.globalize ⋯ ⋯ (Hironaka.BO.localFunctor n m bd) ⋯
Instances For
On a triple with a smooth hypersurface of maximal contact H, BO_{n,m} is Step 2's
maxContactCase for H (the extension property of [Kol07, Theorem 105]: the extension agrees with
the functor on the local triples; globalize_seq_of_mem).