hasFiniteCoproducts_of_has_binary_and_initial

English

If a category has an initial object and binary coproducts, then it has all finite coproducts.

Русский

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

LaTeX

$$$HasInitial(C) \wedge HasBinaryCoproducts(C) \Rightarrow HasFiniteCoproducts(C)$$$

Lean4

/-- If `C` has an initial object and binary coproducts, then it has finite coproducts. -/
theorem hasFiniteCoproducts_of_has_binary_and_initial : HasFiniteCoproducts C :=
  ⟨fun n =>
    ⟨fun K => by
      let that : K ≅ Discrete.functor fun n => K.obj ⟨n⟩ := Discrete.natIso fun ⟨_⟩ => Iso.refl _
      rw [hasColimit_iff_of_iso that]
      apply hasCoproduct_fin⟩⟩

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