From 1a4c6bcc621d0b5f485d6121d26937525a458c54 Mon Sep 17 00:00:00 2001 From: Andrew Yang Date: Thu, 3 Oct 2024 17:24:54 +0000 Subject: [PATCH] feat(AlgebraicGeometry): Residue fields of schemes. (#15333) --- Mathlib.lean | 1 + Mathlib/AlgebraicGeometry/ResidueField.lean | 180 ++++++++++++++++++++ 2 files changed, 181 insertions(+) create mode 100644 Mathlib/AlgebraicGeometry/ResidueField.lean diff --git a/Mathlib.lean b/Mathlib.lean index 22ea50c9663f9..038ecf2264b60 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/AlgebraicGeometry/ResidueField.lean b/Mathlib/AlgebraicGeometry/ResidueField.lean new file mode 100644 index 0000000000000..f192506ed485b --- /dev/null +++ b/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