-
Notifications
You must be signed in to change notification settings - Fork 314
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(AlgebraicGeometry): Residue fields of schemes. #15333
Closed
+181
−0
Closed
Changes from 2 commits
Commits
Show all changes
4 commits
Select commit
Hold shift + click to select a range
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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.LocallyRingedSpace` 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' (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 |
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is it
AlgebraicGeometry.LocallyRingedSpace
orAlgebraicGeometry.Scheme
?