descResidueField — Mathlib

English

Given a field K and a stalk map f: O_{X,x} → K of local type, there is a canonical map κ(x) → K induced by f.

Русский

Для поля K и гомоморфизма стэка f: O_{X,x} → K существет каноническое отображение κ(x) → K, индуцированное f.

LaTeX

$$$$ \kappa(x) \to K \text{ is induced by } f \text{ (canonically).} $$$$

Lean4

/-- If `K` is a field and `f : 𝒪_{X, x} ⟶ K` is a ring map, then this is the induced
map `κ(x) ⟶ K`. -/
def descResidueField {K : Type u} [Field K] {X : Scheme.{u}} {x : X} (f : X.presheaf.stalk x ⟶ .of K)
    [IsLocalHom f.hom] : X.residueField x ⟶ .of K :=
  CommRingCat.ofHom (IsLocalRing.ResidueField.lift (S := K) f.hom)

Похожие утверждения