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.

noncomputable def AlgebraicGeometry.Scheme.residueField (X : Scheme) (x : ↥X) : 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 = { carrier := IsLocalRing.ResidueField ↑(X.presheaf.stalk x), commRing := IsLocalRing.instCommRingResidueField ↑(X.presheaf.stalk x) }

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Scheme.instFieldCarrierResidueField (X : Scheme) (x : ↥X) : Field ↑(X.residueField x)

Equations

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

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Scheme.instUniqueCarrierCarrierCommRingCatSpecResidueField (X : Scheme) (x : ↥X) : Unique ↥(Spec (X.residueField x))

Equations

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

noncomputable def AlgebraicGeometry.Scheme.residue (X : Scheme) (x : ↥X) : X.presheaf.stalk x ⟶ X.residueField x

The residue map from the stalk to the residue field.

Equations

• X.residue x = CommRingCat.ofHom (IsLocalRing.residue ↑(X.presheaf.stalk x))

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

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

@[simp]

theorem AlgebraicGeometry.Scheme.SpecMap_residue_apply {X : Scheme} (x : ↥X) (s : ↥(Spec (X.residueField x))) : (Spec.map (X.residue x)) s = IsLocalRing.closedPoint ↑(X.presheaf.stalk x)

@[deprecated AlgebraicGeometry.Scheme.SpecMap_residue_apply (since := "2025-10-07")]

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

Alias of AlgebraicGeometry.Scheme.SpecMap_residue_apply.

theorem AlgebraicGeometry.Scheme.residue_surjective (X : Scheme) (x : ↥X) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (X.residue x))

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

noncomputable def AlgebraicGeometry.Scheme.descResidueField {K : Type u} [Field K] {X : Scheme} {x : ↥X} (f : X.presheaf.stalk x ⟶ { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }) [IsLocalHom (CommRingCat.Hom.hom f)] : X.residueField x ⟶ { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }

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 = CommRingCat.ofHom (IsLocalRing.ResidueField.lift (CommRingCat.Hom.hom f))

@[simp]

theorem AlgebraicGeometry.Scheme.residue_descResidueField {K : Type u} [Field K] {X : Scheme} {x : ↥X} (f : X.presheaf.stalk x ⟶ { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }) [IsLocalHom (CommRingCat.Hom.hom f)] : CategoryTheory.CategoryStruct.comp (X.residue x) (descResidueField f) = f

@[simp]

theorem AlgebraicGeometry.Scheme.residue_descResidueField_assoc {K : Type u} [Field K] {X : Scheme} {x : ↥X} (f : X.presheaf.stalk x ⟶ { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }) [IsLocalHom (CommRingCat.Hom.hom f)] {Z : CommRingCat} (h : { carrier := K, commRing := Field.toEuclideanDomain.toCommRing } ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.residue x) (CategoryTheory.CategoryStruct.comp (descResidueField f) h) = CategoryTheory.CategoryStruct.comp f h

noncomputable def AlgebraicGeometry.Scheme.evaluation (X : Scheme) (U : X.Opens) (x : ↥X) (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 : Scheme) {U : X.Opens} (x : ↥X) (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 : Scheme) {U : X.Opens} (x : ↥X) (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]

noncomputable abbrev AlgebraicGeometry.Scheme.Γevaluation (X : Scheme) (x : ↥X) : 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_notMem_basicOpen (X : Scheme) {U : X.Opens} (x : ↥X) (hx : x ∈ U) (f : ↑(X.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (X.evaluation U x hx)) f = 0 ↔ x ∉ X.basicOpen f

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

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

noncomputable def AlgebraicGeometry.Scheme.Hom.residueFieldMap {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) : Y.residueField (f 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.Scheme.Hom.residueFieldMap f x = CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x)))

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

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

@[simp]

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

@[simp]

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

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

theorem AlgebraicGeometry.Scheme.evaluation_naturality_assoc {X Y : Scheme} (f : X ⟶ Y) {V : Y.Opens} (x : ↥X) (hx : f x ∈ V) {Z : CommRingCat} (h : X.residueField x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.evaluation V (f x) hx) (CategoryTheory.CategoryStruct.comp (Hom.residueFieldMap f x) h) = CategoryTheory.CategoryStruct.comp (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 Y : Scheme} (f : X ⟶ Y) {V : Y.Opens} (x : ↥X) (hx : f x ∈ V) (s : ↑(Y.presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (Hom.residueFieldMap f x)) ((CategoryTheory.ConcreteCategory.hom (Y.evaluation V (f x) hx)) s) = (CategoryTheory.ConcreteCategory.hom (X.evaluation ((TopologicalSpace.Opens.map f.base).obj V) x hx)) ((CategoryTheory.ConcreteCategory.hom (Hom.app f V)) s)

theorem AlgebraicGeometry.Scheme.Γevaluation_naturality {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) : CategoryTheory.CategoryStruct.comp (Y.Γevaluation (f x)) (Hom.residueFieldMap f x) = CategoryTheory.CategoryStruct.comp (Hom.appTop f) (X.Γevaluation x)

theorem AlgebraicGeometry.Scheme.Γevaluation_naturality_assoc {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) {Z : CommRingCat} (h : X.residueField x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.Γevaluation (f x)) (CategoryTheory.CategoryStruct.comp (Hom.residueFieldMap f x) h) = CategoryTheory.CategoryStruct.comp (Hom.appTop f) (CategoryTheory.CategoryStruct.comp (X.Γevaluation x) h)

theorem AlgebraicGeometry.Scheme.Γevaluation_naturality_apply {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) (a : ↑(Y.presheaf.obj (Opposite.op ⊤))) : (CategoryTheory.ConcreteCategory.hom (Hom.residueFieldMap f x)) ((CategoryTheory.ConcreteCategory.hom (Y.Γevaluation (f x))) a) = (CategoryTheory.ConcreteCategory.hom (X.Γevaluation x)) ((CategoryTheory.ConcreteCategory.hom (Hom.appTop f)) a)

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

noncomputable def AlgebraicGeometry.Scheme.residueFieldCongr {X : Scheme} {x y : ↥X} (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 : Scheme} {x : ↥X} : residueFieldCongr ⋯ = CategoryTheory.Iso.refl (X.residueField x)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem AlgebraicGeometry.Scheme.residue_residueFieldCongr_assoc (X : Scheme) {x y : ↥X} (h : x = y) {Z : CommRingCat} (h✝ : X.residueField y ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.residue x) (CategoryTheory.CategoryStruct.comp (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 Y : Scheme} {f g : X ⟶ Y} (e : f = g) (x : ↥X) : residueFieldMap f x = CategoryTheory.CategoryStruct.comp (residueFieldCongr ⋯).hom (residueFieldMap g x)

noncomputable def AlgebraicGeometry.Scheme.fromSpecResidueField (X : Scheme) (x : ↥X) : 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 : Scheme} (x : ↥X) : IsPreimmersion (X.fromSpecResidueField x)

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Scheme.instOverSpecResidueField {X : Scheme} (x : ↥X) : (Spec (X.residueField x)).Over X

Equations

• AlgebraicGeometry.Scheme.instOverSpecResidueField x = { hom := X.fromSpecResidueField x }

@[simp]

theorem AlgebraicGeometry.Scheme.over_def {X : Scheme} (x : ↥X) : Spec (X.residueField x) ↘ X = X.fromSpecResidueField x

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Scheme.instCanonicallyOverSpecResidueField {X : Scheme} (x : ↥X) : (Spec (X.residueField x)).CanonicallyOver X

Equations

• AlgebraicGeometry.Scheme.instCanonicallyOverSpecResidueField x = { toOverClass := AlgebraicGeometry.Scheme.instOverSpecResidueField x }

@[simp]

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

@[simp]

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

instance AlgebraicGeometry.Scheme.instIsOverMapHomCommRingCatResidueFieldCongr {X : Scheme} {x y : ↥X} (h : x = y) : Hom.IsOver (Spec.map (residueFieldCongr h).hom) X

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) : CategoryTheory.CategoryStruct.comp (Spec.map (residueFieldMap f x)) (Y.fromSpecResidueField (f x)) = CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) f

@[simp]

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

@[deprecated AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField (since := "2025-10-07")]

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

Alias of AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField.

@[deprecated AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc (since := "2025-10-07")]

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

Alias of AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc.

instance AlgebraicGeometry.Scheme.instIsOverMapResidueFieldMapOverInferInstanceOverClass {X Y : Scheme} [X.Over Y] (x : ↥X) : Hom.IsOver (Spec.map (Hom.residueFieldMap (X ↘ Y) x)) Y

@[simp]

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

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

theorem AlgebraicGeometry.Scheme.descResidueField_fromSpecResidueField {K : Type u_1} [Field K] (X : Scheme) {x : ↥X} (f : X.presheaf.stalk x ⟶ { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }) [IsLocalHom (CommRingCat.Hom.hom f)] : CategoryTheory.CategoryStruct.comp (Spec.map (descResidueField f)) (X.fromSpecResidueField x) = CategoryTheory.CategoryStruct.comp (Spec.map f) (X.fromSpecStalk x)

theorem AlgebraicGeometry.Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField (K : Type u) [Field K] (X : Scheme) (f : Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing } ⟶ X) : CategoryTheory.CategoryStruct.comp (Spec.map (descResidueField (stalkClosedPointTo f))) (X.fromSpecResidueField (f (IsLocalRing.closedPoint K))) = f

noncomputable def AlgebraicGeometry.Scheme.Spec.residueFieldIso (R : CommRingCat) (x : ↥(Spec R)) : (Spec R).residueField x ≅ { carrier := x.asIdeal.ResidueField, commRing := IsLocalRing.instCommRingResidueField (Localization.AtPrime x.asIdeal) }

The residue fields of Spec R are isomorphic to Ideal.ResidueField.

Equations

• AlgebraicGeometry.Scheme.Spec.residueFieldIso R x = (IsLocalRing.ResidueField.mapEquiv (AlgebraicGeometry.Spec.stalkIso R x).commRingCatIsoToRingEquiv).toCommRingCatIso

@[simp]

theorem AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv (R : CommRingCat) (x : ↥(Spec R)) : CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField)) (residueFieldIso R x).inv = CategoryTheory.CategoryStruct.comp (ΓSpecIso R).inv (CategoryTheory.CategoryStruct.comp ((Spec R).presheaf.germ ⊤ x trivial) ((Spec R).residue x))

@[simp]

theorem AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc (R : CommRingCat) (x : ↥(Spec R)) {Z : CommRingCat} (h : (Spec R).residueField x ⟶ Z) : CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField)) (CategoryTheory.CategoryStruct.comp (residueFieldIso R x).inv h) = CategoryTheory.CategoryStruct.comp (ΓSpecIso R).inv (CategoryTheory.CategoryStruct.comp ((Spec R).presheaf.germ ⊤ x trivial) (CategoryTheory.CategoryStruct.comp ((Spec R).residue x) h))

@[simp]

theorem AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom (R : CommRingCat) (x : ↥(Spec R)) : CategoryTheory.CategoryStruct.comp ((Spec R).residue x) (residueFieldIso R x).hom = CategoryTheory.CategoryStruct.comp (Spec.stalkIso R x).hom (CommRingCat.ofHom (algebraMap (Localization.AtPrime x.asIdeal) x.asIdeal.ResidueField))

@[simp]

theorem AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom_assoc (R : CommRingCat) (x : ↥(Spec R)) {Z : CommRingCat} (h : { carrier := x.asIdeal.ResidueField, commRing := IsLocalRing.instCommRingResidueField (Localization.AtPrime x.asIdeal) } ⟶ Z) : CategoryTheory.CategoryStruct.comp ((Spec R).residue x) (CategoryTheory.CategoryStruct.comp (residueFieldIso R x).hom h) = CategoryTheory.CategoryStruct.comp (Spec.stalkIso R x).hom (CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap (Localization.AtPrime x.asIdeal) x.asIdeal.ResidueField)) h)

@[simp]

theorem AlgebraicGeometry.Scheme.Spec.map_residueFieldIso_inv_eq_fromSpecResidueField (R : CommRingCat) (x : ↥(Spec R)) : CategoryTheory.CategoryStruct.comp (Spec.map (residueFieldIso R x).inv) (Spec.map (CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField))) = (Spec R).fromSpecResidueField x

@[simp]

theorem AlgebraicGeometry.Scheme.Spec.map_residueFieldIso_inv_eq_fromSpecResidueField_assoc (R : CommRingCat) (x : ↥(Spec R)) {Z : Scheme} (h : Spec { carrier := ↑R, commRing := R.commRing } ⟶ Z) : CategoryTheory.CategoryStruct.comp (Spec.map (residueFieldIso R x).inv) (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField))) h) = CategoryTheory.CategoryStruct.comp ((Spec R).fromSpecResidueField x) h

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

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

noncomputable def AlgebraicGeometry.Scheme.SpecToEquivOfField (K : Type u) [Field K] (X : Scheme) : (Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing } ⟶ X) ≃ (x : ↥X) × (X.residueField x ⟶ { carrier := K, commRing := Field.toEuclideanDomain.toCommRing })

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.