Γ_obj

Mathlib.AlgebraicGeometry.Scheme

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

English

Global sections functor on the opposite scheme equals the global sections on the underlying topological space.

Русский

Глобальные секции применяются к X^{op} дают такие же глобальные секции на X через вершину ⊤.

LaTeX

$$$ \Gamma .\mathrm{obj} (X^{\mathrm{op}}) = \Gamma(\mathrm{unop}(X), \top). $$$

Lean4

@[simp]
theorem Γ_obj (X : Schemeᵒᵖ) : Γ.obj X = Γ(unop X, ⊤) :=
  rfl

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

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

Разделы

Аффилиация

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