instTopologicalSpaceCarrierCarrier

Mathlib.Geometry.RingedSpace.SheafedSpace

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier

English

The global sections functor evaluated at op X equals the presheaf value at op-top.

Русский

Глобальные секции, применённые к op X, равны значению прешефда на op верх.

LaTeX

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

Lean4

instance (X : SheafedSpace C) : TopologicalSpace X :=
  X.carrier.str

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

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

Разделы

Аффилиация

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