Residue fields of points

Any point x of a locally ringed space X comes with a natural residue field, namely the residue field of the stalk at x. Moreover, for every open subset of X containing x, we have a canonical evaluation map from Γ(X, U) to the residue field of X at x.

Main definitions

The following are in the AlgebraicGeometry.LocallyRingedSpace namespace:

• residueField: the residue field of the stalk at x.
• evaluation: for open subsets U of X containing x, the evaluation map from sections over U to the residue field at x.
• evaluationMap: a morphism of locally ringed spaces induces a morphism, i.e. extension, of residue fields.

def AlgebraicGeometry.LocallyRingedSpace.residueField (X : LocallyRingedSpace) (x : ↑X.toTopCat) : CommRingCat

The residue field of X at a point x is the residue field of the stalk of X at x.

Equations

• X.residueField x = CommRingCat.of (IsLocalRing.ResidueField ↑(X.presheaf.stalk x))

instance AlgebraicGeometry.LocallyRingedSpace.instFieldCarrierResidueField (X : LocallyRingedSpace) (x : ↑X.toTopCat) : Field ↑(X.residueField x)

Equations

• X.instFieldCarrierResidueField x = inferInstanceAs (Field (IsLocalRing.ResidueField ↑(X.presheaf.stalk x)))

def AlgebraicGeometry.LocallyRingedSpace.evaluation (X : LocallyRingedSpace) {U : TopologicalSpace.Opens ↑X.toTopCat} (x : ↥U) : X.presheaf.obj (Opposite.op U) ⟶ X.residueField ↑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.

Equations

• X.evaluation x = CategoryTheory.CategoryStruct.comp (X.presheaf.germ U ↑x ⋯) (CommRingCat.ofHom (IsLocalRing.residue ↑(X.presheaf.stalk ↑x)))

def AlgebraicGeometry.LocallyRingedSpace.Γevaluation (X : LocallyRingedSpace) (x : ↑X.toTopCat) : X.presheaf.obj (Opposite.op ⊤) ⟶ X.residueField x

The global evaluation map from Γ(X, ⊤) to the residue field at x.

Equations

• X.Γevaluation x = X.evaluation ⟨x, ⋯⟩

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.evaluation_eq_zero_iff_notMem_basicOpen (X : LocallyRingedSpace) {U : TopologicalSpace.Opens ↑X.toTopCat} (x : ↥U) (f : ↑(X.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (X.evaluation x)) f = 0 ↔ ↑x ∉ X.toRingedSpace.basicOpen f

@[deprecated AlgebraicGeometry.LocallyRingedSpace.evaluation_eq_zero_iff_notMem_basicOpen (since := "2025-05-23")]

theorem AlgebraicGeometry.LocallyRingedSpace.evaluation_eq_zero_iff_not_mem_basicOpen (X : LocallyRingedSpace) {U : TopologicalSpace.Opens ↑X.toTopCat} (x : ↥U) (f : ↑(X.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (X.evaluation x)) f = 0 ↔ ↑x ∉ X.toRingedSpace.basicOpen f

Alias of AlgebraicGeometry.LocallyRingedSpace.evaluation_eq_zero_iff_notMem_basicOpen.

theorem AlgebraicGeometry.LocallyRingedSpace.evaluation_ne_zero_iff_mem_basicOpen (X : LocallyRingedSpace) {U : TopologicalSpace.Opens ↑X.toTopCat} (x : ↥U) (f : ↑(X.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (X.evaluation x)) f ≠ 0 ↔ ↑x ∈ X.toRingedSpace.basicOpen f

theorem AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_iff_forall_evaluation_eq_zero (X : LocallyRingedSpace) {U : TopologicalSpace.Opens ↑X.toTopCat} (f : ↑(X.presheaf.obj (Opposite.op U))) : X.toRingedSpace.basicOpen f = ⊥ ↔ ∀ (x : ↥U), (CategoryTheory.ConcreteCategory.hom (X.evaluation x)) f = 0

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.Γevaluation_eq_zero_iff_notMem_basicOpen (X : LocallyRingedSpace) (x : ↑X.toTopCat) (f : ↑(X.presheaf.obj (Opposite.op ⊤))) : (CategoryTheory.ConcreteCategory.hom (X.Γevaluation x)) f = 0 ↔ x ∉ X.toRingedSpace.basicOpen f

@[deprecated AlgebraicGeometry.LocallyRingedSpace.Γevaluation_eq_zero_iff_notMem_basicOpen (since := "2025-05-23")]

theorem AlgebraicGeometry.LocallyRingedSpace.Γevaluation_eq_zero_iff_not_mem_basicOpen (X : LocallyRingedSpace) (x : ↑X.toTopCat) (f : ↑(X.presheaf.obj (Opposite.op ⊤))) : (CategoryTheory.ConcreteCategory.hom (X.Γevaluation x)) f = 0 ↔ x ∉ X.toRingedSpace.basicOpen f

Alias of AlgebraicGeometry.LocallyRingedSpace.Γevaluation_eq_zero_iff_notMem_basicOpen.

theorem AlgebraicGeometry.LocallyRingedSpace.Γevaluation_ne_zero_iff_mem_basicOpen (X : LocallyRingedSpace) (x : ↑X.toTopCat) (f : ↑(X.presheaf.obj (Opposite.op ⊤))) : (CategoryTheory.ConcreteCategory.hom (X.Γevaluation x)) f ≠ 0 ↔ x ∈ X.toRingedSpace.basicOpen f

def AlgebraicGeometry.LocallyRingedSpace.residueFieldMap {X Y : LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) : Y.residueField ((CategoryTheory.ConcreteCategory.hom f.base) x) ⟶ X.residueField 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.

Equations

• AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f x = CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x)))

theorem AlgebraicGeometry.LocallyRingedSpace.residue_comp_residueFieldMap_eq_stalkMap_comp_residue {X Y : LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) : CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (IsLocalRing.residue ↑(Y.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom f.base) x)))) (residueFieldMap f x) = CategoryTheory.CategoryStruct.comp (Hom.stalkMap f x) (CommRingCat.ofHom (IsLocalRing.residue ↑(X.presheaf.stalk x)))

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.residueFieldMap_id {X : LocallyRingedSpace} (x : ↑X.toTopCat) : residueFieldMap (CategoryTheory.CategoryStruct.id X) x = CategoryTheory.CategoryStruct.id (X.residueField x)

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.residueFieldMap_comp {X Y : LocallyRingedSpace} (f : X ⟶ Y) {Z : LocallyRingedSpace} (g : Y ⟶ Z) (x : ↑X.toTopCat) : residueFieldMap (CategoryTheory.CategoryStruct.comp f g) x = CategoryTheory.CategoryStruct.comp (residueFieldMap g ((CategoryTheory.ConcreteCategory.hom f.base) x)) (residueFieldMap f x)

theorem AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality {X Y : LocallyRingedSpace} (f : X ⟶ Y) {V : TopologicalSpace.Opens ↑Y.toTopCat} (x : ↥((TopologicalSpace.Opens.map f.base).obj V)) : CategoryTheory.CategoryStruct.comp (Y.evaluation ⟨(CategoryTheory.ConcreteCategory.hom f.base) ↑x, ⋯⟩) (residueFieldMap f ↑x) = CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op V)) (X.evaluation x)

theorem AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_assoc {X Y : LocallyRingedSpace} (f : X ⟶ Y) {V : TopologicalSpace.Opens ↑Y.toTopCat} (x : ↥((TopologicalSpace.Opens.map f.base).obj V)) {Z : CommRingCat} (h : X.residueField ↑x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.evaluation ⟨(CategoryTheory.ConcreteCategory.hom f.base) ↑x, ⋯⟩) (CategoryTheory.CategoryStruct.comp (residueFieldMap f ↑x) h) = CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op V)) (CategoryTheory.CategoryStruct.comp (X.evaluation x) h)

theorem AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply {X Y : LocallyRingedSpace} (f : X ⟶ Y) {V : TopologicalSpace.Opens ↑Y.toTopCat} (x : ↥((TopologicalSpace.Opens.map f.base).obj V)) (a : ↑(Y.presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (residueFieldMap f ↑x)) ((CategoryTheory.ConcreteCategory.hom (Y.evaluation ⟨(CategoryTheory.ConcreteCategory.hom f.base) ↑x, ⋯⟩)) a) = (CategoryTheory.ConcreteCategory.hom (X.evaluation x)) ((CategoryTheory.ConcreteCategory.hom (f.c.app (Opposite.op V))) a)

theorem AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality {X Y : LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) : CategoryTheory.CategoryStruct.comp (Y.Γevaluation ((CategoryTheory.ConcreteCategory.hom f.base) x)) (residueFieldMap f x) = CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op ⊤)) (X.Γevaluation x)

theorem AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_assoc {X Y : LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) {Z : CommRingCat} (h : X.residueField x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.Γevaluation ((CategoryTheory.ConcreteCategory.hom f.base) x)) (CategoryTheory.CategoryStruct.comp (residueFieldMap f x) h) = CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op ⊤)) (CategoryTheory.CategoryStruct.comp (X.Γevaluation x) h)

theorem AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply {X Y : LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) (a : ↑(Y.presheaf.obj (Opposite.op ⊤))) : (CategoryTheory.ConcreteCategory.hom (residueFieldMap f x)) ((CategoryTheory.ConcreteCategory.hom (Y.Γevaluation ((CategoryTheory.ConcreteCategory.hom f.base) x))) a) = (CategoryTheory.ConcreteCategory.hom (X.Γevaluation x)) ((CategoryTheory.ConcreteCategory.hom (f.c.app (Opposite.op ⊤))) a)