left_triangle

Mathlib.AlgebraicGeometry.GammaSpecAdjunction

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.ΓSpec.left_triangle

← MathLib Explorer

English

The left triangle identity holds at the level of LocallyRingedSpace without specifying R.

Русский

Левая треугольная идентичность выполняется на уровне LocallyRingedSpace.

LaTeX

$$Γ_Spec_left_triangle (X) := ...$$

Lean4

theorem left_triangle (X : LocallyRingedSpace) :
    SpecΓIdentity.inv.app (Γ.obj (op X)) ≫ (identityToΓSpec.app X).c.app (op ⊤) = 𝟙 _ :=
  X.Γ_Spec_left_triangle

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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