feat(AlgebraicGeometry): Residue fields of schemes. (#15333)

Mathlib.lean

@@ -874,6 +874,7 @@ import Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
 import Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
 import Mathlib.AlgebraicGeometry.Properties
 import Mathlib.AlgebraicGeometry.Pullbacks
+import Mathlib.AlgebraicGeometry.ResidueField
 import Mathlib.AlgebraicGeometry.Restrict
 import Mathlib.AlgebraicGeometry.Scheme
 import Mathlib.AlgebraicGeometry.Sites.BigZariski

Mathlib/AlgebraicGeometry/ResidueField.lean

@@ -0,0 +1,180 @@
+/-
+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
+
+/-!
+
+# Residue fields of points
+
+## Main definitions
+
+The following are in the `AlgebraicGeometry.Scheme` namespace:
+
+- `AlgebraicGeometry.Scheme.residueField`: The residue field of the stalk at `x`.
+- `AlgebraicGeometry.Scheme.evaluation`: For open subsets `U` of `X` containing `x`,
+  the evaluation map from sections over `U` to the residue field at `x`.
+- `AlgebraicGeometry.Scheme.Hom.residueFieldMap`: A morphism of schemes induce a homomorphism of
+  residue fields.
+- `AlgebraicGeometry.Scheme.fromSpecResidueField`: The canonical map `Spec κ(x) ⟶ X`.
+
+-/
+
+universe u
+
+open CategoryTheory TopologicalSpace Opposite
+
+noncomputable section
+
+namespace AlgebraicGeometry.Scheme
+
+variable (X : Scheme.{u}) {U : X.Opens}
+
+/-- The residue field of `X` at a point `x` is the residue field of the stalk of `X`
+at `x`. -/
+def residueField (x : X) : CommRingCat :=
+  CommRingCat.of <| LocalRing.ResidueField (X.presheaf.stalk x)
+
+instance (x : X) : Field (X.residueField x) :=
+  inferInstanceAs <| Field (LocalRing.ResidueField (X.presheaf.stalk x))
+
+/-- The residue map from the stalk to the residue field. -/
+def residue (X : Scheme.{u}) (x) : X.presheaf.stalk x ⟶ X.residueField x :=
+  LocalRing.residue _
+
+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 `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`.
+
+If we interpret sections over `U` as functions of `X` defined on `U`, then this ring map
+corresponds to evaluation at `x`.
+-/
+def evaluation (U : X.Opens) (x : X) (hx : x ∈ U) : Γ(X, U) ⟶ X.residueField x :=
+  X.presheaf.germ ⟨x, hx⟩ ≫ X.residue _
+
+@[reassoc]
+lemma germ_residue (x : U) : X.presheaf.germ x ≫ X.residue x.1 = X.evaluation U x x.2 := rfl
+
+/-- The global evaluation map from `Γ(X, ⊤)` to the residue field at `x`. -/
+abbrev Γevaluation (x : X) : Γ(X, ⊤) ⟶ X.residueField x :=
+  X.evaluation ⊤ x trivial
+
+@[simp]
+lemma evaluation_eq_zero_iff_not_mem_basicOpen (x : X) (hx : x ∈ U) (f : Γ(X, U)) :
+    X.evaluation U x hx f = 0 ↔ x ∉ X.basicOpen f :=
+  X.toLocallyRingedSpace.evaluation_eq_zero_iff_not_mem_basicOpen ⟨x, hx⟩ f
+
+lemma evaluation_ne_zero_iff_mem_basicOpen (x : X) (hx : x ∈ U) (f : Γ(X, U)) :
+    X.evaluation U x hx f ≠ 0 ↔ x ∈ X.basicOpen f := by
+  simp
+
+variable {X Y : Scheme.{u}} (f : X ⟶ Y)
+
+instance (x) : IsLocalRingHom (f.stalkMap x) := inferInstanceAs (IsLocalRingHom (f.val.stalkMap x))
+
+/-- If `X ⟶ Y` is a morphism of locally ringed spaces and `x` a point of `X`, we obtain
+a morphism of residue fields in the other direction. -/
+def Hom.residueFieldMap (f : X.Hom Y) (x : X) :
+    Y.residueField (f.val.base x) ⟶ X.residueField x :=
+  LocalRing.ResidueField.map (f.stalkMap x)
+
+@[reassoc]
+lemma residue_residueFieldMap (x : X) :
+    Y.residue (f.val.base x) ≫ f.residueFieldMap x = f.stalkMap x ≫ X.residue x := by
+  simp [Hom.residueFieldMap]
+  rfl
+
+@[simp]
+lemma residueFieldMap_id (x : X) :
+    Hom.residueFieldMap (𝟙 X) x = 𝟙 (X.residueField x) :=
+  LocallyRingedSpace.residueFieldMap_id _
+
+@[simp]
+lemma residueFieldMap_comp {Z : Scheme.{u}} (g : Y ⟶ Z) (x : X) :
+    (f ≫ g).residueFieldMap x = g.residueFieldMap (f.val.base x) ≫ f.residueFieldMap x :=
+  LocallyRingedSpace.residueFieldMap_comp _ _ _
+
+@[reassoc]
+lemma evaluation_naturality {V : Opens Y} (x : X) (hx : f.val.base x ∈ V) :
+    Y.evaluation V (f.val.base x) hx ≫ f.residueFieldMap x =
+      f.app V ≫ X.evaluation (f ⁻¹ᵁ V) x hx :=
+  LocallyRingedSpace.evaluation_naturality f ⟨x, hx⟩
+
+lemma evaluation_naturality_apply {V : Opens Y} (x : X) (hx : f.val.base x ∈ V) (s) :
+    f.residueFieldMap x (Y.evaluation V (f.val.base x) hx s) =
+      X.evaluation (f ⁻¹ᵁ V) x hx (f.app V s) :=
+  LocallyRingedSpace.evaluation_naturality_apply f ⟨x, hx⟩ s
+
+instance [IsOpenImmersion f] (x) : IsIso (f.residueFieldMap x) :=
+  (LocalRing.ResidueField.mapEquiv
+    (asIso (f.stalkMap x)).commRingCatIsoToRingEquiv).toCommRingCatIso.isIso_hom
+
+section congr
+
+-- replace this def if hard to work with
+/-- The isomorphism between residue fields of equal points. -/
+def residueFieldCongr {x y : X} (h : x = y) :
+    X.residueField x ≅ X.residueField y :=
+  eqToIso (by subst h; rfl)
+
+@[simp]
+lemma residueFieldCongr_refl {x : X} :
+    X.residueFieldCongr (refl x) = Iso.refl _ := rfl
+
+@[simp]
+lemma residueFieldCongr_symm {x y : X} (e : x = y) :
+    (X.residueFieldCongr e).symm = X.residueFieldCongr e.symm := rfl
+
+@[simp]
+lemma residueFieldCongr_inv {x y : X} (e : x = y) :
+    (X.residueFieldCongr e).inv = (X.residueFieldCongr e.symm).hom := rfl
+
+@[simp]
+lemma residueFieldCongr_trans {x y z : X} (e : x = y) (e' : y = z) :
+    X.residueFieldCongr e ≪≫ X.residueFieldCongr e' = X.residueFieldCongr (e.trans e') := by
+  subst e e'
+  rfl
+
+@[reassoc (attr := simp)]
+lemma residueFieldCongr_trans_hom (X : Scheme) {x y z : X} (e : x = y) (e' : y = z) :
+    (X.residueFieldCongr e).hom ≫ (X.residueFieldCongr e').hom =
+      (X.residueFieldCongr (e.trans e')).hom := by
+  subst e e'
+  rfl
+
+@[reassoc]
+lemma residue_residueFieldCongr (X : Scheme) {x y : X} (h : x = y) :
+    X.residue x ≫ (X.residueFieldCongr h).hom =
+      (X.presheaf.stalkCongr (.of_eq h)).hom ≫ X.residue y := by
+  subst h
+  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
+
+@[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
+
+end fromResidueField
+
+end Scheme
+
+end AlgebraicGeometry