feat(AlgebraicGeometry/ResidueField): classification of Spec K ⟶ X …

…with `K` a field (#17768) This PR adds more API for residue fields and in particular the classification of morphisms `Spec K ⟶ X` with `K` a field. From the valuative criterion project. Co-authored-by: Qi Ge Co-authored-by: Andrew Yang Co-authored-by: Andrew Yang <[email protected]> Co-authored-by: Christian Merten <[email protected]>
leanprover-community · Oct 19, 2024 · fee48cc · fee48cc
1 parent 721c01e
commit fee48cc
Show file tree

Hide file tree

Showing 4 changed files with 150 additions and 6 deletions.
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean b/Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
@@ -3,12 +3,10 @@ Copyright (c) 2023 Jonas van der Schaaf. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Amelia Livingston, Christian Merten, Jonas van der Schaaf
 -/
-import Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
 import Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
 import Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
 import Mathlib.AlgebraicGeometry.Morphisms.FiniteType
 import Mathlib.AlgebraicGeometry.ResidueField
-import Mathlib.RingTheory.RingHom.Surjective
 
 /-!
 
@@ -134,6 +132,10 @@ theorem of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsClosedImmersion
     simp_rw [Scheme.stalkMap_comp] at h
     exact Function.Surjective.of_comp h
 
+instance Spec_map_residue {X : Scheme.{u}} (x) : IsClosedImmersion (Spec.map (X.residue x)) :=
+  IsClosedImmersion.spec_of_surjective (X.residue x)
+    Ideal.Quotient.mk_surjective
+
 instance {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] : QuasiCompact f where
   isCompact_preimage _ _ hU' := base_closed.isCompact_preimage hU'
 

diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean b/Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean
@@ -5,6 +5,7 @@ Authors: Andrew Yang
 -/
 import Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
 import Mathlib.RingTheory.RingHom.Surjective
+import Mathlib.RingTheory.SurjectiveOnStalks
 
 /-!
 
@@ -95,6 +96,32 @@ theorem comp_iff {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsPreimmersion g]
     IsPreimmersion (f ≫ g) ↔ IsPreimmersion f :=
   ⟨fun _ ↦ of_comp f g, fun _ ↦ inferInstance⟩
 
+lemma Spec_map_iff {R S : CommRingCat.{u}} (f : R ⟶ S) :
+    IsPreimmersion (Spec.map f) ↔ Embedding (PrimeSpectrum.comap f) ∧ f.SurjectiveOnStalks := by
+  haveI : (RingHom.toMorphismProperty <| fun f ↦ Function.Surjective f).RespectsIso := by
+    rw [← RingHom.toMorphismProperty_respectsIso_iff]
+    exact RingHom.surjective_respectsIso
+  refine ⟨fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ⟨h₁, fun (x : PrimeSpectrum S) ↦ ?_⟩⟩
+  · intro p hp
+    let e := Scheme.arrowStalkMapSpecIso f ⟨p, hp⟩
+    apply ((RingHom.toMorphismProperty <| fun f ↦ Function.Surjective f).arrow_mk_iso_iff e).mp
+    exact h₂ ⟨p, hp⟩
+  · let e := Scheme.arrowStalkMapSpecIso f x
+    apply ((RingHom.toMorphismProperty <| fun f ↦ Function.Surjective f).arrow_mk_iso_iff e).mpr
+    exact h₂ x.asIdeal x.isPrime
+
+lemma mk_Spec_map {R S : CommRingCat.{u}} {f : R ⟶ S}
+    (h₁ : Embedding (PrimeSpectrum.comap f)) (h₂ : f.SurjectiveOnStalks) :
+    IsPreimmersion (Spec.map f) :=
+  (Spec_map_iff f).mpr ⟨h₁, h₂⟩
+
+lemma of_isLocalization {R S : Type u} [CommRing R] (M : Submonoid R) [CommRing S]
+    [Algebra R S] [IsLocalization M S] :
+    IsPreimmersion (Spec.map (CommRingCat.ofHom <| algebraMap R S)) :=
+  IsPreimmersion.mk_Spec_map
+    (PrimeSpectrum.localization_comap_embedding (R := R) S M)
+    (RingHom.surjectiveOnStalks_of_isLocalization (M := M) S)
+
 end IsPreimmersion
 
 end AlgebraicGeometry
diff --git a/Mathlib/AlgebraicGeometry/ResidueField.lean b/Mathlib/AlgebraicGeometry/ResidueField.lean
@@ -3,8 +3,8 @@ 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.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
 import Mathlib.AlgebraicGeometry.Stalk
+import Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
 
 /-!
 
@@ -20,12 +20,15 @@ The following are in the `AlgebraicGeometry.Scheme` namespace:
 - `AlgebraicGeometry.Scheme.Hom.residueFieldMap`: A morphism of schemes induce a homomorphism of
   residue fields.
 - `AlgebraicGeometry.Scheme.fromSpecResidueField`: The canonical map `Spec κ(x) ⟶ X`.
+- `AlgebraicGeometry.Scheme.SpecToEquivOfField`: morphisms `Spec K ⟶ X` for a field `K` correspond
+  to pairs of `x : X` with embedding `κ(x) ⟶ K`.
+
 
 -/
 
 universe u
 
-open CategoryTheory TopologicalSpace Opposite
+open CategoryTheory TopologicalSpace Opposite LocalRing
 
 noncomputable section
 
@@ -45,12 +48,37 @@ instance (x : X) : Field (X.residueField x) :=
 def residue (X : Scheme.{u}) (x) : X.presheaf.stalk x ⟶ X.residueField x :=
   LocalRing.residue _
 
+/-- See `AlgebraicGeometry.IsClosedImmersion.Spec_map_residue` for the stronger result that
+`Spec.map (X.residue x)` is a closed immersion. -/
+instance {X : Scheme.{u}} (x) : IsPreimmersion (Spec.map (X.residue x)) :=
+  IsPreimmersion.mk_Spec_map
+    (PrimeSpectrum.closedEmbedding_comap_of_surjective _ _ (Ideal.Quotient.mk_surjective)).embedding
+    (RingHom.surjectiveOnStalks_of_surjective (Ideal.Quotient.mk_surjective))
+
+@[simp]
+lemma Spec_map_residue_apply {X : Scheme.{u}} (x : X) (s : Spec (X.residueField x)) :
+    (Spec.map (X.residue x)).base s = closedPoint (X.presheaf.stalk x) :=
+  LocalRing.PrimeSpectrum.comap_residue _ s
+
 lemma residue_surjective (X : Scheme.{u}) (x) : Function.Surjective (X.residue x) :=
   Ideal.Quotient.mk_surjective
 
 instance (X : Scheme.{u}) (x) : Epi (X.residue x) :=
   ConcreteCategory.epi_of_surjective _ (X.residue_surjective x)
 
+/-- If `K` is a field and `f : 𝒪_{X, x} ⟶ K` is a ring map, then this is the induced
+map `κ(x) ⟶ K`. -/
+def descResidueField {K : Type u} [Field K] {X : Scheme.{u}} {x : X}
+    (f : X.presheaf.stalk x ⟶ .of K) [IsLocalHom f] :
+    X.residueField x ⟶ .of K :=
+  LocalRing.ResidueField.lift (S := K) f
+
+@[reassoc (attr := simp)]
+lemma residue_descResidueField {K : Type u} [Field K] {X : Scheme.{u}} {x}
+    (f : X.presheaf.stalk x ⟶ .of K) [IsLocalHom f] :
+    X.residue x ≫ X.descResidueField f = f :=
+  RingHom.ext fun _ ↦ rfl
+
 /--
 If `U` is an open of `X` containing `x`, we have a canonical ring map from the sections
 over `U` to the residue field of `x`.
@@ -171,23 +199,97 @@ lemma residue_residueFieldCongr (X : Scheme) {x y : X} (h : x = y) :
   subst h
   simp
 
+lemma Hom.residueFieldMap_congr {f g : X ⟶ Y} (e : f = g) (x : X) :
+    f.residueFieldMap x = (Y.residueFieldCongr (by subst e; rfl)).hom ≫ g.residueFieldMap x := by
+  subst e; simp
+
 end congr
 
 section fromResidueField
 
 /-- The canonical map `Spec κ(x) ⟶ X`. -/
 def fromSpecResidueField (X : Scheme) (x : X) :
     Spec (X.residueField x) ⟶ X :=
-  Spec.map (CommRingCat.ofHom (X.residue x)) ≫ X.fromSpecStalk x
+  Spec.map (X.residue x) ≫ X.fromSpecStalk x
+
+instance {X : Scheme.{u}} (x : X) : IsPreimmersion (X.fromSpecResidueField x) := by
+  dsimp only [Scheme.fromSpecResidueField]
+  rw [IsPreimmersion.comp_iff]
+  infer_instance
 
 @[reassoc (attr := simp)]
 lemma residueFieldCongr_fromSpecResidueField {x y : X} (h : x = y) :
     Spec.map (X.residueFieldCongr h).hom ≫ X.fromSpecResidueField _ =
       X.fromSpecResidueField _ := by
   subst h; simp
 
+@[reassoc]
+lemma Hom.Spec_map_residueFieldMap_fromSpecResidueField (x : X) :
+    Spec.map (f.residueFieldMap x) ≫ Y.fromSpecResidueField _ =
+      X.fromSpecResidueField x ≫ f := by
+  dsimp only [fromSpecResidueField]
+  rw [Category.assoc, ← Spec_map_stalkMap_fromSpecStalk, ← Spec.map_comp_assoc,
+    ← Spec.map_comp_assoc]
+  rfl
+
+@[simp]
+lemma fromSpecResidueField_apply (x : X.carrier) (s : Spec (X.residueField x)) :
+    (X.fromSpecResidueField x).base s = x := by
+  simp [fromSpecResidueField]
+
+lemma range_fromSpecResidueField (x : X.carrier) :
+    Set.range (X.fromSpecResidueField x).base = {x} := by
+  ext s
+  simp only [Set.mem_range, fromSpecResidueField_apply, Set.mem_singleton_iff, eq_comm (a := s)]
+  constructor
+  · rintro ⟨-, h⟩
+    exact h
+  · rintro rfl
+    exact ⟨closedPoint (X.residueField x), rfl⟩
+
+lemma descResidueField_fromSpecResidueField {K : Type*} [Field K] (X : Scheme) {x}
+    (f : X.presheaf.stalk x ⟶ .of K) [IsLocalHom f] :
+    Spec.map (X.descResidueField f) ≫
+      X.fromSpecResidueField x = Spec.map f ≫ X.fromSpecStalk x := by
+  simp [fromSpecResidueField, ← Spec.map_comp_assoc]
+
+lemma descResidueField_stalkClosedPointTo_fromSpecResidueField
+    (K : Type u) [Field K] (X : Scheme.{u}) (f : Spec (.of K) ⟶ X) :
+    Spec.map (X.descResidueField (Scheme.stalkClosedPointTo f)) ≫
+      X.fromSpecResidueField (f.base (closedPoint K)) = f := by
+  erw [X.descResidueField_fromSpecResidueField]
+  rw [Scheme.Spec_stalkClosedPointTo_fromSpecStalk]
+
 end fromResidueField
 
+/-- A helper lemma to work with `AlgebraicGeometry.Scheme.SpecToEquivOfField`. -/
+lemma SpecToEquivOfField_eq_iff {K : Type*} [Field K] {X : Scheme}
+    {f₁ f₂ : Σ x : X.carrier, X.residueField x ⟶ .of K} :
+    f₁ = f₂ ↔ ∃ e : f₁.1 = f₂.1, f₁.2 = (X.residueFieldCongr e).hom ≫ f₂.2 := by
+  constructor
+  · rintro rfl
+    simp
+  · obtain ⟨f, _⟩ := f₁
+    obtain ⟨g, _⟩ := f₂
+    rintro ⟨(rfl : f = g), h⟩
+    simpa
+
+/-- For a field `K` and a scheme `X`, the morphisms `Spec K ⟶ X` bijectively correspond
+to pairs of points `x` of `X` and embeddings `κ(x) ⟶ K`. -/
+def SpecToEquivOfField (K : Type u) [Field K] (X : Scheme.{u}) :
+    (Spec (.of K) ⟶ X) ≃ Σ x, X.residueField x ⟶ .of K where
+  toFun f :=
+    ⟨_, X.descResidueField (Scheme.stalkClosedPointTo f)⟩
+  invFun xf := Spec.map xf.2 ≫ X.fromSpecResidueField xf.1
+  left_inv := Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField K X
+  right_inv f := by
+    rw [SpecToEquivOfField_eq_iff]
+    simp only [CommRingCat.coe_of, Scheme.comp_coeBase, TopCat.coe_comp, Function.comp_apply,
+      Scheme.fromSpecResidueField_apply, exists_true_left]
+    rw [← Spec.map_inj, Spec.map_comp, ← cancel_mono (X.fromSpecResidueField _)]
+    erw [Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField]
+    simp
+
 end Scheme
 
 end AlgebraicGeometry
diff --git a/Mathlib/AlgebraicGeometry/Stalk.lean b/Mathlib/AlgebraicGeometry/Stalk.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang, Fangming Li
 -/
 import Mathlib.AlgebraicGeometry.AffineScheme
+import Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
 
 /-!
 # Stalks of a Scheme
@@ -68,6 +69,19 @@ noncomputable def Scheme.fromSpecStalk (X : Scheme) (x : X) :
 theorem IsAffineOpen.fromSpecStalk_eq_fromSpecStalk {x : X} (hxU : x ∈ U) :
     hU.fromSpecStalk hxU = X.fromSpecStalk x := fromSpecStalk_eq ..
 
+instance IsAffineOpen.fromSpecStalk_isPreimmersion {X : Scheme.{u}} {U : Opens X}
+    (hU : IsAffineOpen U) (x : X) (hx : x ∈ U) : IsPreimmersion (hU.fromSpecStalk hx) := by
+  dsimp [IsAffineOpen.fromSpecStalk]
+  haveI : IsPreimmersion (Spec.map (X.presheaf.germ U x hx)) :=
+    letI : Algebra Γ(X, U) (X.presheaf.stalk x) := (X.presheaf.germ U x hx).toAlgebra
+    haveI := hU.isLocalization_stalk ⟨x, hx⟩
+    IsPreimmersion.of_isLocalization (R := Γ(X, U)) (S := X.presheaf.stalk x)
+      (hU.primeIdealOf ⟨x, hx⟩).asIdeal.primeCompl
+  apply IsPreimmersion.comp
+
+instance {X : Scheme.{u}} (x : X) : IsPreimmersion (X.fromSpecStalk x) :=
+  IsAffineOpen.fromSpecStalk_isPreimmersion _ _ _
+
 lemma IsAffineOpen.fromSpecStalk_closedPoint {U : Opens X} (hU : IsAffineOpen U)
     {x : X} (hxU : x ∈ U) :
     (hU.fromSpecStalk hxU).base (closedPoint (X.presheaf.stalk x)) = x := by
@@ -184,7 +198,6 @@ section stalkClosedPointTo
 
 variable {R} (f : Spec R ⟶ X)
 
-
 namespace Scheme
 
 /--