coproductCocone — Mathlib

English

The coproduct cone in ModuleCat is given by the DirectSum direct sum with injections lof.

Русский

Конус coproduct в ModuleCat задан как прямую сумму DirectSum с инъекциями lof.

LaTeX

$$$ \text{coproductCocone} : Cofan Z = (ModuleCat.of R (⨁ i, Z i)) \to (DirectSum.lof R ι (fun i ↦ Z i))$$$

Lean4

/-- The coproduct cone induced by the concrete coproduct. -/
def coproductCocone : Cofan Z :=
  Cofan.mk (ModuleCat.of R (⨁ i : ι, Z i)) fun i => ofHom (DirectSum.lof R ι (fun i ↦ Z i) i)

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