Γ_map_op

Mathlib.Geometry.RingedSpace.PresheafedSpace

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

English

A repeat statement that Γ.map on op is given by the presheaf component at op-top.

Русский

Повторенное утверждение: Γ.map на op задаётся компонентой прешефа на топе.

LaTeX

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

Lean4

theorem Γ_map_op {X Y : PresheafedSpace C} (f : X ⟶ Y) : Γ.map f.op = f.c.app (op ⊤) :=
  rfl

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

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

Разделы

Аффилиация

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