coequalizer — Mathlib

English

There exists a canonical ring homomorphism from the global sections Γ(X, O_X) to the residue field κ(x) of a point x ∈ X, obtained by evaluating global sections at x.

Русский

Существует канонический кольцевой гомоморфизм из глобальных секций Γ(X, O_X) в остаточное поле κ(x) точки x ∈ X, получаемый путем оценки секций в точке x.

LaTeX

$$Γevaluation (x) : Γ( X, O_X ) → κ(x)$$

Lean4

/-- The coequalizer of two locally ringed spaces in the category of sheafed spaces is a locally
ringed space. -/
noncomputable def coequalizer : LocallyRingedSpace
    where
  toSheafedSpace := Limits.coequalizer f.toShHom g.toShHom
  isLocalRing
    x :=
    by
    obtain ⟨y, rfl⟩ := (TopCat.epi_iff_surjective (coequalizer.π f.toShHom g.toShHom).base).mp inferInstance x
    exact ((coequalizer.π f.toShHom g.toShHom :).stalkMap y).hom.domain_isLocalRing

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