instHasCoproductsIndOfHasFiniteCoproducts

English

If C has finite coproducts, then Ind(C) has coproducts.

Русский

Если в C существуют конечные coproducts, то Ind(C) имеет coproducts.

LaTeX

$$$\operatorname{HasFiniteCoproducts}(C) \Rightarrow \operatorname{HasCoproducts}(\mathrm{Ind}\,C)$$$

Lean4

instance [HasFiniteCoproducts C] : HasCoproducts.{v} (Ind C) :=
  have : HasFiniteCoproducts (Ind C) := ⟨fun _ => hasColimitsOfShape_of_equivalence (Discrete.equivalence Equiv.ulift)⟩
  hasCoproducts_of_finite_and_filtered

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