hasColimitsOfShape_discrete — Mathlib

English

If a category has finite coproducts, then it has colimits of shape Discrete over any finite index set.

Русский

Если в категории есть конечные копроизведения, то существуют колимиты формы Discrete над любым конечным индексом.

LaTeX

$$$[\text{HasFiniteCoproducts } C] \Rightarrow \operatorname{HasColimitsOfShape}(\mathrm{Discrete}\, \iota) C$ for finite ι$$

Lean4

instance hasColimitsOfShape_discrete [HasFiniteCoproducts C] (ι : Type w) [Finite ι] :
    HasColimitsOfShape (Discrete ι) C :=
  by
  rcases Finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩
  haveI : HasColimitsOfShape (Discrete (Fin n)) C := HasFiniteCoproducts.out n
  exact hasColimitsOfShape_of_equivalence (Discrete.equivalence e.symm)

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