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.
• AlgebraicGeometry.Scheme.SpecToEquivOfField: morphisms Spec K ⟶ X for a field K correspond to pairs of x : X with embedding κ(x) ⟶ K.

def AlgebraicGeometry.Scheme.residueField (X : AlgebraicGeometry.Scheme) (x : ↑↑X.toPresheafedSpace) : 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 (LocalRing.ResidueField ↑(X.presheaf.stalk x))

instance AlgebraicGeometry.Scheme.instFieldαCommRingResidueField (X : AlgebraicGeometry.Scheme) (x : ↑↑X.toPresheafedSpace) : Field ↑(X.residueField x)

Equations

• X.instFieldαCommRingResidueField x = inferInstanceAs (Field (LocalRing.ResidueField ↑(X.presheaf.stalk x)))

def AlgebraicGeometry.Scheme.residue (X : AlgebraicGeometry.Scheme) (x : ↑↑X.toPresheafedSpace) : X.presheaf.stalk x ⟶ X.residueField x

The residue map from the stalk to the residue field.

Equations

• X.residue x = LocalRing.residue ↑(X.presheaf.stalk x)

instance AlgebraicGeometry.Scheme.instIsPreimmersionMapResidue {X : AlgebraicGeometry.Scheme} (x : ↑↑X.toPresheafedSpace) : AlgebraicGeometry.IsPreimmersion (AlgebraicGeometry.Spec.map (X.residue x))

See AlgebraicGeometry.IsClosedImmersion.Spec_map_residue for the stronger result that Spec.map (X.residue x) is a closed immersion.

Equations

• ⋯ = ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Spec_map_residue_apply {X : AlgebraicGeometry.Scheme} (x : ↑↑X.toPresheafedSpace) (s : ↑↑(AlgebraicGeometry.Spec (X.residueField x)).toPresheafedSpace) : (AlgebraicGeometry.Spec.map (X.residue x)).base s = LocalRing.closedPoint ↑(X.presheaf.stalk x)

theorem AlgebraicGeometry.Scheme.residue_surjective (X : AlgebraicGeometry.Scheme) (x : ↑↑X.toPresheafedSpace) : Function.Surjective ⇑(X.residue x)

instance AlgebraicGeometry.Scheme.instEpiCommRingCatResidue (X : AlgebraicGeometry.Scheme) (x : ↑↑X.toPresheafedSpace) : CategoryTheory.Epi (X.residue x)

Equations

• ⋯ = ⋯

def AlgebraicGeometry.Scheme.descResidueField {K : Type u} [Field K] {X : AlgebraicGeometry.Scheme} {x : ↑↑X.toPresheafedSpace} (f : X.presheaf.stalk x ⟶ CommRingCat.of K) [IsLocalHom f] : X.residueField x ⟶ CommRingCat.of K

If K is a field and f : 𝒪_{X, x} ⟶ K is a ring map, then this is the induced map κ(x) ⟶ K.

Equations

• AlgebraicGeometry.Scheme.descResidueField f = LocalRing.ResidueField.lift f

@[simp]

theorem AlgebraicGeometry.Scheme.residue_descResidueField {K : Type u} [Field K] {X : AlgebraicGeometry.Scheme} {x : ↑↑X.toPresheafedSpace} (f : X.presheaf.stalk x ⟶ CommRingCat.of K) [IsLocalHom f] : CategoryTheory.CategoryStruct.comp (X.residue x) (AlgebraicGeometry.Scheme.descResidueField f) = f

@[simp]

theorem AlgebraicGeometry.Scheme.residue_descResidueField_assoc {K : Type u} [Field K] {X : AlgebraicGeometry.Scheme} {x : ↑↑X.toPresheafedSpace} (f : X.presheaf.stalk x ⟶ CommRingCat.of K) [IsLocalHom f] {Z : CommRingCat} (h : CommRingCat.of K ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.residue x) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.descResidueField f) h) = CategoryTheory.CategoryStruct.comp f h

def AlgebraicGeometry.Scheme.evaluation (X : AlgebraicGeometry.Scheme) (U : X.Opens) (x : ↑↑X.toPresheafedSpace) (hx : 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 U x hx = CategoryTheory.CategoryStruct.comp (X.presheaf.germ U x hx) (X.residue x)

theorem AlgebraicGeometry.Scheme.germ_residue (X : AlgebraicGeometry.Scheme) {U : X.Opens} (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U) : CategoryTheory.CategoryStruct.comp (X.presheaf.germ U x hx) (X.residue x) = X.evaluation U x hx

theorem AlgebraicGeometry.Scheme.germ_residue_assoc (X : AlgebraicGeometry.Scheme) {U : X.Opens} (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U) {Z : CommRingCat} (h : X.residueField x ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.presheaf.germ U x hx) (CategoryTheory.CategoryStruct.comp (X.residue x) h) = CategoryTheory.CategoryStruct.comp (X.evaluation U x hx) h

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Γevaluation (X : AlgebraicGeometry.Scheme) (x : ↑↑X.toPresheafedSpace) : 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 trivial

@[simp]

theorem AlgebraicGeometry.Scheme.evaluation_eq_zero_iff_not_mem_basicOpen (X : AlgebraicGeometry.Scheme) {U : X.Opens} (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U) (f : ↑(X.presheaf.obj (Opposite.op U))) : (X.evaluation U x hx) f = 0 ↔ x ∉ X.basicOpen f

theorem AlgebraicGeometry.Scheme.evaluation_ne_zero_iff_mem_basicOpen (X : AlgebraicGeometry.Scheme) {U : X.Opens} (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U) (f : ↑(X.presheaf.obj (Opposite.op U))) : (X.evaluation U x hx) f ≠ 0 ↔ x ∈ X.basicOpen f

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

def AlgebraicGeometry.Scheme.Hom.residueFieldMap {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) (x : ↑↑X.toPresheafedSpace) : 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

• f.residueFieldMap x = LocalRing.ResidueField.map (f.stalkMap x)

theorem AlgebraicGeometry.Scheme.residue_residueFieldMap {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↑↑X.toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (Y.residue (f.base x)) (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap f x) (X.residue x)

theorem AlgebraicGeometry.Scheme.residue_residueFieldMap_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↑↑X.toPresheafedSpace) {Z : CommRingCat} (h : X.residueField x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.residue (f.base x)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap f x) (CategoryTheory.CategoryStruct.comp (X.residue x) h)

@[simp]

theorem AlgebraicGeometry.Scheme.residueFieldMap_id {X : AlgebraicGeometry.Scheme} (x : ↑↑X.toPresheafedSpace) : AlgebraicGeometry.Scheme.Hom.residueFieldMap (CategoryTheory.CategoryStruct.id X) x = CategoryTheory.CategoryStruct.id (X.residueField x)

@[simp]

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

theorem AlgebraicGeometry.Scheme.evaluation_naturality {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {V : Y.Opens} (x : ↑↑X.toPresheafedSpace) (hx : f.base x ∈ V) : CategoryTheory.CategoryStruct.comp (Y.evaluation V (f.base x) hx) (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f V) (X.evaluation ((TopologicalSpace.Opens.map f.base).obj V) x hx)

theorem AlgebraicGeometry.Scheme.evaluation_naturality_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {V : Y.Opens} (x : ↑↑X.toPresheafedSpace) (hx : f.base x ∈ V) {Z : CommRingCat} (h : X.residueField x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.evaluation V (f.base x) hx) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f V) (CategoryTheory.CategoryStruct.comp (X.evaluation ((TopologicalSpace.Opens.map f.base).obj V) x hx) h)

theorem AlgebraicGeometry.Scheme.evaluation_naturality_apply {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {V : Y.Opens} (x : ↑↑X.toPresheafedSpace) (hx : f.base x ∈ V) (s : ↑(Y.presheaf.obj (Opposite.op V))) : (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x) ((Y.evaluation V (f.base x) hx) s) = (X.evaluation ((TopologicalSpace.Opens.map f.base).obj V) x hx) ((AlgebraicGeometry.Scheme.Hom.app f V) s)

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

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

theorem AlgebraicGeometry.Scheme.Γevaluation_naturality_apply {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↑↑X.toPresheafedSpace) (a : ↑(Y.presheaf.obj (Opposite.op ⊤))) : (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x) ((Y.Γevaluation (f.base x)) a) = (X.Γevaluation x) ((f.c.app (Opposite.op ⊤)) a)

instance AlgebraicGeometry.Scheme.instIsIsoCommRingCatResidueFieldMapOfIsOpenImmersion {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (x : ↑↑X.toPresheafedSpace) : CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x)

Equations

• ⋯ = ⋯

def AlgebraicGeometry.Scheme.residueFieldCongr {X : AlgebraicGeometry.Scheme} {x : ↑↑X.toPresheafedSpace} {y : ↑↑X.toPresheafedSpace} (h : x = y) : X.residueField x ≅ X.residueField y

The isomorphism between residue fields of equal points.

Equations

• AlgebraicGeometry.Scheme.residueFieldCongr h = CategoryTheory.eqToIso ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.residueFieldCongr_refl {X : AlgebraicGeometry.Scheme} {x : ↑↑X.toPresheafedSpace} : AlgebraicGeometry.Scheme.residueFieldCongr ⋯ = CategoryTheory.Iso.refl (X.residueField x)

@[simp]

theorem AlgebraicGeometry.Scheme.residueFieldCongr_symm {X : AlgebraicGeometry.Scheme} {x : ↑↑X.toPresheafedSpace} {y : ↑↑X.toPresheafedSpace} (e : x = y) : (AlgebraicGeometry.Scheme.residueFieldCongr e).symm = AlgebraicGeometry.Scheme.residueFieldCongr ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.residueFieldCongr_inv {X : AlgebraicGeometry.Scheme} {x : ↑↑X.toPresheafedSpace} {y : ↑↑X.toPresheafedSpace} (e : x = y) : (AlgebraicGeometry.Scheme.residueFieldCongr e).inv = (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).hom

@[simp]

theorem AlgebraicGeometry.Scheme.residueFieldCongr_trans {X : AlgebraicGeometry.Scheme} {x : ↑↑X.toPresheafedSpace} {y : ↑↑X.toPresheafedSpace} {z : ↑↑X.toPresheafedSpace} (e : x = y) (e' : y = z) : AlgebraicGeometry.Scheme.residueFieldCongr e ≪≫ AlgebraicGeometry.Scheme.residueFieldCongr e' = AlgebraicGeometry.Scheme.residueFieldCongr ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.residueFieldCongr_trans_hom (X : AlgebraicGeometry.Scheme) {x : ↑↑X.toPresheafedSpace} {y : ↑↑X.toPresheafedSpace} {z : ↑↑X.toPresheafedSpace} (e : x = y) (e' : y = z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr e).hom (AlgebraicGeometry.Scheme.residueFieldCongr e').hom = (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).hom

@[simp]

theorem AlgebraicGeometry.Scheme.residueFieldCongr_trans_hom_assoc (X : AlgebraicGeometry.Scheme) {x : ↑↑X.toPresheafedSpace} {y : ↑↑X.toPresheafedSpace} {z : ↑↑X.toPresheafedSpace} (e : x = y) (e' : y = z) {Z : CommRingCat} (h : X.residueField z ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr e).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr e').hom h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).hom h

theorem AlgebraicGeometry.Scheme.residue_residueFieldCongr (X : AlgebraicGeometry.Scheme) {x : ↑↑X.toPresheafedSpace} {y : ↑↑X.toPresheafedSpace} (h : x = y) : CategoryTheory.CategoryStruct.comp (X.residue x) (AlgebraicGeometry.Scheme.residueFieldCongr h).hom = CategoryTheory.CategoryStruct.comp (X.presheaf.stalkCongr ⋯).hom (X.residue y)

theorem AlgebraicGeometry.Scheme.residue_residueFieldCongr_assoc (X : AlgebraicGeometry.Scheme) {x : ↑↑X.toPresheafedSpace} {y : ↑↑X.toPresheafedSpace} (h : x = y) {Z : CommRingCat} (h : X.residueField y ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.residue x) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr h✝).hom h) = CategoryTheory.CategoryStruct.comp (X.presheaf.stalkCongr ⋯).hom (CategoryTheory.CategoryStruct.comp (X.residue y) h)

theorem AlgebraicGeometry.Scheme.Hom.residueFieldMap_congr {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {g : X ⟶ Y} (e : f = g) (x : ↑↑X.toPresheafedSpace) : AlgebraicGeometry.Scheme.Hom.residueFieldMap f x = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).hom (AlgebraicGeometry.Scheme.Hom.residueFieldMap g x)

def AlgebraicGeometry.Scheme.fromSpecResidueField (X : AlgebraicGeometry.Scheme) (x : ↑↑X.toPresheafedSpace) : AlgebraicGeometry.Spec (X.residueField x) ⟶ X

The canonical map Spec κ(x) ⟶ X.

Equations

• X.fromSpecResidueField x = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.residue x)) (X.fromSpecStalk x)

instance AlgebraicGeometry.Scheme.instIsPreimmersionFromSpecResidueField {X : AlgebraicGeometry.Scheme} (x : ↑↑X.toPresheafedSpace) : AlgebraicGeometry.IsPreimmersion (X.fromSpecResidueField x)

Equations

• ⋯ = ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.residueFieldCongr_fromSpecResidueField {X : AlgebraicGeometry.Scheme} {x : ↑↑X.toPresheafedSpace} {y : ↑↑X.toPresheafedSpace} (h : x = y) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.residueFieldCongr h).hom) (X.fromSpecResidueField x) = X.fromSpecResidueField y

@[simp]

theorem AlgebraicGeometry.Scheme.residueFieldCongr_fromSpecResidueField_assoc {X : AlgebraicGeometry.Scheme} {x : ↑↑X.toPresheafedSpace} {y : ↑↑X.toPresheafedSpace} (h : x = y) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.residueFieldCongr h✝).hom) (CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) h) = CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField y) h

theorem AlgebraicGeometry.Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↑↑X.toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x)) (Y.fromSpecResidueField (f.base x)) = CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) f

theorem AlgebraicGeometry.Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↑↑X.toPresheafedSpace) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x)) (CategoryTheory.CategoryStruct.comp (Y.fromSpecResidueField (f.base x)) h) = CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) (CategoryTheory.CategoryStruct.comp f h)

@[simp]

theorem AlgebraicGeometry.Scheme.fromSpecResidueField_apply {X : AlgebraicGeometry.Scheme} (x : ↑↑X.toPresheafedSpace) (s : ↑↑(AlgebraicGeometry.Spec (X.residueField x)).toPresheafedSpace) : (X.fromSpecResidueField x).base s = x

theorem AlgebraicGeometry.Scheme.range_fromSpecResidueField {X : AlgebraicGeometry.Scheme} (x : ↑↑X.toPresheafedSpace) : Set.range ⇑(X.fromSpecResidueField x).base = {x}

theorem AlgebraicGeometry.Scheme.descResidueField_fromSpecResidueField {K : Type u_1} [Field K] (X : AlgebraicGeometry.Scheme) {x : ↑↑X.toPresheafedSpace} (f : X.presheaf.stalk x ⟶ CommRingCat.of K) [IsLocalHom f] : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.descResidueField f)) (X.fromSpecResidueField x) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) (X.fromSpecStalk x)

theorem AlgebraicGeometry.Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) (f : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.descResidueField (AlgebraicGeometry.Scheme.stalkClosedPointTo f))) (X.fromSpecResidueField (f.base (LocalRing.closedPoint K))) = f

theorem AlgebraicGeometry.Scheme.SpecToEquivOfField_eq_iff {K : Type u_1} [Field K] {X : AlgebraicGeometry.Scheme} {f₁ : (x : ↑↑X.toPresheafedSpace) × (X.residueField x ⟶ CommRingCat.of K)} {f₂ : (x : ↑↑X.toPresheafedSpace) × (X.residueField x ⟶ CommRingCat.of K)} : f₁ = f₂ ↔ ∃ (e : f₁.fst = f₂.fst), f₁.snd = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr e).hom f₂.snd

A helper lemma to work with AlgebraicGeometry.Scheme.SpecToEquivOfField.

def AlgebraicGeometry.Scheme.SpecToEquivOfField (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) : (AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X) ≃ (x : ↑↑X.toPresheafedSpace) × (X.residueField x ⟶ CommRingCat.of K)

For a field K and a scheme X, the morphisms Spec K ⟶ X bijectively correspond to pairs of points x of X and embeddings κ(x) ⟶ K.

Equations

• One or more equations did not get rendered due to their size.