mathlib documentation

algebra.category.Group.biproducts

The category of abelian groups has finite biproducts #

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

Equations

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

Equations
def AddCommGroup.biproduct_iso_pi {J : Type u} [decidable_eq J] [fintype J] (f : J → AddCommGroup) :
f AddCommGroup.of (Π (j : J), (f j))

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

Equations