finitary_extensive

Mathlib.CategoryTheory.Sites.LeftExact

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

English

The adhesive property holds in the sheaf category given a base adhesive category with pullbacks and pushouts.

Русский

Адгезивность сохраняется в категории шейфов при базовой адгезивной категории с pullbacks и pushouts.

LaTeX

$$$ \\text{Adhesive} (Sheaf J D) $$$

Lean4

instance finitary_extensive [HasSheafify J (Type w)] : FinitaryExtensive (Sheaf J (Type w)) :=
  inferInstance

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

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

Разделы

Аффилиация

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