adhesive

Mathlib.CategoryTheory.Sites.LeftExact

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SheafOfTypes.adhesive

English

The SheafOfTypes category is balanced when it has a sheafify construction.

Русский

Категория SheafOfTypes сбалансирована, когда существует построение шейфикации.

LaTeX

$$$ \\text{Balanced} (Sheaf J Type) $$$

Lean4

instance adhesive [HasSheafify J (Type w)] : Adhesive (Sheaf J (Type w)) :=
  inferInstance

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

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

Разделы

Аффилиация

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