feat(AlgebraicGeometry): Classification of Spec R ⟶ X with R loca…

…l. (#15240)

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

Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

@@ -647,6 +647,10 @@ theorem closedPoint_mem_iff (U : TopologicalSpace.Opens <| PrimeSpectrum R) :
   · rintro rfl
     trivial
 
+lemma closed_point_mem_iff {U : TopologicalSpace.Opens (PrimeSpectrum R)} :
+    closedPoint R ∈ U ↔ U = ⊤ :=
+  ⟨(eq_top_iff.mpr fun x _ ↦ (specializes_closedPoint x).mem_open U.2 ·), (· ▸ trivial)⟩
+
 @[simp]
 theorem PrimeSpectrum.comap_residue (T : Type u) [CommRing T] [LocalRing T]
     (x : PrimeSpectrum (ResidueField T)) : PrimeSpectrum.comap (residue T) x = closedPoint T := by

Mathlib/AlgebraicGeometry/Scheme.lean

@@ -709,4 +709,15 @@ end Scheme
 
 end Stalks
 
+section LocalRing
+
+open LocalRing
+
+@[simp]
+lemma Spec_closedPoint {R S : CommRingCat} [LocalRing R] [LocalRing S]
+    {f : R ⟶ S} [IsLocalRingHom f] : (Spec.map f).base (closedPoint S) = closedPoint R :=
+  LocalRing.comap_closedPoint f
+
+end LocalRing
+
 end AlgebraicGeometry

Mathlib/AlgebraicGeometry/Stalk.lean

@@ -8,14 +8,25 @@ import Mathlib.AlgebraicGeometry.AffineScheme
 /-!
 # Stalks of a Scheme
 
-Given a scheme `X` and a point `x : X`, `AlgebraicGeometry.Scheme.fromSpecStalk X x` is the
-canonical scheme morphism from `Spec(O_x)` to `X`. This is helpful for constructing the canonical
-map from the spectrum of the residue field of a point to the original scheme.
+## Main definitions and results
+
+- `AlgebraicGeometry.Scheme.fromSpecStalk`: The canonical morphism `Spec 𝒪_{X, x} ⟶ X`.
+- `AlgebraicGeometry.Scheme.range_fromSpecStalk`: The range of the map `Spec 𝒪_{X, x} ⟶ X` is
+  exactly the `y`s that specialize to `x`.
+- `AlgebraicGeometry.SpecToEquivOfLocalRing`:
+  Given a local ring `R` and scheme `X`, morphisms `Spec R ⟶ X` corresponds to pairs
+  `(x, f)` where `x : X` and `f : 𝒪_{X, x} ⟶ R` is a local ring homomorphism.
 -/
 
 namespace AlgebraicGeometry
 
-open CategoryTheory Opposite TopologicalSpace
+open CategoryTheory Opposite TopologicalSpace LocalRing
+
+universe u
+
+variable {X Y : Scheme.{u}} (f : X ⟶ Y) {U V : X.Opens} (hU : IsAffineOpen U) (hV : IsAffineOpen V)
+
+section fromSpecStalk
 
 /--
 A morphism from `Spec(O_x)` to `X`, which is defined with the help of an affine open
@@ -30,8 +41,7 @@ noncomputable def IsAffineOpen.fromSpecStalk
 The morphism from `Spec(O_x)` to `X` given by `IsAffineOpen.fromSpec` does not depend on the affine
 open neighborhood of `x` we choose.
 -/
-theorem IsAffineOpen.fromSpecStalk_eq {X : Scheme} (x : X) {U V : X.Opens}
-    (hU : IsAffineOpen U) (hV : IsAffineOpen V) (hxU : x ∈ U) (hxV : x ∈ V) :
+theorem IsAffineOpen.fromSpecStalk_eq (x : X) (hxU : x ∈ U) (hxV : x ∈ V) :
     hU.fromSpecStalk hxU = hV.fromSpecStalk hxV := by
   obtain ⟨U', h₁, h₂, h₃ : U' ≤ U ⊓ V⟩ :=
     Opens.isBasis_iff_nbhd.mp (isBasis_affine_open X) (show x ∈ U ⊓ V from ⟨hxU, hxV⟩)
@@ -51,12 +61,254 @@ theorem IsAffineOpen.fromSpecStalk_eq {X : Scheme} (x : X) {U V : X.Opens}
 If `x` is a point of `X`, this is the canonical morphism from `Spec(O_x)` to `X`.
 -/
 noncomputable def Scheme.fromSpecStalk (X : Scheme) (x : X) :
-    Scheme.Spec.obj (op (X.presheaf.stalk x)) ⟶ X :=
+    Spec (X.presheaf.stalk x) ⟶ X :=
   (isAffineOpen_opensRange (X.affineOpenCover.map x)).fromSpecStalk (X.affineOpenCover.covers x)
 
 @[simp]
-theorem IsAffineOpen.fromSpecStalk_eq_fromSpecStalk
-    {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) {x : X} (hxU : x ∈ U) :
+theorem IsAffineOpen.fromSpecStalk_eq_fromSpecStalk {x : X} (hxU : x ∈ U) :
     hU.fromSpecStalk hxU = X.fromSpecStalk x := fromSpecStalk_eq ..
 
+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
+  rw [IsAffineOpen.fromSpecStalk, Scheme.comp_base_apply]
+  rw [← hU.primeIdealOf_eq_map_closedPoint ⟨x, hxU⟩, hU.fromSpec_primeIdealOf ⟨x, hxU⟩]
+
+namespace Scheme
+
+@[simp]
+lemma fromSpecStalk_closedPoint {x : X} :
+    (X.fromSpecStalk x).base (closedPoint (X.presheaf.stalk x)) = x :=
+  IsAffineOpen.fromSpecStalk_closedPoint _ _
+
+lemma fromSpecStalk_app {x : X} (hxU : x ∈ U) :
+    (X.fromSpecStalk x).app U =
+      X.presheaf.germ U x hxU ≫
+        (ΓSpecIso (X.presheaf.stalk x)).inv ≫
+          (Spec (X.presheaf.stalk x)).presheaf.map (homOfLE le_top).op := by
+  obtain ⟨_, ⟨V : X.Opens, hV, rfl⟩, hxV, hVU⟩ := (isBasis_affine_open X).exists_subset_of_mem_open
+    hxU U.2
+  rw [← hV.fromSpecStalk_eq_fromSpecStalk hxV, IsAffineOpen.fromSpecStalk, Scheme.comp_app,
+    hV.fromSpec_app_of_le _ hVU, ← X.presheaf.germ_res (homOfLE hVU) x hxV]
+  simp [Category.assoc, ← ΓSpecIso_inv_naturality_assoc]
+
+@[reassoc]
+lemma Spec_map_stalkSpecializes_fromSpecStalk {x y : X} (h : x ⤳ y) :
+    Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x := by
+  obtain ⟨_, ⟨U, hU, rfl⟩, hyU, -⟩ :=
+    (isBasis_affine_open X).exists_subset_of_mem_open (Set.mem_univ y) isOpen_univ
+  have hxU : x ∈ U := h.mem_open U.2 hyU
+  rw [← hU.fromSpecStalk_eq_fromSpecStalk hyU, ← hU.fromSpecStalk_eq_fromSpecStalk hxU,
+    IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpecStalk, ← Category.assoc, ← Spec.map_comp,
+    TopCat.Presheaf.germ_stalkSpecializes]
+
+@[reassoc (attr := simp)]
+lemma Spec_map_stalkMap_fromSpecStalk {x} :
+    Spec.map (f.stalkMap x) ≫ Y.fromSpecStalk _ = X.fromSpecStalk x ≫ f := by
+  obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := (isBasis_affine_open Y).exists_subset_of_mem_open
+    (Set.mem_univ (f.base x)) isOpen_univ
+  obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := (isBasis_affine_open X).exists_subset_of_mem_open
+    hxU (f ⁻¹ᵁ U).2
+  rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, ← hV.fromSpecStalk_eq_fromSpecStalk hxV,
+    IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc, Scheme.stalkMap_germ f _ x hxU,
+    IsAffineOpen.fromSpecStalk, Spec.map_comp_assoc, ← X.presheaf.germ_res (homOfLE hVU) x hxV,
+    Spec.map_comp_assoc, Category.assoc, ← Spec.map_comp_assoc (f.app _),
+      Hom.app_eq_appLE, Hom.appLE_map, IsAffineOpen.Spec_map_appLE_fromSpec]
+
+lemma Spec_fromSpecStalk (R : CommRingCat) (x) :
+    (Spec R).fromSpecStalk x =
+      Spec.map ((ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial) := by
+  rw [← (isAffineOpen_top (Spec R)).fromSpecStalk_eq_fromSpecStalk (x := x) trivial,
+    IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpec_top, isoSpec_Spec_inv,
+    ← Spec.map_comp]
+
+-- This is not a simp lemma to respect the abstraction boundaries
+/-- A variant of `Spec_fromSpecStalk` that breaks abstraction boundaries. -/
+lemma Spec_fromSpecStalk' (R : CommRingCat) (x) :
+    (Spec R).fromSpecStalk x = Spec.map (StructureSheaf.toStalk R _) :=
+  Spec_fromSpecStalk _ _
+
+@[stacks 01J7]
+lemma range_fromSpecStalk {x : X} :
+    Set.range (X.fromSpecStalk x).base = { y | y ⤳ x } := by
+  ext y
+  constructor
+  · rintro ⟨y, rfl⟩
+    exact ((LocalRing.specializes_closedPoint y).map (X.fromSpecStalk x).base.2).trans
+      (specializes_of_eq fromSpecStalk_closedPoint)
+  · rintro (hy : y ⤳ x)
+    have := fromSpecStalk_closedPoint (x := y)
+    rw [← Spec_map_stalkSpecializes_fromSpecStalk hy] at this
+    exact ⟨_, this⟩
+
+end Scheme
+
+end fromSpecStalk
+
+variable (R : CommRingCat.{u}) [LocalRing R]
+
+section stalkClosedPointIso
+
+/-- For a local ring `(R, 𝔪)`,
+this is the isomorphism between the stalk of `Spec R` at `𝔪` and `R`. -/
+noncomputable
+def stalkClosedPointIso :
+    (Spec R).presheaf.stalk (closedPoint R) ≅ R :=
+  StructureSheaf.stalkIso _ _ ≪≫ (IsLocalization.atUnits R
+      (closedPoint R).asIdeal.primeCompl fun _ ↦ not_not.mp).toRingEquiv.toCommRingCatIso.symm
+
+lemma stalkClosedPointIso_inv :
+    (stalkClosedPointIso R).inv = StructureSheaf.toStalk R _ := by
+  ext x
+  exact StructureSheaf.localizationToStalk_of _ _ _
+
+lemma ΓSpecIso_hom_stalkClosedPointIso_inv :
+    (Scheme.ΓSpecIso R).hom ≫ (stalkClosedPointIso R).inv =
+      (Spec R).presheaf.germ ⊤ (closedPoint _) trivial := by
+  rw [stalkClosedPointIso_inv, ← Iso.eq_inv_comp]
+  rfl
+
+@[reassoc (attr := simp)]
+lemma germ_stalkClosedPointIso_hom :
+    (Spec R).presheaf.germ ⊤ (closedPoint _) trivial ≫ (stalkClosedPointIso R).hom =
+      (Scheme.ΓSpecIso R).hom := by
+  rw [← ΓSpecIso_hom_stalkClosedPointIso_inv, Category.assoc, Iso.inv_hom_id, Category.comp_id]
+
+lemma Spec_stalkClosedPointIso :
+    Spec.map (stalkClosedPointIso R).inv = (Spec R).fromSpecStalk (closedPoint R) := by
+  rw [stalkClosedPointIso_inv, Scheme.Spec_fromSpecStalk']
+
+end stalkClosedPointIso
+
+section stalkClosedPointTo
+
+variable {R} (f : Spec R ⟶ X)
+
+
+namespace Scheme
+
+/--
+Given a local ring `(R, 𝔪)` and a morphism `f : Spec R ⟶ X`,
+they induce a (local) ring homomorphism `φ : 𝒪_{X, f 𝔪} ⟶ R`.
+
+This is inverse to `φ ↦ Spec.map φ ≫ X.fromSpecStalk (f 𝔪)`. See `SpecToEquivOfLocalRing`.
+-/
+noncomputable
+def stalkClosedPointTo :
+    X.presheaf.stalk (f.base (closedPoint R)) ⟶ R :=
+  f.stalkMap (closedPoint R) ≫ (stalkClosedPointIso R).hom
+
+instance isLocalRingHom_stalkClosedPointTo :
+    IsLocalRingHom (stalkClosedPointTo f) := by
+  apply (config := { allowSynthFailures := true }) RingHom.isLocalRingHom_comp
+  · apply isLocalRingHom_of_iso
+  · apply f.prop
+
+lemma preimage_eq_top_of_closedPoint_mem
+    {U : Opens X} (hU : f.base (closedPoint R) ∈ U) : f ⁻¹ᵁ U = ⊤ :=
+  LocalRing.closed_point_mem_iff.mp hU
+
+lemma stalkClosedPointTo_comp (g : X ⟶ Y) :
+    stalkClosedPointTo (f ≫ g) = g.stalkMap _ ≫ stalkClosedPointTo f := by
+  rw [stalkClosedPointTo, Scheme.stalkMap_comp]
+  exact Category.assoc _ _ _
+
+lemma germ_stalkClosedPointTo_Spec {R S : CommRingCat} [LocalRing S] (φ : R ⟶ S):
+    (Spec R).presheaf.germ ⊤ _ trivial ≫ stalkClosedPointTo (Spec.map φ) =
+      (ΓSpecIso R).hom ≫ φ := by
+  rw [stalkClosedPointTo, Scheme.stalkMap_germ_assoc, ← Iso.inv_comp_eq,
+    ← ΓSpecIso_inv_naturality_assoc]
+  simp_rw [Opens.map_top]
+  rw [germ_stalkClosedPointIso_hom, Iso.inv_hom_id, Category.comp_id]
+
+@[reassoc]
+lemma germ_stalkClosedPointTo (U : Opens X) (hU : f.base (closedPoint R) ∈ U) :
+    X.presheaf.germ U _ hU ≫ stalkClosedPointTo f = f.app U ≫
+      ((Spec R).presheaf.mapIso (eqToIso (preimage_eq_top_of_closedPoint_mem f hU).symm).op ≪≫
+        ΓSpecIso R).hom := by
+  rw [stalkClosedPointTo, Scheme.stalkMap_germ_assoc, Iso.trans_hom]
+  congr 1
+  rw [← Iso.eq_comp_inv, Category.assoc, ΓSpecIso_hom_stalkClosedPointIso_inv]
+  simp only [TopCat.Presheaf.pushforward_obj_obj, Functor.mapIso_hom, Iso.op_hom, eqToIso.hom,
+    TopCat.Presheaf.germ_res]
+
+@[reassoc]
+lemma germ_stalkClosedPointTo_Spec_fromSpecStalk
+    {x : X} (f : X.presheaf.stalk x ⟶ R) [IsLocalRingHom f] (U : Opens X) (hU) :
+    X.presheaf.germ U _ hU ≫ stalkClosedPointTo (Spec.map f ≫ X.fromSpecStalk x) =
+      X.presheaf.germ U x (by simpa using hU) ≫ f := by
+  have : (Spec.map f ≫ X.fromSpecStalk x).base (closedPoint R) = x := by
+    rw [comp_base_apply, Spec_closedPoint, fromSpecStalk_closedPoint]
+  have : x ∈ U := this ▸ hU
+  simp only [TopCat.Presheaf.stalkCongr_hom, TopCat.Presheaf.germ_stalkSpecializes_assoc,
+    germ_stalkClosedPointTo, comp_app,
+    fromSpecStalk_app (X := X) (x := x) this, Category.assoc, Iso.trans_hom,
+    Functor.mapIso_hom, Hom.naturality_assoc, ← Functor.map_comp_assoc,
+    (Spec.map f).app_eq_appLE, Hom.appLE_map_assoc, Hom.map_appLE_assoc]
+  simp_rw [← Opens.map_top (Spec.map f).base]
+  rw [← (Spec.map f).app_eq_appLE, ΓSpecIso_naturality, Iso.inv_hom_id_assoc]
+
+lemma stalkClosedPointTo_fromSpecStalk (x : X) :
+    stalkClosedPointTo (X.fromSpecStalk x) =
+      (X.presheaf.stalkCongr (by rw [fromSpecStalk_closedPoint]; rfl)).hom := by
+  refine TopCat.Presheaf.stalk_hom_ext _ fun U hxU ↦ ?_
+  simp only [TopCat.Presheaf.stalkCongr_hom, TopCat.Presheaf.germ_stalkSpecializes, id_eq]
+  have : X.fromSpecStalk x = Spec.map (𝟙 (X.presheaf.stalk x)) ≫ X.fromSpecStalk x := by simp
+  convert germ_stalkClosedPointTo_Spec_fromSpecStalk (𝟙 (X.presheaf.stalk x)) U hxU
+
+@[reassoc]
+lemma Spec_stalkClosedPointTo_fromSpecStalk :
+    Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk _ = f := by
+  obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := (isBasis_affine_open X).exists_subset_of_mem_open
+    (Set.mem_univ (f.base (closedPoint R))) isOpen_univ
+  have := IsAffineOpen.Spec_map_appLE_fromSpec f hU (isAffineOpen_top _)
+    (preimage_eq_top_of_closedPoint_mem f hxU).ge
+  rw [IsAffineOpen.fromSpec_top, Iso.eq_inv_comp, isoSpec_Spec_hom] at this
+  rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc,
+    germ_stalkClosedPointTo]
+  simpa only [Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom, Category.assoc,
+    Hom.app_eq_appLE, Hom.appLE_map_assoc, Spec.map_comp_assoc]
+
+end Scheme
+
+end stalkClosedPointTo
+
+variable {R}
+
+omit [LocalRing R] in
+/-- useful lemma for applications of `SpecToEquivOfLocalRing` -/
+lemma SpecToEquivOfLocalRing_eq_iff
+    {f₁ f₂ : Σ x, { f : X.presheaf.stalk x ⟶ R // IsLocalRingHom f }} :
+    f₁ = f₂ ↔ ∃ h₁ : f₁.1 = f₂.1, f₁.2.1 =
+      (X.presheaf.stalkCongr (by rw [h₁]; rfl)).hom ≫ f₂.2.1 := by
+  constructor
+  · rintro rfl; simp
+  · obtain ⟨x₁, ⟨f₁, h₁⟩⟩ := f₁
+    obtain ⟨x₂, ⟨f₂, h₂⟩⟩ := f₂
+    rintro ⟨rfl : x₁ = x₂, e : f₁ = _⟩
+    simp [e]
+
+variable (X R)
+
+/--
+Given a local ring `R` and scheme `X`, morphisms `Spec R ⟶ X` corresponds to pairs
+`(x, f)` where `x : X` and `f : 𝒪_{X, x} ⟶ R` is a local ring homomorphism.
+-/
+@[simps]
+noncomputable
+def SpecToEquivOfLocalRing :
+    (Spec R ⟶ X) ≃ Σ x, { f : X.presheaf.stalk x ⟶ R // IsLocalRingHom f } where
+  toFun f := ⟨f.base (closedPoint R), Scheme.stalkClosedPointTo f, inferInstance⟩
+  invFun xf := Spec.map xf.2.1 ≫ X.fromSpecStalk xf.1
+  left_inv := Scheme.Spec_stalkClosedPointTo_fromSpecStalk
+  right_inv xf := by
+    obtain ⟨x, ⟨f, hf⟩⟩ := xf
+    symm
+    refine SpecToEquivOfLocalRing_eq_iff.mpr ⟨?_, ?_⟩
+    · simp only [Scheme.comp_coeBase, TopCat.coe_comp, Function.comp_apply, Spec_closedPoint,
+        Scheme.fromSpecStalk_closedPoint]
+    · refine TopCat.Presheaf.stalk_hom_ext _ fun U hxU ↦ ?_
+      simp only [Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk,
+        TopCat.Presheaf.stalkCongr_hom, TopCat.Presheaf.germ_stalkSpecializes_assoc]
+
 end AlgebraicGeometry