feat(RingTheory): miscellaneous lemmas about etale (#30857)

Author: erdOne

Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean

@@ -98,7 +98,7 @@ theorem of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
     [FormallyUnramified (f ≫ g)] : FormallyUnramified f :=
   HasRingHomProperty.of_comp (fun {R S T _ _ _} f g H ↦ by
     algebraize [f, g, g.comp f]
-    exact Algebra.FormallyUnramified.of_comp R S T) ‹_›
+    exact Algebra.FormallyUnramified.of_restrictScalars R S T) ‹_›
 
 instance : MorphismProperty.IsMultiplicative @FormallyUnramified where
   id_mem _ := inferInstance

Mathlib/RingTheory/Etale/Basic.lean

@@ -108,14 +108,29 @@ end OfEquiv
 
 section Comp
 
+variable [Algebra A B] [IsScalarTower R A B]
+
 variable (R A B) in
-theorem comp [Algebra A B] [IsScalarTower R A B] [FormallyEtale R A] [FormallyEtale A B] :
+theorem comp [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⟩
 
+lemma Algebra.FormallyEtale.of_restrictScalars [FormallyUnramified R A] [FormallyEtale R B] :
+    FormallyEtale A B :=
+  have := FormallyUnramified.of_restrictScalars R A B
+  have := FormallySmooth.of_restrictScalars R A B
+  .of_formallyUnramified_and_formallySmooth
+
 end Comp
 
+lemma Algebra.FormallyEtale.iff_of_surjective
+    {R S : Type u} [CommRing R] [CommRing S]
+    [Algebra R S] (h : Function.Surjective (algebraMap R S)) :
+    Algebra.FormallyEtale R S ↔ IsIdempotentElem (RingHom.ker (algebraMap R S)) := by
+  rw [FormallyEtale.iff_formallyUnramified_and_formallySmooth, ← FormallySmooth.iff_of_surjective h,
+    and_iff_right (FormallyUnramified.of_surjective (Algebra.ofId R S) h)]
+
 section BaseChange
 
 open scoped TensorProduct

Mathlib/RingTheory/RingHom/Unramified.lean

@@ -97,7 +97,7 @@ lemma propertyIsLocal :
     have H : Submonoid.powers r ≤ (Submonoid.powers (f r)).comap f := by
       rintro x ⟨n, rfl⟩; exact ⟨n, by simp⟩
     have : IsScalarTower R R' S' := .of_algebraMap_eq' (IsLocalization.map_comp H).symm
-    exact Algebra.FormallyUnramified.of_comp R R' S'
+    exact Algebra.FormallyUnramified.of_restrictScalars R R' S'
   · exact ofLocalizationSpanTarget
   · exact ofLocalizationSpanTarget.ofLocalizationSpan
       (stableUnderComposition.stableUnderCompositionWithLocalizationAway

Mathlib/RingTheory/Smooth/Basic.lean

@@ -7,6 +7,7 @@ import Mathlib.RingTheory.FiniteStability
 import Mathlib.RingTheory.Ideal.Quotient.Nilpotent
 import Mathlib.RingTheory.Localization.Away.AdjoinRoot
 import Mathlib.RingTheory.Smooth.Kaehler
+import Mathlib.RingTheory.Unramified.Basic
 
 /-!
 
@@ -381,6 +382,8 @@ open scoped Polynomial in
 instance polynomial (R : Type*) [CommRing R] :
   FormallySmooth R R[X] := .of_equiv (MvPolynomial.pUnitAlgEquiv.{_, 0} R)
 
+instance : FormallySmooth R R := .of_equiv (MvPolynomial.isEmptyAlgEquiv R Empty)
+
 end Polynomial
 
 section Comp
@@ -397,8 +400,41 @@ theorem comp [FormallySmooth R A] [FormallySmooth A B] : FormallySmooth R B := b
   apply_fun AlgHom.restrictScalars R at e'
   exact ⟨f''.restrictScalars _, e'.trans (AlgHom.ext fun _ => rfl)⟩
 
+lemma of_restrictScalars [FormallyUnramified R A] [FormallySmooth R B] :
+    FormallySmooth A B := by
+  refine iff_comp_surjective.mpr fun C _ _ I hI f ↦ ?_
+  algebraize [(algebraMap A C).comp (algebraMap R A)]
+  obtain ⟨g, hg⟩ := Algebra.FormallySmooth.comp_surjective _ _ I hI (f.restrictScalars R)
+  suffices g.comp (IsScalarTower.toAlgHom R A B) = IsScalarTower.toAlgHom R A C from
+    ⟨{ __ := g, commutes' x := congr($this x) }, AlgHom.ext fun x ↦ congr($hg x)⟩
+  apply Algebra.FormallyUnramified.comp_injective _ hI
+  rw [← AlgHom.comp_assoc, hg]
+  exact AlgHom.ext f.commutes
+
 end Comp
 
+section surjective
+
+variable {R : Type*} [CommRing R]
+variable {P A : Type*} [CommRing A] [Algebra R A] [CommRing P] [Algebra R P]
+variable (f : P →ₐ[R] A)
+
+lemma iff_of_surjective (h : Function.Surjective (algebraMap R A)) :
+    Algebra.FormallySmooth R A ↔ IsIdempotentElem (RingHom.ker (algebraMap R A)) := by
+  rw [Algebra.FormallySmooth.iff_split_surjection (Algebra.ofId R A) h]
+  constructor
+  · intro ⟨g, hg⟩
+    let e : A ≃ₐ[R] R ⧸ RingHom.ker (algebraMap R A) ^ 2 :=
+      .ofAlgHom _ _ (Ideal.Quotient.algHom_ext _ (by ext)) hg
+    rw [IsIdempotentElem, ← pow_two, ← Ideal.mk_ker (I := _ ^ 2), ← Ideal.Quotient.algebraMap_eq,
+      ← e.toAlgHom.comp_algebraMap, RingHom.ker_comp_of_injective _ (by exact e.injective)]
+  · intro H
+    let e := (Ideal.quotientEquivAlgOfEq _ ((pow_two _).trans H)).trans
+      (Ideal.quotientKerAlgEquivOfSurjective (f := Algebra.ofId R A) h)
+    exact ⟨e.symm.toAlgHom, AlgHom.ext <| h.forall.mpr fun x ↦ by simp⟩
+
+end surjective
+
 section BaseChange
 
 open scoped TensorProduct

Mathlib/RingTheory/Unramified/Basic.lean

@@ -220,7 +220,7 @@ theorem comp [FormallyUnramified R A] [FormallyUnramified A B] :
   congr
   exact FormallyUnramified.ext I ⟨2, hI⟩ (AlgHom.congr_fun e)
 
-theorem of_comp [FormallyUnramified R B] : FormallyUnramified A B := by
+theorem of_restrictScalars [FormallyUnramified R B] : FormallyUnramified A B := by
   rw [iff_comp_injective]
   intro Q _ _ I e f₁ f₂ e'
   letI := ((algebraMap A Q).comp (algebraMap R A)).toAlgebra
@@ -230,6 +230,8 @@ theorem of_comp [FormallyUnramified R B] : FormallyUnramified A B := by
   intro x
   exact AlgHom.congr_fun e' x
 
+@[deprecated (since := "2025-10-24")] alias of_comp := of_restrictScalars
+
 end Comp
 
 section of_surjective
@@ -308,7 +310,7 @@ The intended use is for copying proofs between `Formally{Unramified, Smooth, Eta
 without the need to change anything (including removing redundant arguments). -/
 @[nolint unusedArguments]
 theorem localization_base [FormallyUnramified R Sₘ] : FormallyUnramified Rₘ Sₘ :=
-  FormallyUnramified.of_comp R Rₘ Sₘ
+  FormallyUnramified.of_restrictScalars R Rₘ Sₘ
 
 theorem localization_map [FormallyUnramified R S] :
     FormallyUnramified Rₘ Sₘ := by

Mathlib/RingTheory/Unramified/Field.lean

@@ -197,7 +197,7 @@ theorem range_eq_top_of_isPurelyInseparable
 theorem isSeparable : Algebra.IsSeparable K L := by
   have := finite_of_free (R := K) (S := L)
   rw [← separableClosure.eq_top_iff]
-  have := of_comp K (separableClosure K L) L
+  have := of_restrictScalars K (separableClosure K L) L
   have := EssFiniteType.of_comp K (separableClosure K L) L
   ext
   change _ ↔ _ ∈ (⊤ : Subring _)

Mathlib/RingTheory/Unramified/LocalRing.lean

@@ -34,7 +34,7 @@ instance : FormallyUnramified S (ResidueField S) := .quotient _
 instance [FormallyUnramified R S] :
     FormallyUnramified (ResidueField R) (ResidueField S) :=
   have : FormallyUnramified R (ResidueField S) := .comp _ S _
-  .of_comp R _ _
+  .of_restrictScalars R _ _
 
 variable [EssFiniteType R S]
 
@@ -56,7 +56,7 @@ lemma FormallyUnramified.isField_quotient_map_maximalIdeal [FormallyUnramified R
   have hmR : mR ≤ maximalIdeal S := ((local_hom_TFAE (algebraMap R S)).out 0 2 rfl rfl).mp ‹_›
   letI : Algebra (ResidueField R) (S ⧸ mR) := inferInstanceAs (Algebra (R ⧸ _) _)
   have : IsScalarTower R (ResidueField R) (S ⧸ mR) := inferInstanceAs (IsScalarTower R (R ⧸ _) _)
-  have : FormallyUnramified (ResidueField R) (S ⧸ mR) := .of_comp R _ _
+  have : FormallyUnramified (ResidueField R) (S ⧸ mR) := .of_restrictScalars R _ _
   have : EssFiniteType (ResidueField R) (S ⧸ mR) := .of_comp R _ _
   have : Module.Finite (ResidueField R) (S ⧸ mR) := FormallyUnramified.finite_of_free _ _
   have : IsReduced (S ⧸ mR) := FormallyUnramified.isReduced_of_field (ResidueField R) (S ⧸ mR)
@@ -131,7 +131,7 @@ lemma isUnramifiedAt_iff_map_eq [EssFiniteType R S]
     Localization.isLocalHom_localRingHom _ _ _ Ideal.LiesOver.over
   have : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q) := .of_comp R _ _
   trans Algebra.FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime q)
-  · exact ⟨fun _ ↦ .of_comp R _ _,
+  · exact ⟨fun _ ↦ .of_restrictScalars R _ _,
       fun _ ↦ Algebra.FormallyUnramified.comp _ (Localization.AtPrime p) _⟩
   rw [FormallyUnramified.iff_map_maximalIdeal_eq]
   congr!

Mathlib/RingTheory/Unramified/Locus.lean

@@ -48,13 +48,13 @@ lemma IsUnramifiedAt.comp
     (p : Ideal A) (P : Ideal B) [P.LiesOver p] [p.IsPrime] [P.IsPrime]
     [IsUnramifiedAt R p] [IsUnramifiedAt A P] : IsUnramifiedAt R P := by
   have : FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime P) :=
-    .of_comp A _ _
+    .of_restrictScalars A _ _
   exact FormallyUnramified.comp R (Localization.AtPrime p) _
 
 variable (R) in
 lemma IsUnramifiedAt.of_restrictScalars (P : Ideal B) [P.IsPrime]
     [IsUnramifiedAt R P] : IsUnramifiedAt A P :=
-  FormallyUnramified.of_comp R _ _
+  FormallyUnramified.of_restrictScalars R _ _
 
 end