chore(RingTheory/Etale): split in multiple folders and files (#12017)

Splits `RingTheory/Etale.lean` into 3 new separate folders for étale (resp. unramified, resp. smooth) morphisms.

Mathlib.lean

@@ -3313,7 +3313,7 @@ import Mathlib.RingTheory.DiscreteValuationRing.Basic
 import Mathlib.RingTheory.DiscreteValuationRing.TFAE
 import Mathlib.RingTheory.Discriminant
 import Mathlib.RingTheory.EisensteinCriterion
-import Mathlib.RingTheory.Etale
+import Mathlib.RingTheory.Etale.Basic
 import Mathlib.RingTheory.EuclideanDomain
 import Mathlib.RingTheory.Filtration
 import Mathlib.RingTheory.FinitePresentation
@@ -3454,6 +3454,7 @@ import Mathlib.RingTheory.RootsOfUnity.Basic
 import Mathlib.RingTheory.RootsOfUnity.Complex
 import Mathlib.RingTheory.RootsOfUnity.Minpoly
 import Mathlib.RingTheory.SimpleModule
+import Mathlib.RingTheory.Smooth.Basic
 import Mathlib.RingTheory.Subring.Basic
 import Mathlib.RingTheory.Subring.Order
 import Mathlib.RingTheory.Subring.Pointwise
@@ -3464,6 +3465,7 @@ import Mathlib.RingTheory.Subsemiring.Pointwise
 import Mathlib.RingTheory.TensorProduct.Basic
 import Mathlib.RingTheory.Trace
 import Mathlib.RingTheory.UniqueFactorizationDomain
+import Mathlib.RingTheory.Unramified.Basic
 import Mathlib.RingTheory.Valuation.Basic
 import Mathlib.RingTheory.Valuation.ExtendToLocalization
 import Mathlib.RingTheory.Valuation.Integers

Mathlib/RingTheory/Etale/Basic.lean

@@ -0,0 +1,146 @@
+/-
+Copyright (c) 2022 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.RingTheory.Kaehler
+import Mathlib.RingTheory.QuotientNilpotent
+import Mathlib.RingTheory.Smooth.Basic
+import Mathlib.RingTheory.Unramified.Basic
+
+#align_import ring_theory.etale from "leanprover-community/mathlib"@"73f96237417835f148a1f7bc1ff55f67119b7166"
+
+/-!
+
+# Etale morphisms
+
+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`.
+
+We show that the property extends onto nilpotent ideals, and that these properties are stable
+under `R`-algebra homomorphisms and compositions.
+
+## TODO:
+
+- Define étale morphisms
+
+-/
+
+
+-- Porting note: added to make the syntax work below.
+open scoped TensorProduct
+
+universe u
+
+namespace Algebra
+
+section
+
+variable (R : Type u) [CommSemiring R]
+variable (A : Type u) [Semiring A] [Algebra R A]
+variable {B : Type u} [CommRing B] [Algebra R B] (I : Ideal B)
+
+/-- 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`. -/
+@[mk_iff]
+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)
+#align algebra.formally_etale Algebra.FormallyEtale
+
+variable {R A}
+
+theorem FormallyEtale.iff_unramified_and_smooth :
+    FormallyEtale R A ↔ FormallyUnramified R A ∧ FormallySmooth R A := by
+  rw [formallyUnramified_iff, formallySmooth_iff, formallyEtale_iff]
+  simp_rw [← forall_and, Function.Bijective]
+#align algebra.formally_etale.iff_unramified_and_smooth Algebra.FormallyEtale.iff_unramified_and_smooth
+
+instance (priority := 100) FormallyEtale.to_unramified [h : FormallyEtale R A] :
+    FormallyUnramified R A :=
+  (FormallyEtale.iff_unramified_and_smooth.mp h).1
+#align algebra.formally_etale.to_unramified Algebra.FormallyEtale.to_unramified
+
+instance (priority := 100) FormallyEtale.to_smooth [h : FormallyEtale R A] : FormallySmooth R A :=
+  (FormallyEtale.iff_unramified_and_smooth.mp h).2
+#align algebra.formally_etale.to_smooth Algebra.FormallyEtale.to_smooth
+
+theorem FormallyEtale.of_unramified_and_smooth [h₁ : FormallyUnramified R A]
+    [h₂ : FormallySmooth R A] : FormallyEtale R A :=
+  FormallyEtale.iff_unramified_and_smooth.mpr ⟨h₁, h₂⟩
+#align algebra.formally_etale.of_unramified_and_smooth Algebra.FormallyEtale.of_unramified_and_smooth
+
+end
+
+section OfEquiv
+
+variable {R : Type u} [CommSemiring R]
+variable {A B : Type u} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B]
+
+theorem FormallyEtale.of_equiv [FormallyEtale R A] (e : A ≃ₐ[R] B) : FormallyEtale R B :=
+  FormallyEtale.iff_unramified_and_smooth.mpr
+    ⟨FormallyUnramified.of_equiv e, FormallySmooth.of_equiv e⟩
+#align algebra.formally_etale.of_equiv Algebra.FormallyEtale.of_equiv
+
+end OfEquiv
+
+section Comp
+
+variable (R : Type u) [CommSemiring R]
+variable (A : Type u) [CommSemiring A] [Algebra R A]
+variable (B : Type u) [Semiring B] [Algebra R B] [Algebra A B] [IsScalarTower R A B]
+
+theorem FormallyEtale.comp [FormallyEtale R A] [FormallyEtale A B] : FormallyEtale R B :=
+  FormallyEtale.iff_unramified_and_smooth.mpr
+    ⟨FormallyUnramified.comp R A B, FormallySmooth.comp R A B⟩
+#align algebra.formally_etale.comp Algebra.FormallyEtale.comp
+
+end Comp
+
+section BaseChange
+
+open scoped TensorProduct
+
+variable {R : Type u} [CommSemiring R]
+variable {A : Type u} [Semiring A] [Algebra R A]
+variable (B : Type u) [CommSemiring B] [Algebra R B]
+
+instance FormallyEtale.base_change [FormallyEtale R A] : FormallyEtale B (B ⊗[R] A) :=
+  FormallyEtale.iff_unramified_and_smooth.mpr ⟨inferInstance, inferInstance⟩
+#align algebra.formally_etale.base_change Algebra.FormallyEtale.base_change
+
+end BaseChange
+
+section Localization
+
+variable {R S Rₘ Sₘ : Type u} [CommRing R] [CommRing S] [CommRing Rₘ] [CommRing Sₘ]
+variable (M : Submonoid R)
+variable [Algebra R S] [Algebra R Sₘ] [Algebra S Sₘ] [Algebra R Rₘ] [Algebra Rₘ Sₘ]
+variable [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ]
+variable [IsLocalization M Rₘ] [IsLocalization (M.map (algebraMap R S)) Sₘ]
+
+-- Porting note: no longer supported
+-- attribute [local elab_as_elim] Ideal.IsNilpotent.induction_on
+
+theorem FormallyEtale.of_isLocalization : FormallyEtale R Rₘ :=
+  FormallyEtale.iff_unramified_and_smooth.mpr
+    ⟨FormallyUnramified.of_isLocalization M, FormallySmooth.of_isLocalization M⟩
+#align algebra.formally_etale.of_is_localization Algebra.FormallyEtale.of_isLocalization
+
+theorem FormallyEtale.localization_base [FormallyEtale R Sₘ] : FormallyEtale Rₘ Sₘ :=
+  FormallyEtale.iff_unramified_and_smooth.mpr
+    ⟨FormallyUnramified.localization_base M, FormallySmooth.localization_base M⟩
+#align algebra.formally_etale.localization_base Algebra.FormallyEtale.localization_base
+
+theorem FormallyEtale.localization_map [FormallyEtale R S] : FormallyEtale Rₘ Sₘ := by
+  haveI : FormallyEtale S Sₘ := FormallyEtale.of_isLocalization (M.map (algebraMap R S))
+  haveI : FormallyEtale R Sₘ := FormallyEtale.comp R S Sₘ
+  exact FormallyEtale.localization_base M
+#align algebra.formally_etale.localization_map Algebra.FormallyEtale.localization_map
+
+end Localization
+
+end Algebra