From fdf3cba544c29272bd3ce4bf615802c9bfe77eea Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Sun, 29 Dec 2024 13:27:34 +0000
Subject: [PATCH 1/8] feat(RingTheory): being unramified is a local property

---
 Mathlib/RingTheory/Etale/Kaehler.lean    |  52 +++++++++++
 Mathlib/RingTheory/Smooth/Kaehler.lean   |   3 +
 Mathlib/RingTheory/Unramified/Basic.lean |  51 ++++++++++-
 Mathlib/RingTheory/Unramified/Local.lean | 112 +++++++++++++++++++++++
 4 files changed, 216 insertions(+), 2 deletions(-)
 create mode 100644 Mathlib/RingTheory/Etale/Kaehler.lean
 create mode 100644 Mathlib/RingTheory/Unramified/Local.lean

diff --git a/Mathlib/RingTheory/Etale/Kaehler.lean b/Mathlib/RingTheory/Etale/Kaehler.lean
new file mode 100644
index 0000000000000..62af90bb2009d
--- /dev/null
+++ b/Mathlib/RingTheory/Etale/Kaehler.lean
@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2024 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.RingTheory.Etale.Basic
+import Mathlib.RingTheory.Kaehler.JacobiZariski
+import Mathlib.RingTheory.Localization.BaseChange
+import Mathlib.RingTheory.Smooth.Kaehler
+
+/-!
+# The differential module and etale algebras
+
+## Main results
+`KaehlerDifferential.tensorKaehlerEquivOfEtale`:
+The canonical isomorphism `T ⊗[S] Ω[S⁄R] ≃ₗ[T] Ω[T⁄S]` for `T` a formally etale `S`-algebra.
+-/
+
+universe u
+
+variable (R S T : Type u) [CommRing R] [CommRing S] [CommRing T]
+variable [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T]
+
+open TensorProduct
+
+/--
+The canonical isomorphism `T ⊗[S] Ω[S⁄R] ≃ₗ[T] Ω[T⁄S]` for `T` a formally etale `S`-algebra.
+Also see `S ⊗[R] Ω[A⁄R] ≃ₗ[S] Ω[S ⊗[R] A⁄S]` at `KaehlerDifferential.tensorKaehlerEquiv`.
+-/
+@[simps! apply] noncomputable
+def KaehlerDifferential.tensorKaehlerEquivOfEtale [Algebra.FormallyEtale S T] :
+    T ⊗[S] Ω[S⁄R] ≃ₗ[T] Ω[T⁄R] := by
+  refine LinearEquiv.ofBijective (mapBaseChange R S T)
+    ⟨?_, fun x ↦ (KaehlerDifferential.exact_mapBaseChange_map R S T x).mp (Subsingleton.elim _ _)⟩
+  rw [injective_iff_map_eq_zero]
+  intros x hx
+  obtain ⟨x, rfl⟩ := (Algebra.H1Cotangent.exact_δ_mapBaseChange R S T x).mp hx
+  rw [Subsingleton.elim x 0, map_zero]
+
+lemma KaehlerDifferential.isBaseChange_of_formallyEtale [Algebra.FormallyEtale S T] :
+    IsBaseChange T (map R R S T) := by
+  show Function.Bijective _
+  convert (tensorKaehlerEquivOfEtale R S T).bijective using 1
+  show _ = ((tensorKaehlerEquivOfEtale R S T).toLinearMap.restrictScalars S : T ⊗[S] Ω[S⁄R] → _)
+  congr!
+  ext
+  simp
+
+instance KaehlerDifferential.isLocalization (M : Submonoid S) [IsLocalization M T] :
+    IsLocalizedModule M (map R R S T) :=
+  have := Algebra.FormallyEtale.of_isLocalization (Rₘ := T) M
+  (isLocalizedModule_iff_isBaseChange M T _).mpr (isBaseChange_of_formallyEtale R S T)
diff --git a/Mathlib/RingTheory/Smooth/Kaehler.lean b/Mathlib/RingTheory/Smooth/Kaehler.lean
index 780d71c547b67..089823b7d0f64 100644
--- a/Mathlib/RingTheory/Smooth/Kaehler.lean
+++ b/Mathlib/RingTheory/Smooth/Kaehler.lean
@@ -447,3 +447,6 @@ theorem Algebra.FormallySmooth.iff_subsingleton_and_projective :
   show Function.Injective (Generators.self R S).toExtension.cotangentComplex ↔ _
   rw [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot]
   rfl
+
+instance [Algebra.FormallySmooth R S] : Subsingleton (Algebra.H1Cotangent R S) :=
+  (Algebra.FormallySmooth.iff_subsingleton_and_projective.mp ‹_›).1
diff --git a/Mathlib/RingTheory/Unramified/Basic.lean b/Mathlib/RingTheory/Unramified/Basic.lean
index 81416a42263dc..7a44659d7f2a5 100644
--- a/Mathlib/RingTheory/Unramified/Basic.lean
+++ b/Mathlib/RingTheory/Unramified/Basic.lean
@@ -7,6 +7,7 @@ import Mathlib.RingTheory.FiniteStability
 import Mathlib.RingTheory.Ideal.Quotient.Nilpotent
 import Mathlib.RingTheory.Kaehler.Basic
 import Mathlib.RingTheory.Localization.Away.AdjoinRoot
+import Mathlib.RingTheory.LocalProperties.Basic
 
 /-!
 
@@ -39,8 +40,7 @@ namespace Algebra
 
 section
 
-variable (R : Type v) [CommRing R]
-variable (A : Type u) [CommRing A] [Algebra R A]
+variable (R : Type v) (A : Type u) [CommRing R] [CommRing A] [Algebra R A]
 
 /--
 An `R`-algebra `A` is formally unramified if `Ω[A⁄R]` is trivial.
@@ -335,3 +335,50 @@ end Comp
 end Unramified
 
 end Algebra
+section RingHom
+
+variable {R S : Type*} [CommRing R] [CommRing S]
+
+/--
+A ring homomorphism `R →+* A` is formally unramified if `Ω[A⁄R]` is trivial.
+See `Algebra.FormallyUnramified`.
+-/
+@[algebraize Algebra.FormallyUnramified]
+def RingHom.FormallyUnramified (f : R →+* S) : Prop :=
+  letI := f.toAlgebra
+  Algebra.FormallyUnramified R S
+
+lemma RingHom.formallyUnramified_algebraMap [Algebra R S] :
+    (algebraMap R S).FormallyUnramified ↔ Algebra.FormallyUnramified R S := by
+  delta FormallyUnramified
+  congr!
+  exact Algebra.algebra_ext _ _ fun _ ↦ rfl
+
+lemma RingHom.stableUnderComposition_formallyUnramified :
+    RingHom.StableUnderComposition RingHom.FormallyUnramified := by
+  intros R S T _ _ _ f g _ _
+  algebraize [f, g, g.comp f]
+  exact .comp R S T
+
+lemma RingHom.respectsIso_formallyUnramified :
+    RingHom.RespectsIso RingHom.FormallyUnramified := by
+  refine RingHom.stableUnderComposition_formallyUnramified.respectsIso ?_
+  intros R S _ _ e
+  letI := e.toRingHom.toAlgebra
+  exact Algebra.FormallyUnramified.of_surjective (Algebra.ofId R S) e.surjective
+
+lemma RingHom.holdsForLocalization_formallyUnramified :
+    RingHom.HoldsForLocalizationAway RingHom.FormallyUnramified := by
+  intros R S _ _ _ r _
+  rw [RingHom.formallyUnramified_algebraMap]
+  exact .of_isLocalization (.powers r)
+
+lemma RingHom.isStableUnderBaseChange_formallyUnramified :
+    RingHom.IsStableUnderBaseChange RingHom.FormallyUnramified := by
+  refine .mk _ RingHom.respectsIso_formallyUnramified ?_
+  intros R S T _ _ _ _ _ h
+  show (algebraMap _ _).FormallyUnramified
+  rw [RingHom.formallyUnramified_algebraMap] at h ⊢
+  infer_instance
+
+end RingHom
diff --git a/Mathlib/RingTheory/Unramified/Local.lean b/Mathlib/RingTheory/Unramified/Local.lean
new file mode 100644
index 0000000000000..36eda4a082714
--- /dev/null
+++ b/Mathlib/RingTheory/Unramified/Local.lean
@@ -0,0 +1,112 @@
+/-
+Copyright (c) 2024 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
+import Mathlib.RingTheory.Etale.Kaehler
+import Mathlib.RingTheory.Support
+
+/-!
+# Unramified is a local property
+
+## Main results
+- `Algebra.unramifiedLocus` : The set of primes that is unramified over the base.
+- `Algebra.basicOpen_subset_unramifiedLocus_iff` :
+  `D(f)` is contained in the unramified locus if and only if `A_f` is unramified over `R`.
+- `Algebra.unramifiedLocus_eq_univ_iff` :
+  The unramified locus is the whole spectrum if and only if `A` is unramified over `R`.
+- `Algebra.isOpen_unramifiedLocus` :
+  If `A` is (essentially) of finite type over `R`, then the unramified locus is open.
+-/
+
+universe u
+
+variable (R A : Type u) [CommRing R] [CommRing A] [Algebra R A]
+
+namespace Algebra
+
+/-- `Algebra.unramifiedLocus R A` is the set of primes `p` of `A`
+such that `Aₚ` is formally unramified over `R`. -/
+def unramifiedLocus : Set (PrimeSpectrum A) :=
+  { p | Algebra.FormallyUnramified R (Localization.AtPrime p.asIdeal) }
+
+variable {R A}
+
+lemma unramifiedLocus_eq_compl_support :
+    unramifiedLocus R A = (Module.support A (Ω[A⁄R]))ᶜ := by
+  ext p
+  simp only [Set.mem_compl_iff, Module.not_mem_support_iff]
+  have := IsLocalizedModule.iso p.asIdeal.primeCompl
+    (KaehlerDifferential.map R R A (Localization.AtPrime p.asIdeal))
+  exact (Algebra.formallyUnramified_iff _ _).trans this.subsingleton_congr.symm
+
+lemma basicOpen_subset_unramifiedLocus_iff {f : A} :
+    ↑(PrimeSpectrum.basicOpen f) ⊆ unramifiedLocus R A ↔
+      Algebra.FormallyUnramified R (Localization.Away f) := by
+  rw [unramifiedLocus_eq_compl_support, Set.subset_compl_comm,
+    PrimeSpectrum.basicOpen_eq_zeroLocus_compl, compl_compl,
+    ← LocalizedModule.subsingleton_iff_support_subset, Algebra.formallyUnramified_iff]
+  exact (IsLocalizedModule.iso (.powers f)
+    (KaehlerDifferential.map R R A (Localization.Away f))).subsingleton_congr
+
+lemma unramifiedLocus_eq_univ_iff :
+    unramifiedLocus R A = Set.univ ↔ Algebra.FormallyUnramified R A := by
+  rw [unramifiedLocus_eq_compl_support, compl_eq_comm, Set.compl_univ, eq_comm,
+    Module.support_eq_empty_iff, Algebra.formallyUnramified_iff]
+
+lemma isOpen_unramifiedLocus [EssFiniteType R A] : IsOpen (unramifiedLocus R A) := by
+  rw [unramifiedLocus_eq_compl_support, Module.support_eq_zeroLocus]
+  exact (PrimeSpectrum.isClosed_zeroLocus _).isOpen_compl
+
+end Algebra
+
+lemma RingHom.ofLocalizationPrime_formallyUnramified :
+    RingHom.OfLocalizationPrime RingHom.FormallyUnramified := by
+  intros R S _ _ f H
+  algebraize [f]
+  rw [FormallyUnramified, ← Algebra.unramifiedLocus_eq_univ_iff, Set.eq_univ_iff_forall]
+  intro x
+  let Rₓ := Localization.AtPrime (x.asIdeal.comap f)
+  let Sₓ := Localization.AtPrime x.asIdeal
+  have := Algebra.FormallyUnramified.of_isLocalization (Rₘ := Rₓ) (x.asIdeal.comap f).primeCompl
+  letI : Algebra Rₓ Sₓ := (Localization.localRingHom _ _ _ rfl).toAlgebra
+  have : IsScalarTower R Rₓ Sₓ := .of_algebraMap_eq
+    fun x ↦ (Localization.localRingHom_to_map _ _ _ rfl x).symm
+  have : Algebra.FormallyUnramified Rₓ Sₓ := H _ _
+  exact Algebra.FormallyUnramified.comp R Rₓ Sₓ
+
+lemma RingHom.ofLocalizationSpanTarget_formallyUnramified :
+    RingHom.OfLocalizationSpanTarget RingHom.FormallyUnramified := by
+  intros R S _ _ f s hs H
+  algebraize [f]
+  rw [FormallyUnramified, ← Algebra.unramifiedLocus_eq_univ_iff, Set.eq_univ_iff_forall]
+  intro x
+  obtain ⟨r, hr, hrx⟩ : ∃ r ∈ s, x ∈ PrimeSpectrum.basicOpen r := by
+    simpa using (PrimeSpectrum.iSup_basicOpen_eq_top_iff'.mpr hs).ge
+      (TopologicalSpace.Opens.mem_top x)
+  refine Algebra.basicOpen_subset_unramifiedLocus_iff.mpr ?_ hrx
+  convert H ⟨r, hr⟩
+  dsimp
+  rw [← RingHom.algebraMap_toAlgebra f, ← IsScalarTower.algebraMap_eq,
+    RingHom.formallyUnramified_algebraMap]
+
+lemma RingHom.isLocal_formallyUnramified :
+    RingHom.PropertyIsLocal RingHom.FormallyUnramified := by
+  constructor
+  · intro R S _ _ f r R' S' _ _ _ _ _ _ H
+    algebraize [f, (algebraMap S S').comp f, IsLocalization.Away.map R' S' f r]
+    have := Algebra.FormallyUnramified.of_isLocalization (Rₘ := S') (.powers (f r))
+    have := Algebra.FormallyUnramified.comp R S S'
+    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 RingHom.ofLocalizationSpanTarget_formallyUnramified
+  · exact RingHom.ofLocalizationSpanTarget_formallyUnramified.ofLocalizationSpan
+      (RingHom.stableUnderComposition_formallyUnramified
+        |>.stableUnderCompositionWithLocalizationAway
+          RingHom.holdsForLocalizationAway_formallyUnramified).1
+  · exact (RingHom.stableUnderComposition_formallyUnramified
+      |>.stableUnderCompositionWithLocalizationAway
+        RingHom.holdsForLocalizationAway_formallyUnramified).2

From 2d2a8767494b72f6fe44b7bb482ac8411b5e1d40 Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Sun, 29 Dec 2024 14:35:33 +0000
Subject: [PATCH 2/8] oops

---
 Mathlib.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index d6a597218d32d..71c666f962086 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -4361,6 +4361,7 @@ import Mathlib.RingTheory.EisensteinCriterion
 import Mathlib.RingTheory.EssentialFiniteness
 import Mathlib.RingTheory.Etale.Basic
 import Mathlib.RingTheory.Etale.Field
+import Mathlib.RingTheory.Etale.Kaehler
 import Mathlib.RingTheory.EuclideanDomain
 import Mathlib.RingTheory.Extension
 import Mathlib.RingTheory.Filtration
@@ -4664,6 +4665,7 @@ import Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
 import Mathlib.RingTheory.Unramified.Basic
 import Mathlib.RingTheory.Unramified.Field
 import Mathlib.RingTheory.Unramified.Finite
+import Mathlib.RingTheory.Unramified.Local
 import Mathlib.RingTheory.Unramified.Pi
 import Mathlib.RingTheory.Valuation.AlgebraInstances
 import Mathlib.RingTheory.Valuation.Basic

From f02c4644b05ddbcc957dc9a275404bf199bfc5ca Mon Sep 17 00:00:00 2001
From: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Date: Sun, 29 Dec 2024 15:14:49 +0000
Subject: [PATCH 3/8] Update Basic.lean

---
 Mathlib/RingTheory/Unramified/Basic.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Mathlib/RingTheory/Unramified/Basic.lean b/Mathlib/RingTheory/Unramified/Basic.lean
index 7a44659d7f2a5..fd65e4452af9d 100644
--- a/Mathlib/RingTheory/Unramified/Basic.lean
+++ b/Mathlib/RingTheory/Unramified/Basic.lean
@@ -367,12 +367,6 @@ lemma RingHom.respectsIso_formallyUnramified :
   letI := e.toRingHom.toAlgebra
   exact Algebra.FormallyUnramified.of_surjective (Algebra.ofId R S) e.surjective
 
-lemma RingHom.holdsForLocalization_formallyUnramified :
-    RingHom.HoldsForLocalizationAway RingHom.FormallyUnramified := by
-  intros R S _ _ _ r _
-  rw [RingHom.formallyUnramified_algebraMap]
-  exact .of_isLocalization (.powers r)
-
 lemma RingHom.isStableUnderBaseChange_formallyUnramified :
     RingHom.IsStableUnderBaseChange RingHom.FormallyUnramified := by
   refine .mk _ RingHom.respectsIso_formallyUnramified ?_
@@ -381,4 +375,10 @@ lemma RingHom.isStableUnderBaseChange_formallyUnramified :
   rw [RingHom.formallyUnramified_algebraMap] at h ⊢
   infer_instance
 
+lemma RingHom.holdsForLocalizationAway_formallyUnramified :
+    RingHom.HoldsForLocalizationAway RingHom.FormallyUnramified := by
+  intros R S _ _ _ r _
+  rw [RingHom.formallyUnramified_algebraMap]
+  exact .of_isLocalization (.powers r)
+
 end RingHom

From 6026487f88894032a9a14f9d2d78beb9590c97c2 Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Mon, 6 Jan 2025 15:28:42 +0000
Subject: [PATCH 4/8] move to new file

---
 Mathlib.lean                             |   2 +-
 Mathlib/RingTheory/Unramified/Basic.lean |  47 ----------
 Mathlib/RingTheory/Unramified/Local.lean | 112 -----------------------
 Mathlib/RingTheory/Unramified/Locus.lean |  62 +++++++++++++
 4 files changed, 63 insertions(+), 160 deletions(-)
 delete mode 100644 Mathlib/RingTheory/Unramified/Local.lean
 create mode 100644 Mathlib/RingTheory/Unramified/Locus.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 71c666f962086..2214b7617b414 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -4665,7 +4665,7 @@ import Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
 import Mathlib.RingTheory.Unramified.Basic
 import Mathlib.RingTheory.Unramified.Field
 import Mathlib.RingTheory.Unramified.Finite
-import Mathlib.RingTheory.Unramified.Local
+import Mathlib.RingTheory.Unramified.Locus
 import Mathlib.RingTheory.Unramified.Pi
 import Mathlib.RingTheory.Valuation.AlgebraInstances
 import Mathlib.RingTheory.Valuation.Basic
diff --git a/Mathlib/RingTheory/Unramified/Basic.lean b/Mathlib/RingTheory/Unramified/Basic.lean
index fd65e4452af9d..11ef4e2e19cbd 100644
--- a/Mathlib/RingTheory/Unramified/Basic.lean
+++ b/Mathlib/RingTheory/Unramified/Basic.lean
@@ -335,50 +335,3 @@ end Comp
 end Unramified
 
 end Algebra
-section RingHom
-
-variable {R S : Type*} [CommRing R] [CommRing S]
-
-/--
-A ring homomorphism `R →+* A` is formally unramified if `Ω[A⁄R]` is trivial.
-See `Algebra.FormallyUnramified`.
--/
-@[algebraize Algebra.FormallyUnramified]
-def RingHom.FormallyUnramified (f : R →+* S) : Prop :=
-  letI := f.toAlgebra
-  Algebra.FormallyUnramified R S
-
-lemma RingHom.formallyUnramified_algebraMap [Algebra R S] :
-    (algebraMap R S).FormallyUnramified ↔ Algebra.FormallyUnramified R S := by
-  delta FormallyUnramified
-  congr!
-  exact Algebra.algebra_ext _ _ fun _ ↦ rfl
-
-lemma RingHom.stableUnderComposition_formallyUnramified :
-    RingHom.StableUnderComposition RingHom.FormallyUnramified := by
-  intros R S T _ _ _ f g _ _
-  algebraize [f, g, g.comp f]
-  exact .comp R S T
-
-lemma RingHom.respectsIso_formallyUnramified :
-    RingHom.RespectsIso RingHom.FormallyUnramified := by
-  refine RingHom.stableUnderComposition_formallyUnramified.respectsIso ?_
-  intros R S _ _ e
-  letI := e.toRingHom.toAlgebra
-  exact Algebra.FormallyUnramified.of_surjective (Algebra.ofId R S) e.surjective
-
-lemma RingHom.isStableUnderBaseChange_formallyUnramified :
-    RingHom.IsStableUnderBaseChange RingHom.FormallyUnramified := by
-  refine .mk _ RingHom.respectsIso_formallyUnramified ?_
-  intros R S T _ _ _ _ _ h
-  show (algebraMap _ _).FormallyUnramified
-  rw [RingHom.formallyUnramified_algebraMap] at h ⊢
-  infer_instance
-
-lemma RingHom.holdsForLocalizationAway_formallyUnramified :
-    RingHom.HoldsForLocalizationAway RingHom.FormallyUnramified := by
-  intros R S _ _ _ r _
-  rw [RingHom.formallyUnramified_algebraMap]
-  exact .of_isLocalization (.powers r)
-
-end RingHom
diff --git a/Mathlib/RingTheory/Unramified/Local.lean b/Mathlib/RingTheory/Unramified/Local.lean
deleted file mode 100644
index 36eda4a082714..0000000000000
--- a/Mathlib/RingTheory/Unramified/Local.lean
+++ /dev/null
@@ -1,112 +0,0 @@
-/-
-Copyright (c) 2024 Andrew Yang. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Andrew Yang
--/
-import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
-import Mathlib.RingTheory.Etale.Kaehler
-import Mathlib.RingTheory.Support
-
-/-!
-# Unramified is a local property
-
-## Main results
-- `Algebra.unramifiedLocus` : The set of primes that is unramified over the base.
-- `Algebra.basicOpen_subset_unramifiedLocus_iff` :
-  `D(f)` is contained in the unramified locus if and only if `A_f` is unramified over `R`.
-- `Algebra.unramifiedLocus_eq_univ_iff` :
-  The unramified locus is the whole spectrum if and only if `A` is unramified over `R`.
-- `Algebra.isOpen_unramifiedLocus` :
-  If `A` is (essentially) of finite type over `R`, then the unramified locus is open.
--/
-
-universe u
-
-variable (R A : Type u) [CommRing R] [CommRing A] [Algebra R A]
-
-namespace Algebra
-
-/-- `Algebra.unramifiedLocus R A` is the set of primes `p` of `A`
-such that `Aₚ` is formally unramified over `R`. -/
-def unramifiedLocus : Set (PrimeSpectrum A) :=
-  { p | Algebra.FormallyUnramified R (Localization.AtPrime p.asIdeal) }
-
-variable {R A}
-
-lemma unramifiedLocus_eq_compl_support :
-    unramifiedLocus R A = (Module.support A (Ω[A⁄R]))ᶜ := by
-  ext p
-  simp only [Set.mem_compl_iff, Module.not_mem_support_iff]
-  have := IsLocalizedModule.iso p.asIdeal.primeCompl
-    (KaehlerDifferential.map R R A (Localization.AtPrime p.asIdeal))
-  exact (Algebra.formallyUnramified_iff _ _).trans this.subsingleton_congr.symm
-
-lemma basicOpen_subset_unramifiedLocus_iff {f : A} :
-    ↑(PrimeSpectrum.basicOpen f) ⊆ unramifiedLocus R A ↔
-      Algebra.FormallyUnramified R (Localization.Away f) := by
-  rw [unramifiedLocus_eq_compl_support, Set.subset_compl_comm,
-    PrimeSpectrum.basicOpen_eq_zeroLocus_compl, compl_compl,
-    ← LocalizedModule.subsingleton_iff_support_subset, Algebra.formallyUnramified_iff]
-  exact (IsLocalizedModule.iso (.powers f)
-    (KaehlerDifferential.map R R A (Localization.Away f))).subsingleton_congr
-
-lemma unramifiedLocus_eq_univ_iff :
-    unramifiedLocus R A = Set.univ ↔ Algebra.FormallyUnramified R A := by
-  rw [unramifiedLocus_eq_compl_support, compl_eq_comm, Set.compl_univ, eq_comm,
-    Module.support_eq_empty_iff, Algebra.formallyUnramified_iff]
-
-lemma isOpen_unramifiedLocus [EssFiniteType R A] : IsOpen (unramifiedLocus R A) := by
-  rw [unramifiedLocus_eq_compl_support, Module.support_eq_zeroLocus]
-  exact (PrimeSpectrum.isClosed_zeroLocus _).isOpen_compl
-
-end Algebra
-
-lemma RingHom.ofLocalizationPrime_formallyUnramified :
-    RingHom.OfLocalizationPrime RingHom.FormallyUnramified := by
-  intros R S _ _ f H
-  algebraize [f]
-  rw [FormallyUnramified, ← Algebra.unramifiedLocus_eq_univ_iff, Set.eq_univ_iff_forall]
-  intro x
-  let Rₓ := Localization.AtPrime (x.asIdeal.comap f)
-  let Sₓ := Localization.AtPrime x.asIdeal
-  have := Algebra.FormallyUnramified.of_isLocalization (Rₘ := Rₓ) (x.asIdeal.comap f).primeCompl
-  letI : Algebra Rₓ Sₓ := (Localization.localRingHom _ _ _ rfl).toAlgebra
-  have : IsScalarTower R Rₓ Sₓ := .of_algebraMap_eq
-    fun x ↦ (Localization.localRingHom_to_map _ _ _ rfl x).symm
-  have : Algebra.FormallyUnramified Rₓ Sₓ := H _ _
-  exact Algebra.FormallyUnramified.comp R Rₓ Sₓ
-
-lemma RingHom.ofLocalizationSpanTarget_formallyUnramified :
-    RingHom.OfLocalizationSpanTarget RingHom.FormallyUnramified := by
-  intros R S _ _ f s hs H
-  algebraize [f]
-  rw [FormallyUnramified, ← Algebra.unramifiedLocus_eq_univ_iff, Set.eq_univ_iff_forall]
-  intro x
-  obtain ⟨r, hr, hrx⟩ : ∃ r ∈ s, x ∈ PrimeSpectrum.basicOpen r := by
-    simpa using (PrimeSpectrum.iSup_basicOpen_eq_top_iff'.mpr hs).ge
-      (TopologicalSpace.Opens.mem_top x)
-  refine Algebra.basicOpen_subset_unramifiedLocus_iff.mpr ?_ hrx
-  convert H ⟨r, hr⟩
-  dsimp
-  rw [← RingHom.algebraMap_toAlgebra f, ← IsScalarTower.algebraMap_eq,
-    RingHom.formallyUnramified_algebraMap]
-
-lemma RingHom.isLocal_formallyUnramified :
-    RingHom.PropertyIsLocal RingHom.FormallyUnramified := by
-  constructor
-  · intro R S _ _ f r R' S' _ _ _ _ _ _ H
-    algebraize [f, (algebraMap S S').comp f, IsLocalization.Away.map R' S' f r]
-    have := Algebra.FormallyUnramified.of_isLocalization (Rₘ := S') (.powers (f r))
-    have := Algebra.FormallyUnramified.comp R S S'
-    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 RingHom.ofLocalizationSpanTarget_formallyUnramified
-  · exact RingHom.ofLocalizationSpanTarget_formallyUnramified.ofLocalizationSpan
-      (RingHom.stableUnderComposition_formallyUnramified
-        |>.stableUnderCompositionWithLocalizationAway
-          RingHom.holdsForLocalizationAway_formallyUnramified).1
-  · exact (RingHom.stableUnderComposition_formallyUnramified
-      |>.stableUnderCompositionWithLocalizationAway
-        RingHom.holdsForLocalizationAway_formallyUnramified).2
diff --git a/Mathlib/RingTheory/Unramified/Locus.lean b/Mathlib/RingTheory/Unramified/Locus.lean
new file mode 100644
index 0000000000000..ec9cd9995a51e
--- /dev/null
+++ b/Mathlib/RingTheory/Unramified/Locus.lean
@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2024 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
+import Mathlib.RingTheory.Etale.Kaehler
+import Mathlib.RingTheory.Support
+
+/-!
+# Unramified locus of an algebra
+
+## Main results
+- `Algebra.unramifiedLocus` : The set of primes that is unramified over the base.
+- `Algebra.basicOpen_subset_unramifiedLocus_iff` :
+  `D(f)` is contained in the unramified locus if and only if `A_f` is unramified over `R`.
+- `Algebra.unramifiedLocus_eq_univ_iff` :
+  The unramified locus is the whole spectrum if and only if `A` is unramified over `R`.
+- `Algebra.isOpen_unramifiedLocus` :
+  If `A` is (essentially) of finite type over `R`, then the unramified locus is open.
+-/
+
+universe u
+
+variable (R A : Type u) [CommRing R] [CommRing A] [Algebra R A]
+
+namespace Algebra
+
+/-- `Algebra.unramifiedLocus R A` is the set of primes `p` of `A`
+such that `Aₚ` is formally unramified over `R`. -/
+def unramifiedLocus : Set (PrimeSpectrum A) :=
+  { p | Algebra.FormallyUnramified R (Localization.AtPrime p.asIdeal) }
+
+variable {R A}
+
+lemma unramifiedLocus_eq_compl_support :
+    unramifiedLocus R A = (Module.support A (Ω[A⁄R]))ᶜ := by
+  ext p
+  simp only [Set.mem_compl_iff, Module.not_mem_support_iff]
+  have := IsLocalizedModule.iso p.asIdeal.primeCompl
+    (KaehlerDifferential.map R R A (Localization.AtPrime p.asIdeal))
+  exact (Algebra.formallyUnramified_iff _ _).trans this.subsingleton_congr.symm
+
+lemma basicOpen_subset_unramifiedLocus_iff {f : A} :
+    ↑(PrimeSpectrum.basicOpen f) ⊆ unramifiedLocus R A ↔
+      Algebra.FormallyUnramified R (Localization.Away f) := by
+  rw [unramifiedLocus_eq_compl_support, Set.subset_compl_comm,
+    PrimeSpectrum.basicOpen_eq_zeroLocus_compl, compl_compl,
+    ← LocalizedModule.subsingleton_iff_support_subset, Algebra.formallyUnramified_iff]
+  exact (IsLocalizedModule.iso (.powers f)
+    (KaehlerDifferential.map R R A (Localization.Away f))).subsingleton_congr
+
+lemma unramifiedLocus_eq_univ_iff :
+    unramifiedLocus R A = Set.univ ↔ Algebra.FormallyUnramified R A := by
+  rw [unramifiedLocus_eq_compl_support, compl_eq_comm, Set.compl_univ, eq_comm,
+    Module.support_eq_empty_iff, Algebra.formallyUnramified_iff]
+
+lemma isOpen_unramifiedLocus [EssFiniteType R A] : IsOpen (unramifiedLocus R A) := by
+  rw [unramifiedLocus_eq_compl_support, Module.support_eq_zeroLocus]
+  exact (PrimeSpectrum.isClosed_zeroLocus _).isOpen_compl
+
+end Algebra

From 5a740ef6c1af15dfcc395db6867f01862a6609e1 Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Mon, 6 Jan 2025 15:30:08 +0000
Subject: [PATCH 5/8] oops

---
 Mathlib.lean                               |   1 +
 Mathlib/RingTheory/RingHom/Unramified.lean | 111 +++++++++++++++++++++
 Mathlib/RingTheory/Unramified/Basic.lean   |   4 +-
 3 files changed, 114 insertions(+), 2 deletions(-)
 create mode 100644 Mathlib/RingTheory/RingHom/Unramified.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 2214b7617b414..4cf333b946ecd 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -4616,6 +4616,7 @@ import Mathlib.RingTheory.RingHom.Integral
 import Mathlib.RingTheory.RingHom.Locally
 import Mathlib.RingTheory.RingHom.StandardSmooth
 import Mathlib.RingTheory.RingHom.Surjective
+import Mathlib.RingTheory.RingHom.Unramified
 import Mathlib.RingTheory.RingHomProperties
 import Mathlib.RingTheory.RingInvo
 import Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed
diff --git a/Mathlib/RingTheory/RingHom/Unramified.lean b/Mathlib/RingTheory/RingHom/Unramified.lean
new file mode 100644
index 0000000000000..2f64bd3193de9
--- /dev/null
+++ b/Mathlib/RingTheory/RingHom/Unramified.lean
@@ -0,0 +1,111 @@
+/-
+Copyright (c) 2024 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.RingTheory.Unramified.Locus
+import Mathlib.RingTheory.LocalProperties.Basic
+
+/-!
+
+# The meta properties of unramified ring homomorphisms.
+
+-/
+
+namespace RingHom
+
+variable {R S : Type*} [CommRing R] [CommRing S]
+
+/--
+A ring homomorphism `R →+* A` is formally unramified if `Ω[A⁄R]` is trivial.
+See `Algebra.FormallyUnramified`.
+-/
+@[algebraize Algebra.FormallyUnramified]
+def FormallyUnramified (f : R →+* S) : Prop :=
+  letI := f.toAlgebra
+  Algebra.FormallyUnramified R S
+
+lemma formallyUnramified_algebraMap [Algebra R S] :
+    (algebraMap R S).FormallyUnramified ↔ Algebra.FormallyUnramified R S := by
+  delta FormallyUnramified
+  congr!
+  exact Algebra.algebra_ext _ _ fun _ ↦ rfl
+
+namespace FormallyUnramified
+
+lemma stableUnderComposition :
+    StableUnderComposition FormallyUnramified := by
+  intros R S T _ _ _ f g _ _
+  algebraize [f, g, g.comp f]
+  exact .comp R S T
+
+lemma respectsIso :
+    RespectsIso FormallyUnramified := by
+  refine stableUnderComposition.respectsIso ?_
+  intros R S _ _ e
+  letI := e.toRingHom.toAlgebra
+  exact Algebra.FormallyUnramified.of_surjective (Algebra.ofId R S) e.surjective
+
+lemma isStableUnderBaseChange :
+    IsStableUnderBaseChange FormallyUnramified := by
+  refine .mk _ respectsIso ?_
+  intros R S T _ _ _ _ _ h
+  show (algebraMap _ _).FormallyUnramified
+  rw [formallyUnramified_algebraMap] at h ⊢
+  infer_instance
+
+lemma holdsForLocalizationAway :
+    HoldsForLocalizationAway FormallyUnramified := by
+  intros R S _ _ _ r _
+  rw [formallyUnramified_algebraMap]
+  exact .of_isLocalization (.powers r)
+
+lemma ofLocalizationPrime :
+    OfLocalizationPrime FormallyUnramified := by
+  intros R S _ _ f H
+  algebraize [f]
+  rw [FormallyUnramified, ← Algebra.unramifiedLocus_eq_univ_iff, Set.eq_univ_iff_forall]
+  intro x
+  let Rₓ := Localization.AtPrime (x.asIdeal.comap f)
+  let Sₓ := Localization.AtPrime x.asIdeal
+  have := Algebra.FormallyUnramified.of_isLocalization (Rₘ := Rₓ) (x.asIdeal.comap f).primeCompl
+  letI : Algebra Rₓ Sₓ := (Localization.localRingHom _ _ _ rfl).toAlgebra
+  have : IsScalarTower R Rₓ Sₓ := .of_algebraMap_eq
+    fun x ↦ (Localization.localRingHom_to_map _ _ _ rfl x).symm
+  have : Algebra.FormallyUnramified Rₓ Sₓ := H _ _
+  exact Algebra.FormallyUnramified.comp R Rₓ Sₓ
+
+lemma ofLocalizationSpanTarget :
+    OfLocalizationSpanTarget FormallyUnramified := by
+  intros R S _ _ f s hs H
+  algebraize [f]
+  rw [FormallyUnramified, ← Algebra.unramifiedLocus_eq_univ_iff, Set.eq_univ_iff_forall]
+  intro x
+  obtain ⟨r, hr, hrx⟩ : ∃ r ∈ s, x ∈ PrimeSpectrum.basicOpen r := by
+    simpa using (PrimeSpectrum.iSup_basicOpen_eq_top_iff'.mpr hs).ge
+      (TopologicalSpace.Opens.mem_top x)
+  refine Algebra.basicOpen_subset_unramifiedLocus_iff.mpr ?_ hrx
+  convert H ⟨r, hr⟩
+  dsimp
+  rw [← algebraMap_toAlgebra f, ← IsScalarTower.algebraMap_eq,
+    formallyUnramified_algebraMap]
+
+lemma propertyIsLocal :
+    PropertyIsLocal FormallyUnramified := by
+  constructor
+  · intro R S _ _ f r R' S' _ _ _ _ _ _ H
+    algebraize [f, (algebraMap S S').comp f, IsLocalization.Away.map R' S' f r]
+    have := Algebra.FormallyUnramified.of_isLocalization (Rₘ := S') (.powers (f r))
+    have := Algebra.FormallyUnramified.comp R S S'
+    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 ofLocalizationSpanTarget
+  · exact ofLocalizationSpanTarget.ofLocalizationSpan
+      (stableUnderComposition.stableUnderCompositionWithLocalizationAway
+          holdsForLocalizationAway).1
+  · exact (stableUnderComposition.stableUnderCompositionWithLocalizationAway
+        holdsForLocalizationAway).2
+
+end RingHom.FormallyUnramified
diff --git a/Mathlib/RingTheory/Unramified/Basic.lean b/Mathlib/RingTheory/Unramified/Basic.lean
index 11ef4e2e19cbd..81416a42263dc 100644
--- a/Mathlib/RingTheory/Unramified/Basic.lean
+++ b/Mathlib/RingTheory/Unramified/Basic.lean
@@ -7,7 +7,6 @@ import Mathlib.RingTheory.FiniteStability
 import Mathlib.RingTheory.Ideal.Quotient.Nilpotent
 import Mathlib.RingTheory.Kaehler.Basic
 import Mathlib.RingTheory.Localization.Away.AdjoinRoot
-import Mathlib.RingTheory.LocalProperties.Basic
 
 /-!
 
@@ -40,7 +39,8 @@ namespace Algebra
 
 section
 
-variable (R : Type v) (A : Type u) [CommRing R] [CommRing A] [Algebra R A]
+variable (R : Type v) [CommRing R]
+variable (A : Type u) [CommRing A] [Algebra R A]
 
 /--
 An `R`-algebra `A` is formally unramified if `Ω[A⁄R]` is trivial.

From 9049053e0f0ba72b6bf7813ce1bbd029f4867c9d Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Mon, 6 Jan 2025 15:42:21 +0000
Subject: [PATCH 6/8] fix again

---
 Mathlib/RingTheory/RingHom/Unramified.lean | 2 +-
 Mathlib/RingTheory/Unramified/Basic.lean   | 3 +--
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/Mathlib/RingTheory/RingHom/Unramified.lean b/Mathlib/RingTheory/RingHom/Unramified.lean
index 2f64bd3193de9..1016996901edb 100644
--- a/Mathlib/RingTheory/RingHom/Unramified.lean
+++ b/Mathlib/RingTheory/RingHom/Unramified.lean
@@ -14,7 +14,7 @@ import Mathlib.RingTheory.LocalProperties.Basic
 
 namespace RingHom
 
-variable {R S : Type*} [CommRing R] [CommRing S]
+variable {R : Type*} {S : Type*} [CommRing R] [CommRing S]
 
 /--
 A ring homomorphism `R →+* A` is formally unramified if `Ω[A⁄R]` is trivial.
diff --git a/Mathlib/RingTheory/Unramified/Basic.lean b/Mathlib/RingTheory/Unramified/Basic.lean
index 81416a42263dc..9e91002b6692d 100644
--- a/Mathlib/RingTheory/Unramified/Basic.lean
+++ b/Mathlib/RingTheory/Unramified/Basic.lean
@@ -39,8 +39,7 @@ namespace Algebra
 
 section
 
-variable (R : Type v) [CommRing R]
-variable (A : Type u) [CommRing A] [Algebra R A]
+variable (R : Type v) (A : Type u) [CommRing R] [CommRing A] [Algebra R A]
 
 /--
 An `R`-algebra `A` is formally unramified if `Ω[A⁄R]` is trivial.

From 36fde450687e735d60b0e4e16304296419bde0e8 Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Mon, 6 Jan 2025 15:43:38 +0000
Subject: [PATCH 7/8] address comments

---
 Mathlib/RingTheory/Etale/Kaehler.lean | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/Mathlib/RingTheory/Etale/Kaehler.lean b/Mathlib/RingTheory/Etale/Kaehler.lean
index 62af90bb2009d..1ac4c96c3ba43 100644
--- a/Mathlib/RingTheory/Etale/Kaehler.lean
+++ b/Mathlib/RingTheory/Etale/Kaehler.lean
@@ -12,8 +12,8 @@ import Mathlib.RingTheory.Smooth.Kaehler
 # The differential module and etale algebras
 
 ## Main results
-`KaehlerDifferential.tensorKaehlerEquivOfEtale`:
-The canonical isomorphism `T ⊗[S] Ω[S⁄R] ≃ₗ[T] Ω[T⁄S]` for `T` a formally etale `S`-algebra.
+`KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale`:
+The canonical isomorphism `T ⊗[S] Ω[S⁄R] ≃ₗ[T] Ω[T⁄R]` for `T` a formally etale `S`-algebra.
 -/
 
 universe u
@@ -24,11 +24,11 @@ variable [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T]
 open TensorProduct
 
 /--
-The canonical isomorphism `T ⊗[S] Ω[S⁄R] ≃ₗ[T] Ω[T⁄S]` for `T` a formally etale `S`-algebra.
+The canonical isomorphism `T ⊗[S] Ω[S⁄R] ≃ₗ[T] Ω[T⁄R]` for `T` a formally etale `S`-algebra.
 Also see `S ⊗[R] Ω[A⁄R] ≃ₗ[S] Ω[S ⊗[R] A⁄S]` at `KaehlerDifferential.tensorKaehlerEquiv`.
 -/
 @[simps! apply] noncomputable
-def KaehlerDifferential.tensorKaehlerEquivOfEtale [Algebra.FormallyEtale S T] :
+def KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale [Algebra.FormallyEtale S T] :
     T ⊗[S] Ω[S⁄R] ≃ₗ[T] Ω[T⁄R] := by
   refine LinearEquiv.ofBijective (mapBaseChange R S T)
     ⟨?_, fun x ↦ (KaehlerDifferential.exact_mapBaseChange_map R S T x).mp (Subsingleton.elim _ _)⟩
@@ -40,13 +40,14 @@ def KaehlerDifferential.tensorKaehlerEquivOfEtale [Algebra.FormallyEtale S T] :
 lemma KaehlerDifferential.isBaseChange_of_formallyEtale [Algebra.FormallyEtale S T] :
     IsBaseChange T (map R R S T) := by
   show Function.Bijective _
-  convert (tensorKaehlerEquivOfEtale R S T).bijective using 1
-  show _ = ((tensorKaehlerEquivOfEtale R S T).toLinearMap.restrictScalars S : T ⊗[S] Ω[S⁄R] → _)
+  convert (tensorKaehlerEquivOfFormallyEtale R S T).bijective using 1
+  show _ = ((tensorKaehlerEquivOfFormallyEtale
+    R S T).toLinearMap.restrictScalars S : T ⊗[S] Ω[S⁄R] → _)
   congr!
   ext
   simp
 
-instance KaehlerDifferential.isLocalization (M : Submonoid S) [IsLocalization M T] :
+instance KaehlerDifferential.isLocalizedModule (M : Submonoid S) [IsLocalization M T] :
     IsLocalizedModule M (map R R S T) :=
   have := Algebra.FormallyEtale.of_isLocalization (Rₘ := T) M
   (isLocalizedModule_iff_isBaseChange M T _).mpr (isBaseChange_of_formallyEtale R S T)

From 35916247f0a2ae28e84028987814900b7dbb9e0a Mon Sep 17 00:00:00 2001
From: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Date: Mon, 6 Jan 2025 16:01:54 +0000
Subject: [PATCH 8/8] Update Kaehler.lean

---
 Mathlib/RingTheory/Etale/Kaehler.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/RingTheory/Etale/Kaehler.lean b/Mathlib/RingTheory/Etale/Kaehler.lean
index 1ac4c96c3ba43..509af402e838f 100644
--- a/Mathlib/RingTheory/Etale/Kaehler.lean
+++ b/Mathlib/RingTheory/Etale/Kaehler.lean
@@ -47,7 +47,7 @@ lemma KaehlerDifferential.isBaseChange_of_formallyEtale [Algebra.FormallyEtale S
   ext
   simp
 
-instance KaehlerDifferential.isLocalizedModule (M : Submonoid S) [IsLocalization M T] :
+instance KaehlerDifferential.isLocalizedModule_map (M : Submonoid S) [IsLocalization M T] :
     IsLocalizedModule M (map R R S T) :=
   have := Algebra.FormallyEtale.of_isLocalization (Rₘ := T) M
   (isLocalizedModule_iff_isBaseChange M T _).mpr (isBaseChange_of_formallyEtale R S T)