coprodIsoDirectSum — Mathlib

English

The categorical coproduct is isomorphic to the direct sum in ModuleCat.

Русский

Категориальное копроизведение изоморфно прямому сумме в ModuleCat.

LaTeX

$$$ \text{coprodIsoDirectSum} : ∐ Z ≅ ModuleCat.of R (⨁ i, Z i)$$$

Lean4

/-- The categorical coproduct of a family of objects in `ModuleCat`
agrees with direct sum.
-/
noncomputable def coprodIsoDirectSum : ∐ Z ≅ ModuleCat.of R (⨁ i, Z i) :=
  colimit.isoColimitCocone ⟨_, coproductCoconeIsColimit Z⟩

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