Smooth divisors are smooth of relative dimension n − 1

The converse of isSmoothDivisor_of_smoothOfRelativeDimension (Hironaka.Scheme.Snc.SmoothDivisor): a smooth divisor D of X, smooth of relative dimension n over the perfect field k, is smooth of relative dimension n − 1 over k — for every n, with n − 1 the truncated difference (at n = 0 the stalks are fields and a smooth divisor is empty). The closed subscheme V(D) is regular, hence smooth over k (Hironaka.Algebra.RegularSmooth.RegularSmoothEquiv); its relative dimension is read off at one point of each affine chart: for a standard smooth k-algebra S the module Ω[S⁄k] is free, so its rank is dim_κ κ(𝔮) ⊗ Ω[S⁄k] at any prime 𝔮, which is dim S_𝔮 + trdeg_k κ(𝔮) (the dimension count of Hironaka.Algebra.RegularSmooth.Dimension), and Mathlib's IsStandardSmoothOfRelativeDimension.iff_of_isStandardSmooth turns the rank into the relative dimension. At a point z of V(D) over x ∈ X the local ring is 𝒪_{X,x}/(a) with a ∈ 𝔪_x ∖ 𝔪_x², of dimension dim 𝒪_{X,x} − 1, with the residue field of x, and dim 𝒪_{X,x} + trdeg_k κ(x) = n (ringKrullDim_stalk_add_trdeg_residueField_of_smoothOfRelativeDimension). Together the two directions are the equivalence "D is a smooth divisor iff V(D) is smooth of relative dimension n − 1", which the passage to a hypersurface of maximal contact (Hironaka.Resolution.Algebraic.MaximalContact.GoingDown) and the dimension bookkeeping of Hironaka.Stage use.

theorem AlgebraicGeometry.isStandardSmoothOfRelativeDimension_of_ringKrullDim_add_trdeg {k : Type u} [Field k] {S : Type u} [CommRing S] [Algebra k S] [PerfectField k] [Algebra.IsStandardSmooth k S] [Nontrivial S] (𝔮 : Ideal S) [𝔮.IsPrime] (m : ℕ) (h : ringKrullDim (Localization.AtPrime 𝔮) + ↑(Cardinal.toENat (Algebra.trdeg k 𝔮.ResidueField)) = ↑m) : Algebra.IsStandardSmoothOfRelativeDimension m k S

A standard smooth algebra over a perfect field whose local ring at a prime 𝔮 satisfies dim S_𝔮 + trdeg_k κ(𝔮) = m is standard smooth of relative dimension m: Ω[S⁄k] is free of rank dim_κ κ(𝔮) ⊗ Ω[S⁄k] = dim_κ 𝔪/𝔪² + dim_κ Ω[κ(𝔮)⁄k], which is dim S_𝔮 + trdeg since S_𝔮 is regular (the dimension count of Hironaka.Algebra.RegularSmooth.Dimension).

theorem AlgebraicGeometry.smoothOfRelativeDimension_of_forall_exists_affineOpen {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (m : ℕ) (h : ∀ (x : ↥X), ∃ (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V), Algebra.IsStandardSmoothOfRelativeDimension m k ↑(X.presheaf.obj (Opposite.op V))) : SmoothOfRelativeDimension m f

The converse of Scheme.Hom.exists_affineOpen_isStandardSmoothOfRelativeDimension: a morphism to Spec k such that every point has an affine neighbourhood V with Γ(X, V) standard smooth of relative dimension m over k (the k-algebra structure through f) is smooth of relative dimension m.

theorem AlgebraicGeometry.exists_affineOpen_isStandardSmooth {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [Smooth f] (x : ↥X) : ∃ (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V), Algebra.IsStandardSmooth k ↑(X.presheaf.obj (Opposite.op V))

A scheme smooth over k is covered by affine opens whose section rings are standard smooth k-algebras (through f); the Smooth analogue of exists_affineOpen_isStandardSmoothOfRelativeDimension.

theorem AlgebraicGeometry.natCast_add_eq_natCast_sub_one {p r n : ℕ} {t : ℕ∞} (hX : ↑r + ↑t = ↑n) (hpr : p + 1 = r) : ↑p + ↑t = ↑(n - 1)

Cancellation in WithBot ℕ∞: from r + t = n with r, n finite and p + 1 = r, p + t = n − 1.

theorem AlgebraicGeometry.smoothOfRelativeDimension_of_isSmoothDivisor {k : Type u} [Field k] {X : Scheme} [PerfectField k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (D : X.IdealSheafData) (hD : IsSmoothDivisor D) : SmoothOfRelativeDimension (n - 1) (CategoryTheory.CategoryStruct.comp D.subschemeι f)

A smooth divisor of X, smooth of relative dimension n over the perfect field k, is smooth of relative dimension n − 1 over k (for every n, n − 1 truncated): the converse of isSmoothDivisor_of_smoothOfRelativeDimension.