The relative dimension of a smooth morphism between reduced equidimensional schemes is constant

For a smooth k-morphism h : Y ⟶ X between reduced schemes whose smooth loci over k have relative dimensions dY and dX (the members of the class IsReducedEquidimensional of the functorial resolution theorem), h is smooth of relative dimension dY - dX (smoothOfRelativeDimension_sub_of_smoothLocus). This is what clause (4a) of the theorem needs: the affine (34.1) (BRAffine_eq_eraseEmpty_pullback_of_smooth) and its descent to the resolution functor (BR_eq_eraseEmpty_pullback_of_smooth) take the relative dimension d of h as an input, and on the class of the theorem it is dY - dX (Hironaka.Resolution.Algebraic.Kol07.Thm36.Theorem36). Kollár's schemes are equidimensional by convention [Kol07, Notation 64], so the relative dimension of a smooth morphism between them is constant when the source is connected; here it is derived.

The argument uses no dimension theory:

• smoothOfRelativeDimension_ι_comp_of_appLE, exists_smoothOfRelativeDimension_ι_comp: a smooth morphism has a relative dimension near every point (Mathlib's Smooth is affine-locally standard smooth, and a submersive presentation has a dimension), lifted to the scheme level on an affine open of the source.
• exists_smoothOfRelativeDimension_of_irreducibleSpace: on an irreducible source the local relative dimensions agree (SmoothOfRelativeDimension.eq_of_nonempty on the nonempty overlaps) and glue (SmoothOfRelativeDimension n is Zariski-local at the source).
• smoothOfRelativeDimension_sub_of_smoothLocus: near every point of Y the relative dimension n of h satisfies n + dX = dY, by eq_of_nonempty on a nonempty open of that neighbourhood lying over both smooth loci: the smooth locus of the reduced Y is dense (dense_smoothLocus_of_perfectField), the smooth h is an open map, and the smooth locus of the reduced X is dense, so some smooth point of the neighbourhood maps to a smooth point of X; source-locality assembles h.

theorem Hironaka.Resolution.smoothOfRelativeDimension_ι_comp_of_appLE {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {V : Y.Opens} (hV : AlgebraicGeometry.IsAffineOpen V) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (n : ℕ) (hn : RingHom.IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e))) : AlgebraicGeometry.SmoothOfRelativeDimension n (CategoryTheory.CategoryStruct.comp V.ι f)

An affine pair U ⊆ X, V ⊆ Y on which f is standard smooth of relative dimension n gives the scheme-level relative dimension of f on the open V: f.resLE U V e has it by HasRingHomProperty.iff_of_isAffine (the global sections of the restriction are f.appLE U V e up to isomorphism, arrowResLEAppIso), and V.ι ≫ f = f.resLE U V e ≫ U.ι adds the relative dimension 0 of the open immersion.

theorem Hironaka.Resolution.exists_smoothOfRelativeDimension_ι_comp {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) [AlgebraicGeometry.Smooth f] (y : ↥Y) : ∃ (V : Y.Opens) (n : ℕ), y ∈ V ∧ AlgebraicGeometry.SmoothOfRelativeDimension n (CategoryTheory.CategoryStruct.comp V.ι f)

A smooth morphism has a relative dimension near every point of the source: Mathlib's Smooth is affine-locally standard smooth (Smooth.exists_isStandardSmooth), and a submersive presentation has a dimension.

theorem Hironaka.Resolution.exists_smoothOfRelativeDimension_of_irreducibleSpace {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) [AlgebraicGeometry.Smooth f] [IrreducibleSpace ↥Y] : ∃ (n : ℕ), AlgebraicGeometry.SmoothOfRelativeDimension n f

A smooth morphism from an IRREDUCIBLE scheme has a global relative dimension: two local relative dimensions agree on the (nonempty) overlap of their opens (SmoothOfRelativeDimension.eq_of_nonempty), and SmoothOfRelativeDimension n is Zariski-local at the source.

theorem Hironaka.Resolution.smoothOfRelativeDimension_sub_of_smoothLocus {k : Type u} [Field k] [CharZero k] (X Y : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] [Y.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (Y ↘ AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsReduced X] [AlgebraicGeometry.IsReduced Y] {dX dY : ℕ} [hdX : AlgebraicGeometry.SmoothOfRelativeDimension dX (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)).ι (X ↘ AlgebraicGeometry.Spec ↧k))] [hdY : AlgebraicGeometry.SmoothOfRelativeDimension dY (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.smoothLocus (Y ↘ AlgebraicGeometry.Spec ↧k)).ι (Y ↘ AlgebraicGeometry.Spec ↧k))] (h : Y ⟶ X) [AlgebraicGeometry.Scheme.Hom.IsOver h (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.Smooth h] : AlgebraicGeometry.SmoothOfRelativeDimension (dY - dX) h

The relative dimension of a smooth morphism between reduced equidimensional schemes is constant: a smooth k-morphism h : Y ⟶ X between reduced schemes whose smooth loci over k have relative dimensions dY and dX is smooth of relative dimension dY - dX. Source-locality over opens U ∋ y on which h has a relative dimension n (exists_smoothOfRelativeDimension_ι_comp); n + dX = dY by eq_of_nonempty on the nonempty open U ∩ Y^ns ∩ h⁻¹(X^ns) of U: U ∩ Y^ns is a nonempty open (Y^ns is dense, dense_smoothLocus_of_perfectField), its image under the open map h (Scheme.Hom.isOpenMap, smooth morphisms being flat and locally of finite presentation) meets the dense X^ns; there the structure morphism of Y factors through Y^ns (relative dimension dY) and through h and X^ns (relative dimension n + dX). No dimension theory enters.