Γ_obj — Mathlib

English

The global sections functor evaluated on X in the opposite category equals the presheaf value of X at the top open, i.e., Γ.obj X = (unop X).presheaf.obj (op ⊤).

Русский

Глобальные секции: Γ.obj X равняется значению предшаблонной оболочки X на верхнем открытом, т.е. Γ.obj X = (unop X).presheaf.obj (op ⊤).

LaTeX

$$$\Gamma.obj X = (\mathrm{unop}\;X).presheaf.obj(\mathrm{op}\;\top)$$$

Lean4

@[simp]
theorem Γ_obj (X : (SheafedSpace C)ᵒᵖ) : Γ.obj X = (unop X).presheaf.obj (op ⊤) :=
  rfl

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