# mathlibdocumentation

algebra.category.Group.biproducts

# The category of abelian groups has finite biproducts #

@[protected, instance]
@[protected, instance]

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

Equations
@[simp]
@[simp]
@[simp]

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

Equations
@[simp]
@[simp]
@[simp]
theorem AddCommGroup.has_limit.lift_apply {J : Type w} (f : J → AddCommGroup) (x : (s.X)) (j : J) :
x j = (s.π.app {as := j}) x
def AddCommGroup.has_limit.lift {J : Type w} (f : J → AddCommGroup)  :
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.

Equations

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

Equations
@[simp]
@[simp]
theorem AddCommGroup.has_limit.product_limit_cone_cone_X {J : Type w} (f : J → AddCommGroup) :
= AddCommGroup.of (Π (j : J), (f j))
@[simp]
@[simp]
theorem AddCommGroup.biproduct_iso_pi_hom_apply {J : Type} [fintype J] (f : J → AddCommGroup) (x : ) (j : J) :
j =
noncomputable def AddCommGroup.biproduct_iso_pi {J : Type} [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
@[simp]
theorem AddCommGroup.biproduct_iso_pi_inv_comp_π_apply {J : Type} [fintype J] (f : J → AddCommGroup) (j : J) (x : (AddCommGroup.of (Π (j : J), (f j)))) :
x) = (pi.eval_add_monoid_hom (λ (j : J), (f j)) j) x
@[simp]
theorem AddCommGroup.biproduct_iso_pi_inv_comp_π {J : Type} [fintype J] (f : J → AddCommGroup) (j : J) :
= pi.eval_add_monoid_hom (λ (j : J), (f j)) j