Γ_obj_op — Mathlib

English

Same as Γ_obj but for X in the original SheafedSpace rather than its opposite; the global sections equal the presheaf value at the top.

Русский

То же самое для X в оригинальном расслоенном пространстве: глобальные секции равны значению предшествующей оболочки в вершине.

LaTeX

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

Lean4

theorem Γ_obj_op (X : SheafedSpace C) : Γ.obj (op X) = X.presheaf.obj (op ⊤) :=
  rfl

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