Functoriality of the affine resolution under smooth morphisms of a given relative dimension

Clause (4) of [Kol07, Theorem 36], commutation with smooth morphisms [Kol07, 34.1], for the affine resolution BRAffine (Hironaka.Resolution.Algebraic.Kol07.Thm36.BR) of affine reduced equidimensional schemes (IsReducedEquidimensional): for a smooth h : Y ⟶ X of relative dimension d between such schemes, with admissible pairs of X and of Y given, BRAffine k Y = ((BRAffine k X).pullback h).eraseEmpty. The relative dimension and the admissible pairs are inputs here; they are supplied by Hironaka.Resolution.Algebraic.Kol07.Thm36.RelativeDimensionConstancy and Hironaka.Resolution.Algebraic.Kol07.Thm36.AdmissiblePairs when the clause is derived for the resolution functor (Hironaka.Resolution.Algebraic.Kol07.Thm36.BRDescent).

The argument

Kollár reduces (34.1) for BR to (34.1) for the principalization sequence through the charts of [Kol07, Lemma 41] and the locality of (34.1) [Kol07, Theorem 36, proof]. Fix admissible pairs (TX, embX) of X and (TY, embY) of Y and finitely many charts cᵢ : Chart h embX embY d (Hironaka.Resolution.Algebraic.Kol07.Thm36.SmoothCharts) whose opens Wᵢ cover Y. Let Z := ∐ Wᵢ, an affine reduced equidimensional scheme (a disjoint union of open subschemes of the member Y, IsReducedEquidimensional.sigma), over k through e := Sigma.desc eᵢ : Z ⟶ Y, a surjective flat (étale) morphism.

• Over Y. The squares of the charts over AY glue (admissibleEmbedding_sigma) to an admissible pair of Z in the triple ∐ D(Gᵢ) over TY, with Sigma.desc (D(Gᵢ)).ι smooth of relative dimension 0 and TY.IsPullbackOf; BRAffine_eq_eraseEmpty_pullback_of_admissible (Hironaka.Resolution.Algebraic.Kol07.Thm36.BRAffinePullback) gives BRAffine k Z = ((BRAffine k Y).pullback e).eraseEmpty, and since e is flat and surjective the deletion of empty blow-ups is trivial (eraseEmpty_pullback_of_flat_surjective, eraseEmpty_BRAffine): BRAffine k Z = (BRAffine k Y).pullback e.
• Over X. The squares over AX glue to an admissible pair of Z in the triple ∐ Bᵢ over TX, with Sigma.desc qᵢ smooth of relative dimension d; the same lemma along e ≫ h gives BRAffine k Z = (((BRAffine k X).pullback h).pullback e).eraseEmpty, which by the same flat surjective e is ((BRAffine k X).pullback h).eraseEmpty.pullback e.
• Descent. Both sides of the identity pull back to the same sequence on Z, hence agree on each Wᵢ; a blow-up sequence is determined by its pullbacks to an open cover (eq_of_pullback_of_covers).

BRAffine_eq_eraseEmpty_pullback_of_smooth supplies the charts: exists_chart_mem at every point of Y and a finite subcover (Y is quasi-compact over k); the empty Y is the degenerate case nil = nil (eraseEmpty_eq_nil_of_isEmpty).

theorem Hironaka.Resolution.BRAffine_eq_eraseEmpty_pullback_of_charts {k : Type u} [Field k] [CharZero k] {ι : Type u} [Finite ι] [Nonempty ι] (X Y : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.QuasiCompact (X ↘ AlgebraicGeometry.Spec ↧k)] [Y.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (Y ↘ AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.QuasiCompact (Y ↘ AlgebraicGeometry.Spec ↧k)] (hX : AlgebraicGeometry.Scheme.IsReducedEquidimensional k X) (hY : AlgebraicGeometry.Scheme.IsReducedEquidimensional k Y) (h : Y ⟶ X) [AlgebraicGeometry.Scheme.Hom.IsOver h (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.Smooth h] (d : ℕ) (TX : AlgebraicGeometry.Triple k) (embX : X ⟶ TX.X.left) (hadmX : AdmissibleEmbedding k X TX embX) (TY : AlgebraicGeometry.Triple k) (embY : Y ⟶ TY.X.left) (hadmY : AdmissibleEmbedding k Y TY embY) (c : ι → Chart h embX embY d) (hcov : ∀ (y : ↥Y), ∃ (i : ι) (w : ↥(c i).W), (c i).e w = y) : BRAffine k Y = ((BRAffine k X).pullback h).eraseEmpty

Commutation of BRAffine with a smooth h of relative dimension d, from a finite family of charts covering Y [Kol07, Theorem 36, proof; 34.1]: Z := ∐ (c i).W carries two admissible pairs (admissibleEmbedding_sigma over Y and over X), BRAffine_eq_eraseEmpty_pullback_of_admissible computes BRAffine Z from both, the surjective Sigma.desc e turns the deletion of empty blow-ups into an equality on the nose, and eq_of_pullback_of_covers descends to Y.

theorem Hironaka.Resolution.BRAffine_eq_eraseEmpty_pullback_of_smooth {k : Type u} [Field k] [CharZero k] (X Y : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.QuasiCompact (X ↘ AlgebraicGeometry.Spec ↧k)] [Y.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (Y ↘ AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.QuasiCompact (Y ↘ AlgebraicGeometry.Spec ↧k)] (hX : AlgebraicGeometry.Scheme.IsReducedEquidimensional k X) (hY : AlgebraicGeometry.Scheme.IsReducedEquidimensional k Y) (h : Y ⟶ X) [AlgebraicGeometry.Scheme.Hom.IsOver h (AlgebraicGeometry.Spec ↧k)] (d : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension d h] (TX : AlgebraicGeometry.Triple k) (embX : X ⟶ TX.X.left) (hadmX : AdmissibleEmbedding k X TX embX) (TY : AlgebraicGeometry.Triple k) (embY : Y ⟶ TY.X.left) (hadmY : AdmissibleEmbedding k Y TY embY) : BRAffine k Y = ((BRAffine k X).pullback h).eraseEmpty

Commutation of BRAffine with a smooth h of relative dimension d between affine reduced equidimensional schemes, given admissible pairs of both [Kol07, Theorem 36, proof; 34.1]: the charts of exists_chart_mem at every point, a finite subcover, and BRAffine_eq_eraseEmpty_pullback_of_charts.