mathlib documentation

algebra.category.Group.biproducts

The category of abelian groups has finite biproducts

source
def AddCommGroup.binary_product_limit_cone (G H : AddCommGroup) :
category_theory.limits.limit_cone (category_theory.limits.pair G H)

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

Equations
source
@[instance]
def AddCommGroup.has_binary_product (G H : AddCommGroup) :
category_theory.limits.has_binary_product G H

source
@[instance]
def AddCommGroup.category_theory.limits.has_binary_biproduct (G H : AddCommGroup) :
category_theory.limits.has_binary_biproduct G H

source
def AddCommGroup.biprod_iso_prod (G H : AddCommGroup) :
G ⊞ H ≅ AddCommGroup.of (↥G × ↥H)

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

Equations
source
def AddCommGroup.has_limit.lift {J : Type u} (F : category_theory.discrete J ⥤ AddCommGroup) (s : category_theory.limits.cone F) :
s.X ⟶ AddCommGroup.of (Π (j : category_theory.discrete J), ↥(F.obj j))

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

Equations
source
@[simp]
theorem AddCommGroup.has_limit.lift_apply {J : Type u} (F : category_theory.discrete J ⥤ AddCommGroup) (s : category_theory.limits.cone F) (x : ↥(s.X)) (j : J) :
⇑(AddCommGroup.has_limit.lift F s) x j = ⇑(s.π.app j) x

source
def AddCommGroup.has_limit.product_limit_cone {J : Type u} (F : category_theory.discrete J ⥤ AddCommGroup) :
category_theory.limits.limit_cone F

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

Equations
source
@[instance]
def AddCommGroup.category_theory.limits.has_biproduct {J : Type u} [decidable_eq J] [fintype J] (f : J → AddCommGroup) :
category_theory.limits.has_biproduct f

source
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
source
@[instance]
def AddCommGroup.category_theory.limits.has_finite_biproducts  :
category_theory.limits.has_finite_biproducts AddCommGroup