instHasFiniteColimits

Mathlib.CategoryTheory.Sites.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Sheaf.instHasFiniteColimits

English

If D has finite colimits, then HasFiniteColimits (Sheaf J D).

Русский

Если D имеет конечные колимиты, то у шейфов J D есть конечные колимиты.

LaTeX

$$$(\text{HasFiniteColimits } D) \Rightarrow (\text{HasFiniteColimits } (\mathrm{Sh}(J,D))).$$$

Lean4

instance [HasFiniteColimits D] : HasFiniteColimits (Sheaf J D) :=
  ⟨fun _ ↦ inferInstance⟩

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

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

Разделы

Аффилиация

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