The coproduct of fibre-square charts as an admissible pair #
Kollár reduces the functoriality of the resolution of an affine scheme under a smooth morphism
h : Y → X to the functoriality of the principalization sequence through the charts of
[Kol07, Lemma 41]: near every point of Y there is a fibre square in which Y is a closed
subscheme of a scheme smooth over the ambient of X [Kol07, Theorem 36, proof]. Here the charts
are fibre squares Wᵢ = Y₀ ×_{T.X.left} Bᵢ: jᵢ : Wᵢ ⟶ Bᵢ a closed immersion into an affine Bᵢ
smooth of relative dimension d over the ambient T.X.left of an admissible pair (T, emb₀) of
Y₀, eᵢ : Wᵢ ⟶ Y₀, with IsPullback jᵢ eᵢ qᵢ emb₀. Their coproduct Z := ∐ Wᵢ sits in the
coproduct ambient ∐ Bᵢ, and this file shows that (sigmaTriple T q d, Sigma.map j) is an
admissible pair of Z (AdmissibleEmbedding) carrying the pullback data of T along
Sigma.desc q (Triple.IsPullbackOf): the hypotheses of
BRAffine_eq_eraseEmpty_pullback_of_admissible
(Hironaka.Resolution.Algebraic.Kol07.Thm36.BRAffinePullback) for Z over Y₀.
Sigma.map j : ∐ W ⟶ ∐ B, the coproduct of thejᵢ, with the pullback squaresIsPullback (j i) (Sigma.ι W i) (Sigma.ι B i) (Sigma.map j): coproducts of schemes are disjoint (sigmaι_eq_iff), so the preimage of thei-th summand is thei-th summand and Mathlib's criterionIsOpenImmersion.isPullbackapplies. HenceSigma.map jis a closed immersion (closed immersions are local on the target,IsZariskiLocalAtTarget.iff_of_iSup_eq_topon the summands) and its kernel restricts on each summand toker (j i)(ker_fst_of_isClosedImmersion), so it isI.comap (Sigma.desc q)wheneverker (j i) = I.comap (q i)(eq_of_comap_eq_of_covers).Sigma.descof a family inheritsLocallyOfFiniteType,Flat,SmoothandSmoothOfRelativeDimension d(Zariski-locality on the source,IsZariskiLocalAtSource.sigmaDesc) and surjectivity from a covering family ("X' := ∐ Uᵢ", [Kol07, Proposition 37, proof]).sigmaTriple T q d: the pullback triple ofTalongSigma.desc q(Triple.pullback), the coproduct∐ BoverkthroughSigma.desc q(sigmaOverOfDesc): affine, of finite type, separated, smooth overkof relative dimensiond + nfornthe relative dimension ofT.X.left(smoothOfRelativeDimension_comp). Its ideal isT.I.comap (Sigma.desc q)and its boundaryT.E.comap (Sigma.desc q), empty whenT.Eis.admissibleEmbedding_sigma: the admissibility of(sigmaTriple T q d, Sigma.map j)for∐ W, given the fibre squares and the admissibility of(T, emb₀).
The relative dimension d common to the charts is that of h
(Hironaka.Resolution.Algebraic.Kol07.Thm36.SmoothCharts, where the charts are constructed); the
charts are assembled in Hironaka.Resolution.Algebraic.Kol07.Thm36.AffineFunctoriality.
The coproduct of a family of closed immersions #
Mathlib's Sigma.map j : ∐ W ⟶ ∐ B on points: the summand of j i w.
The preimage of the i-th summand of ∐ B under the coproduct map is the i-th summand of
∐ W: coproducts of schemes are disjoint (sigmaι_eq_iff).
The i-th summand square of the coproduct map is a pullback (Mathlib's criterion
IsOpenImmersion.isPullback on the two summand inclusions).
A coproduct of pullback squares over a common morphism p is a pullback square (schemes are
extensive): checked on the open cover of ∐ B by its summands (Scheme.isPullback_of_openCover),
where the canonical pullback of the summand is W i (isPullback_sigmaMap).
The summands cover the coproduct.
A property local at the target holds for the coproduct of morphisms that have it: on the
summand Sigma.ι B i the coproduct restricts to j i up to the canonical isomorphism
(isPullback_morphismRestrict, IsPullback.isoIsPullback).
A coproduct of closed immersions is a closed immersion: local on the target along the
summands, where it is j i up to the pullback isomorphism.
The kernel of the coproduct of closed immersions restricts on the i-th summand to the kernel
of j i (ker_fst_of_isClosedImmersion on the summand square).
If every ker (j i) is the inverse image of I along q i, the kernel of the coproduct of the
j i is the inverse image of I along Sigma.desc q (ideal sheaves agreeing on the covering
summands agree).
Commuting squares on the summands give a commuting square of the coproducts.
The kernel of the closed immersion of a fibre square over a closed immersion emb₀ is the
inverse image of ker emb₀: j is pullback.fst up to the pullback isomorphism.
Properties of Sigma.desc #
The coproduct map of a covering family is surjective ("X' := ∐ Uᵢ … there is a smooth
surjection g : X' → X", [Kol07, Proposition 37, proof]).
The pull-back triple on a coproduct of charts #
∐ B over k through the coproduct map Sigma.desc q.
Equations
Instances For
The coproduct is smooth over k of relative dimension d + n (condition (1) of Kol07,
Notation 64 for the coproduct triple).
Sigma.desc q is over k for the structure sigmaOverOfDesc.
The pullback triple of T on the coproduct ∐ B of affine schemes smooth of relative dimension
d over T.X.left (Triple.pullback along Sigma.desc q): the triple to which the functoriality
of the principalization sequence [Kol07, 34.1] is applied on the coproduct of the charts.
Equations
Instances For
The coproduct triple carries the pull-back data of T along Sigma.desc q.
The coproduct of fibre-square charts over an admissible pair (T, emb₀) of Y₀ is an
admissible pair of ∐ W over the pullback triple on ∐ B: the closed immersion Sigma.map j,
over k through the squares, into the affine ∐ B with empty boundary, with kernel the inverse
image of T.I = ker emb₀ along Sigma.desc q.