# Documentation

Mathlib.Algebra.Category.GroupCat.Biproducts

# The category of abelian groups has finite biproducts #

Construct limit data for a binary product in AddCommGroupCat, using AddCommGroupCat.of (G × H).

Instances For
@[simp]
().hom i = (CategoryTheory.Limits.biprod.fst i, CategoryTheory.Limits.biprod.snd i)

We verify that the biproduct in AddCommGroupCat is isomorphic to the cartesian product of the underlying types:

Instances For
CategoryTheory.Limits.biprod.fst (().inv x) = ↑(AddMonoidHom.fst G H) x
CategoryTheory.Limits.biprod.snd (().inv x) = ↑(AddMonoidHom.snd G H) x
@[simp]
theorem AddCommGroupCat.HasLimit.lift_apply {J : Type w} (f : ) (s : ) (x : s.pt) (j : J) :
↑() x j = ↑(s.app { as := j }) x
def AddCommGroupCat.HasLimit.lift {J : Type w} (f : ) (s : ) :
s.pt AddCommGroupCat.of ((j : J) → ↑(f j))

The map from an arbitrary cone over an indexed family of abelian groups to the cartesian product of those groups.

Instances For
@[simp]
@[simp]
theorem AddCommGroupCat.HasLimit.productLimitCone_cone_pt {J : Type w} (f : ) :
.pt = AddCommGroupCat.of ((j : J) → ↑(f j))

Construct limit data for a product in AddCommGroupCat, using AddCommGroupCat.of (∀ j, F.obj j).

Instances For
@[simp]
theorem AddCommGroupCat.biproductIsoPi_hom_apply {J : Type} [] (f : ) (j : J) :
().hom x j =
noncomputable def AddCommGroupCat.biproductIsoPi {J : Type} [] (f : ) :
f AddCommGroupCat.of ((j : J) → ↑(f j))

We verify that the biproduct we've just defined is isomorphic to the AddCommGroupCat structure on the dependent function type.

Instances For
theorem AddCommGroupCat.biproductIsoPi_inv_comp_π_apply {J : Type} [] (f : ) (j : J) (x : ) :
↑() (().inv x) = ↑(Pi.evalAddMonoidHom (fun j => ↑(f j)) j) x
@[simp]
theorem AddCommGroupCat.biproductIsoPi_inv_comp_π {J : Type} [] (f : ) (j : J) :
= Pi.evalAddMonoidHom (fun j => ↑(f j)) j