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 : AlgebraicGeometry.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 : AlgebraicGeometry.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 : AlgebraicGeometry.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 : AlgebraicGeometry.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_not_mem_basicOpen (X : AlgebraicGeometry.LocallyRingedSpace) {U : TopologicalSpace.Opens ↑X.toTopCat} (x : ↥U) (f : ↑(X.presheaf.obj (Opposite.op U))) : (X.evaluation x).hom f = 0 ↔ ↑x ∉ X.toRingedSpace.basicOpen f

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

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

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

theorem AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_assoc {X Y : AlgebraicGeometry.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 ⟨f.base ↑x, ⋯⟩) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.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 : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) {V : TopologicalSpace.Opens ↑Y.toTopCat} (x : ↥((TopologicalSpace.Opens.map f.base).obj V)) (a : ↑(Y.presheaf.obj (Opposite.op V))) : (AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f ↑x).hom ((Y.evaluation ⟨f.base ↑x, ⋯⟩).hom a) = (X.evaluation x).hom ((f.c.app (Opposite.op V)).hom a)

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

theorem AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_assoc {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) {Z : CommRingCat} (h : X.residueField x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.Γevaluation (f.base x)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.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 : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) (a : ↑(Y.presheaf.obj (Opposite.op ⊤))) : (AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f x).hom ((Y.Γevaluation (f.base x)).hom a) = (X.Γevaluation x).hom ((f.c.app (Opposite.op ⊤)).hom a)