The descent of the resolution functor and its functoriality under smooth morphisms #
The descent of [Kol07, Proposition 37] for the resolution functor BR
(Hironaka.Resolution.Algebraic.Kol07.Thm36.BR), and clause (4a) of the functorial resolution
theorem, commutation with smooth morphisms [Kol07, 34.1], with the relative dimension d of the
smooth morphism taken as an input (it is supplied by
Hironaka.Resolution.Algebraic.Kol07.Thm36.RelativeDimensionConstancy on the class of the theorem).
The condition (37.1) and the descent #
For a member X of the class IsReducedEquidimensional k X (quasi-compact, separated over k),
the finite affine cover ∐ Uᵢ → X (Hironaka.Scheme.BlowUpSequence.AffineCover) has affine
members of the class as source X' = ∐ Uᵢ and kernel pair X'' = X' ×_X X'
(Hironaka.Resolution.Algebraic.Kol07.Thm36.ClassClosure), and the two projections τ₁, τ₂ : X'' → X' are smooth surjective of relative dimension 0. The affine (34.1) with d = 0
(Hironaka.Resolution.Algebraic.Kol07.Thm36.AffineFunctoriality, the admissible pairs from
Hironaka.Resolution.Algebraic.Kol07.Thm36.AdmissiblePairs) gives (37.1): BRAffine X'' = τᵢ^* BRAffine X' on the nose, which is the kernel-pair condition of the descent
(exists_pullback_eq_of_kernelPair). Hence BRDescends k X holds on every member of the class, BR X is the (deleted) descended sequence, and g^* BR X = BRAffine X'
(BR_pullback_affineCoverDesc). On an affine member the same (34.1) for g itself gives BRAffine X' = g^* BRAffine X, so the descent returns BRAffine X and BR X = BRAffine X
(BR_eq_BRAffine_of_isAffine); on an integral affine X, a member
(isReducedEquidimensional_of_isIntegral), BR X is the embedding-free affine resolution with its
empty steps deleted (BR_eq_BR_affine'_of_integral).
Clause (4a) with the relative dimension as input #
For a smooth q : Z → Y of relative dimension d from an affine member Z to a member Y, cover
Y by its finite affine cover Uᵢ and Z by the preimages q⁻¹Uᵢ (affine, since q is an affine
morphism: Z affine, Y separated). The coproduct ∐ q⁻¹Uᵢ → ∐ Uᵢ is smooth of relative dimension
d between affine members (sigmaMap_of_isZariskiLocalAtTarget), so the affine (34.1) computes
BRAffine (∐ q⁻¹Uᵢ) from BRAffine (∐ Uᵢ) = g^* BR Y; the étale surjection ∐ q⁻¹Uᵢ → Z computes
it from BRAffine Z; comparing and cancelling the flat surjection gives
BRAffine Z = (q^* BR Y).eraseEmpty (BRAffine_eq_eraseEmpty_BR_pullback_of_smooth). For a smooth
h : Y → X of relative dimension d between members, apply this to ∐ Uᵢ → Y → X and cancel
∐ Uᵢ → Y: BR Y = (h^* BR X).eraseEmpty (BR_eq_eraseEmpty_pullback_of_smooth), and on the nose
when h is surjective (BR_eq_pullback_of_smooth_surjective).
The surjective form of (34.1) for affine members [Kol07, Theorem 36, proof]: a smooth surjective
morphism of relative dimension d between affine members of the class pulls BRAffine back on the
nose, by BRAffine_eq_eraseEmpty_pullback_of_smooth with the admissible pairs of
exists_admissibleEmbedding, the deletion of empty steps being trivial along a flat surjection
(eraseEmpty_pullback_of_flat_surjective).
τ₂ is smooth of relative dimension 0 (the base change of g; the counterpart of
AlgebraicGeometry.smoothOfRelativeDimension_zero_affineCoverFst).
The condition (37.1) of [Kol07, Proposition 37]: both projections of the kernel pair
X'' = X' ×_X X' are smooth surjective of relative dimension 0 between affine members of the
class, so the affine (34.1) on the nose (BRAffine_eq_pullback_of_smooth_surjective) gives both
equalities BRAffine X'' = τᵢ^* BRAffine X'.
The cover descent BRDescends holds on every member of the class [Kol07, Proposition 37]:
(37.1) is the kernel-pair condition of exists_pullback_eq_of_kernelPair.
The defining property of BR on every member of the class: its pullback along the finite
affine cover is the affine value on the cover scheme [Kol07, Proposition 37, proof].
On an affine member of the class the resolution functor is the affine resolution:
BRAffine (∐ Uᵢ) = g^* BRAffine X by the affine (34.1) for the étale surjection g, so the cover
descent returns BRAffine X itself (the uniqueness BR_eq_eraseEmpty_of_pullback_eq; the deletion
of empty steps is idempotent).
On an integral affine X, a member of the class (isReducedEquidimensional_of_isIntegral),
the resolution functor is the embedding-free affine resolution BR_affine' k X
(Hironaka.Resolution.Algebraic.Kol07.Thm36.Independence) with its globally empty steps deleted:
BR X = BRAffine X (the cover descent), and BRAffine is that deletion by definition.
The preimage in Z of the i-th member of the finite affine cover of Y, as a scheme.
Equations
Instances For
The open immersion of the i-th preimage into Z.
Equations
Instances For
The restriction of q to the i-th preimage, landing in the i-th member of the cover.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The i-th preimage is the fibre product of Z and the i-th member of the cover over Y.
The affine (34.1) read on the target's resolution functor: for an affine member Z of the class
and a smooth q : Z ⟶ Y of relative dimension d to a member Y,
BRAffine Z = (q^* BR Y).eraseEmpty, through the coproduct of the preimages of the finite affine
cover of Y, the affine (34.1) for ∐ q⁻¹Uᵢ → ∐ Uᵢ, and the cover descent of Y.
Clause (4a) of the functorial resolution theorem with the relative dimension as INPUT Kol07,
Theorem 36 (4); 34.1: for a smooth h : Y ⟶ X of relative dimension d between members of the
class, BR Y = (h^* BR X).eraseEmpty, by the affine (34.1) for ∐ Uᵢ → Y → X read on BR X, the
cover descent of Y, and the injectivity of the pullback along the flat surjection ∐ Uᵢ → Y. On
the class of the theorem the relative dimension is supplied by
Hironaka.Resolution.Algebraic.Kol07.Thm36.RelativeDimensionConstancy.
The first part of clause (4a), with the relative dimension as input: along a smooth surjective
h the pullback is exact (eraseEmpty_BR).