hasFiniteColimits — Mathlib

English

In an Abelian category, finite colimits exist. In particular, the category has all finite colimits, i.e., coequalizers and finite coproducts, etc.

Русский

В абелевой категории существуют конечные колимиты. В частности, у категории есть все конечные коки (коуравниватели) и конечные копродукты и т.д.

LaTeX

$$$\\\\forall C \\\\text{ abelian }, \\\\mathrm{HasFiniteColimits}(C)$$

Lean4

instance (priority := 100) hasFiniteColimits : HasFiniteColimits C :=
  Limits.hasFiniteColimits_of_hasCoequalizers_and_finite_coproducts

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