The hypotheses of Theorem 105: classes of morphisms, global and local triples #
Kollár's globalization theorem [Kol07, Theorem 105] assumes (1) a class M of smooth morphisms
closed under fibre products and coproducts, (2) two classes of triples, the global triples GT
and the local triples LT, such that every point of a global triple has an M-neighbourhood
that is a local triple and LT is closed under disjoint unions, and (3) a blow-up sequence
functor on LT commuting with the surjections in M. The definitions (IsGlobalizationClass,
openImmersionCoprods, Triple.GlobalizationData, CommutesWithSurjectionsIn) are in
Hironaka/Scheme/BlowUpSequence/FunctorVocabulary.lean; this module proves the elementary facts
about them and exhibits Kollár's three examples of classes M.
The three examples #
Kollár's parenthetical "for instance, M could be all smooth morphisms, all étale morphisms or
all open immersions" in [Kol07, Theorem 105] asks, for each class, for three facts: its members
are smooth, it is stable under base change, and the morphism ∐ᵢ Uᵢ → X induced by members
Uᵢ → X is a member.
For smooth and for étale morphisms the first two are Mathlib's (Etale → Smooth,
smooth_isStableUnderBaseChange, etale_isStableUnderBaseChange) and the third is locality on the
source (IsZariskiLocalAtSource.sigmaDesc: both properties are HasRingHomProperty classes).
The third class needs care. The open immersions themselves are not closed under coproducts
(not_isGlobalizationClass_isOpenImmersion): for a nonempty scheme X, the morphism
X ⊔ X → X induced by two copies of the identity identifies the two copies of a point, so it is
not a monomorphism, and open immersions are monomorphisms. What Kollár uses (his g : X' → X
and the projections τ₁, τ₂ of X' ×_X X' in the proof of Theorem 105; the "coproduct of the
injections" of [Kol07, 104, Step 3]) is the class of coproducts of open immersions,
openImmersionCoprods: f : Y ⟶ X such that Y is a coproduct of schemes Uᵢ, along a colimit
cofan ιᵢ : Uᵢ ⟶ Y, with every ιᵢ ≫ f an open immersion.
The single tool for this class is Mathlib's characterization of colimit cofans of schemes: a cofan
ι on Y is a colimit iff the induced Sigma.desc ι : ∐ᵢ Uᵢ ⟶ Y is an isomorphism
(Cofan.nonempty_isColimit_iff_isIso_sigmaDesc), together with the point-set description of ∐ᵢ Uᵢ
(sigmaMk, sigmaι_eq_iff) and the converse criterion nonempty_isColimit_cofanMk_of (a family of
open immersions with disjoint images covering Y is a colimit cofan). From the first we read off
that the injections ιᵢ of a colimit cofan are open immersions, jointly surjective and pairwise
disjoint on points (isOpenImmersion_of_isColimit_cofan, exists_eq_of_isColimit_cofan,
ne_of_isColimit_cofan); the second, in its point-set form
(nonempty_isColimit_cofanMk_of_range), builds the new cofans.
- Étaleness (
openImmersionCoprods_etale):f = (Sigma.desc ι)⁻¹ ≫ Sigma.desc (ιᵢ ≫ f), and the second factor is étale by locality on the source, its pieces being open immersions. - Base change (
isStableUnderBaseChange_openImmersionCoprods): for the pullbackP = X ×_S Yofg : Y → Salongf : X → S, the schemesWᵢ := P ×_Y Uᵢwith their first projectionsWᵢ → Pform a cofan of open immersions (base changes ofιᵢ), coveringP(a point ofPoverιᵢ(x)lifts toWᵢ,Scheme.Pullback.exists_preimage_pullback) and pairwise disjoint (their images map to the disjoint images of theιᵢ), hence a colimit cofan; andWᵢ → P → Xis the base change of the open immersionιᵢ ≫ g : Uᵢ → Salongf(the two squares paste,IsPullback.paste_horiz). Mathlib'sIsStableUnderBaseChange.mk'reduces the general pullback square to this canonical one, givenRespectsIso(respectsIso_openImmersionCoprods: transport the cofan along the isomorphism). - Coproducts (
sigmaDesc_openImmersionCoprods): if eachgᵢ : Uᵢ → Xis a coproduct of open immersions alongκᵢⱼ : Vᵢⱼ → Uᵢ, then∐ᵢ Uᵢis the coproduct of theVᵢⱼalongκᵢⱼ ≫ Sigma.ι Uᵢ(index typeΣ i, τᵢ), and(κᵢⱼ ≫ Sigma.ι Uᵢ) ≫ Sigma.desc g = κᵢⱼ ≫ gᵢ.
The data and the functor hypothesis #
Triple.GlobalizationData M GT LT is monotone in M and antitone in GT (its clause (i)
quantifies over GT and asks for a member of M). CommutesWithSurjectionsIn B M is antitone
in M; for M = all smooth morphisms it is CommutesWithSmoothSurjections (the instance binder
[Smooth h] against the hypothesis @Smooth _ _ h), and a functor commuting with all smooth
surjections commutes with the surjections in every class of Theorem 105, whose members are
smooth.
Colimit cofans of schemes, read on points #
A colimit cofan of schemes is the canonical coproduct up to the isomorphism Sigma.desc ι
(Mathlib's Cofan.nonempty_isColimit_iff_isIso_sigmaDesc).
The injections of a colimit cofan of schemes are open immersions.
The injections of a colimit cofan of schemes are jointly surjective.
The injections of a colimit cofan of schemes have pairwise disjoint images.
Mathlib's nonempty_isColimit_cofanMk_of on points: a family of open immersions into S
that covers S and has pairwise disjoint images is a colimit cofan.
Kollár's three examples of classes #
The first example of a class in [Kol07, Theorem 105 (1)]: all smooth morphisms.
The second example of a class in [Kol07, Theorem 105 (1)]: all étale morphisms.
An open immersion is a coproduct of open immersions with one summand.
The morphism ∐ᵢ Uᵢ → X induced by open immersions Uᵢ → X (the "coproduct of the
injections" of [Kol07, 104, Step 3]) is a coproduct of open immersions.
A coproduct of open immersions is étale.
Coproducts of open immersions respect isomorphisms: transport the cofan.
Coproducts of open immersions are stable under base change: the pullback of Y = ∐ᵢ Uᵢ → S
along f : X → S is covered by the disjoint open subschemes P ×_Y Uᵢ, each mapping to X by
the base change of the open immersion Uᵢ → S.
Coproducts of open immersions are closed under coproducts: a coproduct of coproducts is a coproduct, indexed by the sigma type.
The third example of a class in [Kol07, Theorem 105 (1)], read as the proof uses it: the coproducts of open immersions.
For a nonempty scheme X, the morphism X ⊔ X → X induced by two copies of the identity is
not an open immersion: it identifies the two copies of a point, so it is not a monomorphism.
The open immersions are not closed under coproducts, so they are not, as they stand, a class
of [Kol07, Theorem 105]; the class the proof uses is openImmersionCoprods.
A class of Theorem 105 respects isomorphisms (Mathlib: base-change stability gives
RespectsIso).
The data (2) of [Kol07, Theorem 105] is monotone in the class M.
The data (2) of [Kol07, Theorem 105] restricts to a smaller class of global triples.
The hypothesis (3) of [Kol07, Theorem 105] with M = all smooth morphisms is the first
bullet of [Kol07, 34.1], commutation with smooth surjections.
Commuting with the surjections in M is antitone in M.
A functor commuting with smooth surjections commutes with the surjections in every class of Theorem 105.
The unfolding of CommutesWithSurjectionsIn.
The hypothesis (3) of [Kol07, Theorem 105] with M = all smooth morphisms, for marked
functors: commutation with smooth surjections.
Commuting with the surjections in M is antitone in M (marked functors).
A marked functor commuting with smooth surjections commutes with the surjections in every class of Theorem 105.
The unfolding of CommutesWithSurjectionsIn for marked functors.