mathlib documentation


The category of abelian groups has finite biproducts #

noncomputable def AddCommGroup.biprod_iso_prod (G H : AddCommGroup) :

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

theorem AddCommGroup.has_limit.lift_apply {J : Type u} (f : J → AddCommGroup) (s : f) (x : (s.X)) (j : J) :
def AddCommGroup.has_limit.lift {J : Type u} (f : J → AddCommGroup) (s : f) :
s.X AddCommGroup.of (Π (j : J), (f j))

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

noncomputable def AddCommGroup.biproduct_iso_pi {J : Type u} [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

theorem AddCommGroup.biproduct_iso_pi_inv_comp_π_apply {J : Type u} [fintype J] (f : J → AddCommGroup) (j : J) (x : (AddCommGroup.of (Π (j : J), (f j)))) :