Smoothness of relative dimension m is fpqc local on the base

Smoothness of relative dimension m descends along surjective, flat, quasi-compact morphisms of schemes. For smoothness itself this is [TSPA, Tag 02VL] ("the property f is smooth is fpqc local on the base"); the relative dimension is the addition made here. Mathlib descends Smooth through HasRingHomProperty.descendsAlong_flat, whose input is the codescent of the ring-hom property along faithfully flat ring maps (RingHom.Smooth.codescendsAlong_faithfullyFlat); the same route gives the relative dimension once the ring-level codescent is proved, which is the content of this file.

Why it holds. Let R → S be faithfully flat and R → T a ring map whose base change S → S ⊗_R T is locally standard smooth of relative dimension n. Then S → S ⊗_R T is smooth, so R → T is smooth (Mathlib's descent of smoothness), hence T is covered by basic opens T[1/t] standard smooth over R, with Ω[T[1/t]⁄R] free of some rank d. Base change to B = S ⊗_R T[1/t] = (S ⊗_R T)[1/(1 ⊗ t)]: Ω[B⁄S] = B ⊗ Ω[T[1/t]⁄R] is free of rank d (Kähler differentials commute with base change), B is nontrivial when T[1/t] is (faithful flatness), and S → B is locally standard smooth of relative dimension n (localization of the hypothesis), so on some nontrivial basic open B[1/v] the differentials are free of rank n while also being the localization of Ω[B⁄S], free of rank d; hence d = n and T[1/t] is standard smooth of relative dimension n (Mathlib's characterization by the rank of the differentials for a standard smooth algebra). Discarding the nilpotent t (which generate no part of the unit ideal) gives the cover witnessing Locally (IsStandardSmoothOfRelativeDimension n) for R → T.

Main declarations

• AlgebraicGeometry.rank_kaehlerDifferential_eq_of_locally: a nontrivial algebra with free Kähler differentials that is locally standard smooth of relative dimension n has differentials of rank n.
• AlgebraicGeometry.codescendsAlong_locally_isStandardSmoothOfRelativeDimension: the ring-level codescent along faithfully flat maps.
• AlgebraicGeometry.descendsAlong_smoothOfRelativeDimension: the scheme statement, used to descend the relative dimension of a smooth morphism along an fpqc cover (Hironaka/Scheme/Smooth/ExceptionalDivisorSmooth.lean).

theorem AlgebraicGeometry.rank_kaehlerDifferential_localizationAway (S : Type u) [CommRing S] {B : Type u} [CommRing B] [Algebra S B] [Nontrivial B] [Module.Free B Ω[B⁄S]] (t : B) [Nontrivial (Localization.Away t)] : Module.rank (Localization.Away t) Ω[Localization.Away t⁄S] = Module.rank B Ω[B⁄S]

The Kähler differentials of B[1/t] over S are the base change of those of B; when the latter are free, the rank is unchanged.

theorem AlgebraicGeometry.exists_not_isNilpotent_of_span_eq_top {B : Type u} [CommRing B] [Nontrivial B] {s : Set B} (hs : Ideal.span s = ⊤) : ∃ t ∈ s, ¬IsNilpotent t

A generating set of the unit ideal of a nontrivial ring contains a non-nilpotent element.

theorem AlgebraicGeometry.nontrivial_localizationAway_of_not_isNilpotent {B : Type u} [CommRing B] {t : B} (ht : ¬IsNilpotent t) : Nontrivial (Localization.Away t)

B[1/t] is nontrivial when t is not nilpotent.

theorem AlgebraicGeometry.rank_kaehlerDifferential_eq_of_locally (S : Type u) [CommRing S] {B : Type u} [CommRing B] [Algebra S B] [Nontrivial B] [Module.Free B Ω[B⁄S]] (n : ℕ) (h : RingHom.Locally (fun {R S : Type u} [CommRing R] [CommRing S] => RingHom.IsStandardSmoothOfRelativeDimension n) (algebraMap S B)) : Module.rank B Ω[B⁄S] = ↑n

If S → B is locally standard smooth of relative dimension n, B is nontrivial and Ω[B⁄S] is free, then Ω[B⁄S] has rank n: on a nontrivial basic open B[1/t] of the cover the differentials are free of rank n (Mathlib's rank_kaehlerDifferential) and are the base change of Ω[B⁄S].

theorem AlgebraicGeometry.locally_tensorProduct_localizationAway {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (n : ℕ) (h : RingHom.Locally (fun {R S : Type u} [CommRing R] [CommRing S] => RingHom.IsStandardSmoothOfRelativeDimension n) (algebraMap S (TensorProduct R S T))) (t : T) : RingHom.Locally (fun {R S : Type u} [CommRing R] [CommRing S] => RingHom.IsStandardSmoothOfRelativeDimension n) (algebraMap S (TensorProduct R S (Localization.Away t)))

S ⊗[R] T[1/t] is the localization of S ⊗[R] T at 1 ⊗ t, so a property that holds locally for S → S ⊗[R] T holds locally for S → S ⊗[R] T[1/t].

theorem AlgebraicGeometry.codescendsAlong_locally_isStandardSmoothOfRelativeDimension (n : ℕ) : RingHom.CodescendsAlong (fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.Locally fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.IsStandardSmoothOfRelativeDimension n) fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.FaithfullyFlat

Being locally standard smooth of relative dimension n codescends along faithfully flat ring maps: the ring-level form of the descent ([TSPA, Tag 02VL] for smoothness alone, Mathlib's RingHom.Smooth.codescendsAlong_faithfullyFlat).

theorem AlgebraicGeometry.descendsAlong_smoothOfRelativeDimension (m : ℕ) : CategoryTheory.MorphismProperty.DescendsAlong (@SmoothOfRelativeDimension m) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Smoothness of relative dimension m descends along surjective, flat, quasi-compact morphisms: it is fpqc local on the base ([TSPA, Tag 02VL] for smoothness alone). Mathlib's descendsAlong_flat applied to the ring-level codescent above.