feat(RingTheory): being unramified is a local property (#20323)

Co-authored-by: Andrew Yang <[email protected]>

Mathlib.lean

@@ -4392,6 +4392,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.Etale.Pi
 import Mathlib.RingTheory.EuclideanDomain
 import Mathlib.RingTheory.Extension
@@ -4647,6 +4648,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
@@ -4696,6 +4698,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.Locus
 import Mathlib.RingTheory.Unramified.Pi
 import Mathlib.RingTheory.Valuation.AlgebraInstances
 import Mathlib.RingTheory.Valuation.Basic

Mathlib/RingTheory/Etale/Kaehler.lean

@@ -0,0 +1,53 @@
+/-
+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.tensorKaehlerEquivOfFormallyEtale`:
+The canonical isomorphism `T ⊗[S] Ω[S⁄R] ≃ₗ[T] Ω[T⁄R]` 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⁄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.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 _ _)⟩
+  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 (tensorKaehlerEquivOfFormallyEtale R S T).bijective using 1
+  show _ = ((tensorKaehlerEquivOfFormallyEtale
+    R S T).toLinearMap.restrictScalars S : T ⊗[S] Ω[S⁄R] → _)
+  congr!
+  ext
+  simp
+
+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)

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 : Type*} {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

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

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.

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