Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.descResidueField_fromSpecResidueField

∀ {K : Type u_1} [inst : Field K] (X : AlgebraicGeometry.Scheme) {x : ↥X} (f : X.presheaf.stalk x ⟶ CommRingCat.of K)
  [inst_1 : IsLocalHom (CommRingCat.Hom.hom f)],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.descResidueField f))
      (X.fromSpecResidueField x) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) (X.fromSpecStalk x)

Defined in

Mathlib.AlgebraicGeometry.ResidueField

Cited by

1 results in Mathlib

Foundations

Depth 148 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldIsLocalHom