Γ_obj_op

Mathlib.Geometry.RingedSpace.PresheafedSpace

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.PresheafedSpace.Γ_obj_op

English

Restating Γ.map on op yields the component at op-top.

Русский

Повтор Γ.map на опере даёт компоненту на op-top.

LaTeX

$$$\Gamma.map f.op = f.c.app(\mathrm{op}\top)$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru