ΓIsEquiv

Mathlib.AlgebraicGeometry.AffineScheme

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.AffineScheme.ΓIsEquiv

English

The global sections functor Γ is an equivalence (IsEquivalence).

Русский

Функтор Γ является эквивалентностью (IsEquivalence).

LaTeX

$$$$ \text{Γ is an equivalence}. $$$$

Lean4

instance ΓIsEquiv : Γ.{u}.IsEquivalence :=
  inferInstanceAs (Γ.{u}.rightOp.op ⋙ (opOpEquivalence _).functor).IsEquivalence

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

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

Разделы

Аффилиация

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