Γ_obj

Mathlib.Geometry.RingedSpace.LocallyRingedSpace

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.LocallyRingedSpace.Γ_obj

English

For X in LocallyRingedSpace, Γ.obj (op X) equals X.presheaf.obj (op ⊤).

Русский

Для X в LocallyRingedSpace, Γ.obj (op X) равно X.presheaf.obj (op ⊤).

LaTeX

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

Lean4

@[simp]
theorem Γ_obj (X : LocallyRingedSpace.{u}ᵒᵖ) : Γ.obj X = X.unop.presheaf.obj (op ⊤) :=
  rfl

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

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

Разделы

Аффилиация

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