hasZeroObject_of_hasFiniteBiproducts

English

There is an equivalence between morphisms ⟶ between biproducts and matrices of morphisms; the equivalence is defined by toFun = biproduct.components and invFun = biproduct.matrix, with the stated inverses.

Русский

Существует эквивалентность между морфизмами между биопродуктами и матрицами морфизмов; эквивалентность задаётся через toFun = biproduct.components и invFun = biproduct.matrix, с указанными обратными связями.

LaTeX

$$$ (\\⟶) : (⨁ f ⟶ ⨁ g) \\simeq (j: J) (k: K) → \\mathrm{Hom}(f j, g k) $$$

Lean4

/-- A category with finite biproducts has a zero object. -/
instance (priority := 100) hasZeroObject_of_hasFiniteBiproducts [HasFiniteBiproducts C] : HasZeroObject C :=
  by
  refine ⟨⟨biproduct Empty.elim, fun X => ⟨⟨⟨0⟩, ?_⟩⟩, fun X => ⟨⟨⟨0⟩, ?_⟩⟩⟩⟩
  · intro a; apply biproduct.hom_ext'; simp
  · intro a; apply biproduct.hom_ext; simp

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