chore(RingTheory): redefine FormallySmooth in terms of Ω[S⁄R] and H¹(L_{S/R}) (#30876)

Previously `FormallySmooth` was defined in terms of an infinitesimal lifting criterion, which involved quantifying over all algebras in an universe. We also showed that this is equivalent to `Ω[S⁄R]` being projective and `H¹(L_{S/R}) = 0`. We change the definition to switch to the latter so that we do not need to quantify over types. As a plus we can generalize the universes of `FormallySmooth` and by extension `Smooth`, `Etale` etc.

Author: erdOne

Mathlib/LinearAlgebra/Quotient/Defs.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov
 import Mathlib.Algebra.Module.Equiv.Defs
 import Mathlib.Algebra.Module.Submodule.Defs
 import Mathlib.GroupTheory.QuotientGroup.Defs
+import Mathlib.Logic.Small.Basic
 
 /-!
 # Quotients by submodules
@@ -197,6 +198,11 @@ theorem mk_surjective : Function.Surjective (@mk _ _ _ _ _ p) := by
   rintro ⟨x⟩
   exact ⟨x, rfl⟩
 
+universe u in
+instance {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] {N : Submodule R M} [Small.{u} M] :
+    Small.{u} (M ⧸ N) :=
+  small_of_surjective (Submodule.Quotient.mk_surjective _)
+
 end Quotient
 
 section

Mathlib/LinearAlgebra/TensorProduct/Basic.lean

@@ -3,11 +3,11 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Mario Carneiro
 -/
-import Mathlib.Algebra.Module.Submodule.Bilinear
 import Mathlib.Algebra.Module.Equiv.Basic
+import Mathlib.Algebra.Module.Shrink
+import Mathlib.Algebra.Module.Submodule.Bilinear
 import Mathlib.GroupTheory.Congruence.Hom
 import Mathlib.Tactic.Abel
-import Mathlib.Tactic.SuppressCompilation
 
 /-!
 # Tensor product of modules over commutative semirings.
@@ -1010,6 +1010,12 @@ lemma map_bijective {f : M →ₗ[R] N} {g : P →ₗ[R] Q}
     Function.Bijective (map f g) :=
   (TensorProduct.congr (.ofBijective f hf) (.ofBijective g hg)).bijective
 
+universe u in
+instance {R M N : Type*} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N]
+    [Module R M] [Module R N] [Small.{u} M] [Small.{u} N] : Small.{u} (M ⊗[R] N) :=
+  ⟨_, ⟨(TensorProduct.congr
+    (Shrink.linearEquiv R M) (Shrink.linearEquiv R N)).symm.toEquiv⟩⟩
+
 end TensorProduct
 
 open scoped TensorProduct

Mathlib/RingTheory/Etale/Basic.lean

@@ -11,10 +11,11 @@ import Mathlib.RingTheory.Unramified.Basic
 
 # Étale morphisms
 
-An `R`-algebra `A` is formally étale if for every `R`-algebra `B`,
+An `R`-algebra `A` is formally etale if `Ω[A⁄R]` and `H¹(L_{A/R})` both vanish.
+This is equivalent to the standard definition that "for every `R`-algebra `B`,
 every square-zero ideal `I : Ideal B` and `f : A →ₐ[R] B ⧸ I`, there exists
-exactly one lift `A →ₐ[R] B`.
-It is étale if it is formally étale and of finite presentation.
+exactly one lift `A →ₐ[R] B`".
+An `R`-algebra `A` is étale if it is formally étale and of finite presentation.
 
 We show that the property extends onto nilpotent ideals, and that these properties are stable
 under `R`-algebra homomorphisms and compositions.
@@ -26,58 +27,78 @@ localization at an element.
 
 open scoped TensorProduct
 
-universe u
+universe u v
 
 namespace Algebra
 
-section
+variable {R : Type u} {A : Type v} {B : Type*} [CommRing R] [CommRing A] [Algebra R A]
+  [CommRing B] [Algebra R B]
 
-variable (R : Type u) [CommRing R]
-variable (A : Type u) [CommRing A] [Algebra R A]
+section
 
-/-- An `R` algebra `A` is formally étale if for every `R`-algebra, every square-zero ideal
-`I : Ideal B` and `f : A →ₐ[R] B ⧸ I`, there exists exactly one lift `A →ₐ[R] B`. -/
+variable (R A) in
+/-- An `R`-algebra `A` is formally etale if both `Ω[A⁄R]` and `H¹(L_{A/R})` are zero.
+For the infinitesimal lifting definition, see `FormallyEtale.iff_comp_bijective`. -/
 @[mk_iff, stacks 00UQ]
 class FormallyEtale : Prop where
-  comp_bijective :
-    ∀ ⦃B : Type u⦄ [CommRing B],
-      ∀ [Algebra R B] (I : Ideal B) (_ : I ^ 2 = ⊥),
-        Function.Bijective ((Ideal.Quotient.mkₐ R I).comp : (A →ₐ[R] B) → A →ₐ[R] B ⧸ I)
+  subsingleton_kaehlerDifferential : Subsingleton Ω[A⁄R]
+  subsingleton_h1Cotangent : Subsingleton (H1Cotangent R A)
+
+attribute [instance]
+  FormallyEtale.subsingleton_kaehlerDifferential FormallyEtale.subsingleton_h1Cotangent
 
 end
 
 namespace FormallyEtale
 
 section
 
-variable {R : Type u} [CommRing R]
-variable {A : Type u} [CommRing A] [Algebra R A]
+instance (priority := 100) [FormallyEtale R A] :
+    FormallyUnramified R A := ⟨inferInstance⟩
+
+instance (priority := 100) [FormallyEtale R A] : FormallySmooth R A :=
+  ⟨inferInstance, inferInstance⟩
 
-theorem iff_unramified_and_smooth :
-    FormallyEtale R A ↔ FormallyUnramified R A ∧ FormallySmooth R A := by
-  rw [FormallyUnramified.iff_comp_injective, formallySmooth_iff, formallyEtale_iff]
-  simp_rw [← forall_and, Function.Bijective]
+theorem iff_formallyUnramified_and_formallySmooth :
+    FormallyEtale R A ↔ FormallyUnramified R A ∧ FormallySmooth R A :=
+  ⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ ⟨inferInstance, inferInstance⟩⟩
 
-instance (priority := 100) to_unramified [h : FormallyEtale R A] :
-    FormallyUnramified R A :=
-  (FormallyEtale.iff_unramified_and_smooth.mp h).1
+@[deprecated (since := "2025-11-03")]
+alias iff_unramified_and_smooth := iff_formallyUnramified_and_formallySmooth
 
-instance (priority := 100) to_smooth [h : FormallyEtale R A] : FormallySmooth R A :=
-  (FormallyEtale.iff_unramified_and_smooth.mp h).2
+theorem of_formallyUnramified_and_formallySmooth [FormallyUnramified R A]
+    [FormallySmooth R A] : FormallyEtale R A :=
+  FormallyEtale.iff_formallyUnramified_and_formallySmooth.mpr ⟨‹_›, ‹_›⟩
 
-theorem of_unramified_and_smooth [h₁ : FormallyUnramified R A]
-    [h₂ : FormallySmooth R A] : FormallyEtale R A :=
-  FormallyEtale.iff_unramified_and_smooth.mpr ⟨h₁, h₂⟩
+@[deprecated (since := "2025-11-03")]
+alias of_unramified_and_smooth := of_formallyUnramified_and_formallySmooth
+
+variable (R A) in
+lemma comp_bijective [FormallyEtale R A] (I : Ideal B) (hI : I ^ 2 = ⊥) :
+    Function.Bijective ((Ideal.Quotient.mkₐ R I).comp : (A →ₐ[R] B) → A →ₐ[R] B ⧸ I) :=
+  ⟨FormallyUnramified.comp_injective I hI, FormallySmooth.comp_surjective R A I hI⟩
+
+/--
+An `R`-algebra `A` is formally etale iff "for every `R`-algebra `B`,
+every square-zero ideal `I : Ideal B` and `f : A →ₐ[R] B ⧸ I`, there exists
+a unique lift `A →ₐ[R] B`".
+-/
+theorem iff_comp_bijective :
+   FormallyEtale R A ↔ ∀ ⦃B : Type max u v⦄ [CommRing B] [Algebra R B] (I : Ideal B), I ^ 2 = ⊥ →
+      Function.Bijective ((Ideal.Quotient.mkₐ R I).comp : (A →ₐ[R] B) → A →ₐ[R] B ⧸ I) :=
+  ⟨fun _ _ ↦ comp_bijective R A, fun H ↦
+    have : FormallyUnramified R A := FormallyUnramified.iff_comp_injective_of_small.{max u v}.mpr
+      (by aesop (add safe Function.Bijective.injective))
+    have : FormallySmooth R A := FormallySmooth.of_comp_surjective
+      (by aesop (add safe Function.Bijective.surjective))
+   .of_formallyUnramified_and_formallySmooth⟩
 
 end
 
 section OfEquiv
 
-variable {R : Type u} [CommRing R]
-variable {A B : Type u} [CommRing A] [Algebra R A] [CommRing B] [Algebra R B]
-
 theorem of_equiv [FormallyEtale R A] (e : A ≃ₐ[R] B) : FormallyEtale R B :=
-  FormallyEtale.iff_unramified_and_smooth.mpr
+  FormallyEtale.iff_formallyUnramified_and_formallySmooth.mpr
     ⟨FormallyUnramified.of_equiv e, FormallySmooth.of_equiv e⟩
 
 theorem iff_of_equiv (e : A ≃ₐ[R] B) : FormallyEtale R A ↔ FormallyEtale R B :=
@@ -87,12 +108,10 @@ end OfEquiv
 
 section Comp
 
-variable (R : Type u) [CommRing R]
-variable (A : Type u) [CommRing A] [Algebra R A]
-variable (B : Type u) [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B]
-
-theorem comp [FormallyEtale R A] [FormallyEtale A B] : FormallyEtale R B :=
-  FormallyEtale.iff_unramified_and_smooth.mpr
+variable (R A B) in
+theorem comp [Algebra A B] [IsScalarTower R A B] [FormallyEtale R A] [FormallyEtale A B] :
+    FormallyEtale R B :=
+  FormallyEtale.iff_formallyUnramified_and_formallySmooth.mpr
     ⟨FormallyUnramified.comp R A B, FormallySmooth.comp R A B⟩
 
 end Comp
@@ -101,12 +120,8 @@ section BaseChange
 
 open scoped TensorProduct
 
-variable {R : Type u} [CommRing R]
-variable {A : Type u} [CommRing A] [Algebra R A]
-variable (B : Type u) [CommRing B] [Algebra R B]
-
-instance base_change [FormallyEtale R A] : FormallyEtale B (B ⊗[R] A) :=
-  FormallyEtale.iff_unramified_and_smooth.mpr ⟨inferInstance, inferInstance⟩
+instance [FormallyEtale R A] : FormallyEtale B (B ⊗[R] A) :=
+  .of_formallyUnramified_and_formallySmooth
 
 end BaseChange
 
@@ -129,7 +144,7 @@ subset `M` of `R`.
 -/
 
 /-! Let R, S, Rₘ, Sₘ be commutative rings -/
-variable {R S Rₘ Sₘ : Type u} [CommRing R] [CommRing S] [CommRing Rₘ] [CommRing Sₘ]
+variable {R S Rₘ Sₘ : Type*} [CommRing R] [CommRing S] [CommRing Rₘ] [CommRing Sₘ]
 /-! Let M be a multiplicatively closed subset of `R` -/
 variable (M : Submonoid R)
 /-! Assume that the rings are in a commutative diagram as above. -/
@@ -140,11 +155,11 @@ variable [IsLocalization M Rₘ] [IsLocalization (M.map (algebraMap R S)) Sₘ]
 include M
 
 theorem of_isLocalization : FormallyEtale R Rₘ :=
-  FormallyEtale.iff_unramified_and_smooth.mpr
+  FormallyEtale.iff_formallyUnramified_and_formallySmooth.mpr
     ⟨FormallyUnramified.of_isLocalization M, FormallySmooth.of_isLocalization M⟩
 
 theorem localization_base [FormallyEtale R Sₘ] : FormallyEtale Rₘ Sₘ :=
-  FormallyEtale.iff_unramified_and_smooth.mpr
+  FormallyEtale.iff_formallyUnramified_and_formallySmooth.mpr
     ⟨FormallyUnramified.localization_base M, FormallySmooth.localization_base M⟩
 
 /-- The localization of a formally étale map is formally étale. -/
@@ -159,9 +174,7 @@ end FormallyEtale
 
 section
 
-variable (R : Type u) [CommRing R]
-variable (A : Type u) [CommRing A] [Algebra R A]
-
+variable (R A) in
 /-- An `R`-algebra `A` is étale if it is formally étale and of finite presentation. -/
 @[stacks 00U1 "Note that this is a different definition from this Stacks entry, but
 <https://stacks.math.columbia.edu/tag/00UR> shows that it is equivalent to the definition here."]
@@ -175,9 +188,6 @@ namespace Etale
 
 attribute [instance] formallyEtale finitePresentation
 
-variable {R : Type u} [CommRing R]
-variable {A B : Type u} [CommRing A] [Algebra R A] [CommRing B] [Algebra R B]
-
 /-- Being étale is transported via algebra isomorphisms. -/
 theorem of_equiv [Etale R A] (e : A ≃ₐ[R] B) : Etale R B where
   formallyEtale := FormallyEtale.of_equiv e
@@ -198,17 +208,19 @@ instance baseChange [Etale R A] : Etale B (B ⊗[R] A) where
 end Comp
 
 /-- Localization at an element is étale. -/
-theorem of_isLocalization_Away (r : R) [IsLocalization.Away r A] : Etale R A where
+theorem of_isLocalizationAway (r : R) [IsLocalization.Away r A] : Etale R A where
   formallyEtale := Algebra.FormallyEtale.of_isLocalization (Submonoid.powers r)
   finitePresentation := IsLocalization.Away.finitePresentation r
 
+@[deprecated (since := "2025-11-03")] alias of_isLocalization_Away := of_isLocalizationAway
+
 end Etale
 
 end Algebra
 
 namespace RingHom
 
-variable {R S : Type u} [CommRing R] [CommRing S]
+variable {R S : Type*} [CommRing R] [CommRing S]
 
 /--
 A ring homomorphism `R →+* A` is formally étale if it is formally unramified and formally smooth.

Mathlib/RingTheory/Etale/Field.lean

@@ -32,7 +32,7 @@ Let `K` be a field, `A` be a `K`-algebra and `L` be a field extension of `K`.
 
 universe u
 
-variable (K L A : Type u) [Field K] [Field L] [CommRing A] [Algebra K L] [Algebra K A]
+variable (K L : Type*) (A : Type u) [Field K] [Field L] [CommRing A] [Algebra K L] [Algebra K A]
 
 open Algebra Polynomial
 
@@ -52,10 +52,10 @@ theorem of_isSeparable_aux [Algebra.IsSeparable K L] [EssFiniteType K L] :
   -- IsSeparable + EssFiniteType => FormallyUnramified + Finite
   have := FormallyUnramified.of_isSeparable K L
   have := FormallyUnramified.finite_of_free (R := K) (S := L)
-  constructor
   -- We shall show that any `f : L → B/I` can be lifted to `L → B` if `I^2 = ⊥`
-  intro B _ _ I h
-  refine ⟨FormallyUnramified.iff_comp_injective.mp (FormallyUnramified.of_isSeparable K L) I h, ?_⟩
+  refine FormallyEtale.iff_comp_bijective.mpr fun B _ _ I h ↦ ?_
+  refine ⟨FormallyUnramified.iff_comp_injective_of_small.mp
+    (FormallyUnramified.of_isSeparable K L) I h, ?_⟩
   intro f
   -- By separability and finiteness, we may assume `L = K(α)` with `p` the minpoly of `α`.
   let pb := Field.powerBasisOfFiniteOfSeparable K L
@@ -89,12 +89,12 @@ theorem of_isSeparable_aux [Algebra.IsSeparable K L] [EssFiniteType K L] :
 
 open scoped IntermediateField in
 lemma of_isSeparable [Algebra.IsSeparable K L] : FormallyEtale K L := by
-  constructor
-  intro B _ _ I h
   -- We shall show that any `f : L → B/I` can be lifted to `L → B` if `I^2 = ⊥`.
+  refine FormallyEtale.iff_comp_bijective.mpr fun B _ _ I h ↦ ?_
   -- But we already know that there exists a unique lift for every finite subfield of `L`
   -- by `of_isSeparable_aux`, so we can glue them all together.
-  refine ⟨FormallyUnramified.iff_comp_injective.mp (FormallyUnramified.of_isSeparable K L) I h, ?_⟩
+  refine ⟨FormallyUnramified.iff_comp_injective_of_small.mp
+    (FormallyUnramified.of_isSeparable K L) I h, ?_⟩
   intro f
   have : ∀ k : L, ∃! g : K⟮k⟯ →ₐ[K] B,
       (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K _ L) := by

Mathlib/RingTheory/Etale/Kaehler.lean

@@ -21,7 +21,7 @@ import Mathlib.RingTheory.Flat.Localization
 
 universe u
 
-variable (R S T : Type u) [CommRing R] [CommRing S] [CommRing T]
+variable (R S T : Type*) [CommRing R] [CommRing S] [CommRing T]
 variable [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T]
 
 open TensorProduct

Mathlib/RingTheory/Etale/Pi.lean

@@ -18,19 +18,17 @@ import Mathlib.RingTheory.Etale.Basic
 
 -/
 
-universe u v
-
 namespace Algebra.FormallyEtale
 
-variable {R : Type (max u v)} {I : Type u} (A : I → Type (max u v))
+variable {R : Type*} {I : Type*} (A : I → Type*)
 variable [CommRing R] [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)]
 
 theorem pi_iff [Finite I] :
     FormallyEtale R (Π i, A i) ↔ ∀ i, FormallyEtale R (A i) := by
-  simp_rw [FormallyEtale.iff_unramified_and_smooth, forall_and]
+  simp_rw [FormallyEtale.iff_formallyUnramified_and_formallySmooth, forall_and]
   rw [FormallyUnramified.pi_iff A, FormallySmooth.pi_iff A]
 
 instance [Finite I] [∀ i, FormallyEtale R (A i)] : FormallyEtale R (Π i, A i) :=
-  .of_unramified_and_smooth
+  .of_formallyUnramified_and_formallySmooth
 
 end Algebra.FormallyEtale

Mathlib/RingTheory/RingHom/Etale.lean

@@ -16,29 +16,27 @@ universe u
 
 namespace RingHom
 
-variable {R S : Type u} [CommRing R] [CommRing S]
+variable {R S : Type*} [CommRing R] [CommRing S]
 
 /-- A ring hom `R →+* S` is étale, if `S` is an étale `R`-algebra. -/
 @[algebraize RingHom.Etale.toAlgebra]
-def Etale {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : Prop :=
-  @Algebra.Etale R _ S _ f.toAlgebra
+def Etale {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S) : Prop :=
+  @Algebra.Etale R S _ _ f.toAlgebra
 
 /-- Helper lemma for the `algebraize` tactic -/
 lemma Etale.toAlgebra {f : R →+* S} (hf : Etale f) :
-    @Algebra.Etale R _ S _ f.toAlgebra := hf
+    @Algebra.Etale R S _ _ f.toAlgebra := hf
 
-variable {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S)
+variable {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S)
 
 lemma etale_algebraMap [Algebra R S] : (algebraMap R S).Etale ↔ Algebra.Etale R S := by
   rw [RingHom.Etale, toAlgebra_algebraMap]
 
 lemma etale_iff_formallyUnramified_and_smooth : f.Etale ↔ f.FormallyUnramified ∧ f.Smooth := by
   algebraize [f]
   simp only [Etale, Smooth, FormallyUnramified]
-  refine ⟨fun h ↦ ⟨inferInstance, ?_⟩, fun ⟨h1, h2⟩ ↦ ⟨?_, inferInstance⟩⟩
-  · constructor <;> infer_instance
-  · rw [Algebra.FormallyEtale.iff_unramified_and_smooth]
-    constructor <;> infer_instance
+  exact ⟨fun h ↦ ⟨inferInstance, inferInstance, inferInstance⟩,
+    fun ⟨h1, h2⟩ ↦ ⟨.of_formallyUnramified_and_formallySmooth, inferInstance⟩⟩
 
 lemma Etale.eq_formallyUnramified_and_smooth :
     @Etale = fun R S (_ : CommRing R) (_ : CommRing S) f ↦ f.FormallyUnramified ∧ f.Smooth := by