The category of abelian groups has finite biproducts

instance AddCommGroupCat.instHasBinaryBiproductsAddCommGroupCatInstAddCommGroupCatLargeCategoryPreadditiveHasZeroMorphismsInstPreadditiveAddCommGroupCatInstAddCommGroupCatLargeCategory : CategoryTheory.Limits.HasBinaryBiproducts AddCommGroupCat

instance AddCommGroupCat.instHasFiniteBiproductsAddCommGroupCatInstAddCommGroupCatLargeCategoryPreadditiveHasZeroMorphismsInstPreadditiveAddCommGroupCatInstAddCommGroupCatLargeCategory : CategoryTheory.Limits.HasFiniteBiproducts AddCommGroupCat

@[simp]

theorem AddCommGroupCat.binaryProductLimitCone_cone_pt (G : AddCommGroupCat) (H : AddCommGroupCat) : (AddCommGroupCat.binaryProductLimitCone G H).cone.pt = AddCommGroupCat.of (↑G × ↑H)

@[simp]

theorem AddCommGroupCat.binaryProductLimitCone_isLimit_lift (G : AddCommGroupCat) (H : AddCommGroupCat) (s : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair G H)) : CategoryTheory.Limits.IsLimit.lift (AddCommGroupCat.binaryProductLimitCone G H).isLimit s = AddMonoidHom.prod (s.π.app { as := CategoryTheory.Limits.WalkingPair.left }) (s.π.app { as := CategoryTheory.Limits.WalkingPair.right })

def AddCommGroupCat.binaryProductLimitCone (G : AddCommGroupCat) (H : AddCommGroupCat) : CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair G H)

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

@[simp]

theorem AddCommGroupCat.binaryProductLimitCone_cone_π_app_left (G : AddCommGroupCat) (H : AddCommGroupCat) : (AddCommGroupCat.binaryProductLimitCone G H).cone.π.app { as := CategoryTheory.Limits.WalkingPair.left } = AddMonoidHom.fst ↑G ↑H

@[simp]

theorem AddCommGroupCat.binaryProductLimitCone_cone_π_app_right (G : AddCommGroupCat) (H : AddCommGroupCat) : (AddCommGroupCat.binaryProductLimitCone G H).cone.π.app { as := CategoryTheory.Limits.WalkingPair.right } = AddMonoidHom.snd ↑G ↑H

@[simp]

theorem AddCommGroupCat.biprodIsoProd_hom_apply (G : AddCommGroupCat) (H : AddCommGroupCat) (i : ↑(CategoryTheory.Limits.BinaryBicone.toCone (CategoryTheory.Limits.BinaryBiproduct.bicone G H)).pt) : ↑(AddCommGroupCat.biprodIsoProd G H).hom i = (↑CategoryTheory.Limits.biprod.fst i, ↑CategoryTheory.Limits.biprod.snd i)

noncomputable def AddCommGroupCat.biprodIsoProd (G : AddCommGroupCat) (H : AddCommGroupCat) : G ⊞ H ≅ AddCommGroupCat.of (↑G × ↑H)

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

theorem AddCommGroupCat.biprodIsoProd_inv_comp_fst_apply (G : AddCommGroupCat) (H : AddCommGroupCat) (x : (CategoryTheory.forget AddCommGroupCat).obj (AddCommGroupCat.binaryProductLimitCone G H).cone.pt) : ↑CategoryTheory.Limits.biprod.fst (↑(CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso (CategoryTheory.Limits.BinaryBiproduct.isLimit G H) (AddCommGroupCat.binaryProductLimitCone G H).isLimit).inv x) = ↑(AddMonoidHom.fst ↑G ↑H) x

@[simp]

theorem AddCommGroupCat.biprodIsoProd_inv_comp_fst (G : AddCommGroupCat) (H : AddCommGroupCat) : CategoryTheory.CategoryStruct.comp (AddCommGroupCat.biprodIsoProd G H).inv CategoryTheory.Limits.biprod.fst = AddMonoidHom.fst ↑G ↑H

theorem AddCommGroupCat.biprodIsoProd_inv_comp_snd_apply (G : AddCommGroupCat) (H : AddCommGroupCat) (x : (CategoryTheory.forget AddCommGroupCat).obj (AddCommGroupCat.binaryProductLimitCone G H).cone.pt) : ↑CategoryTheory.Limits.biprod.snd (↑(CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso (CategoryTheory.Limits.BinaryBiproduct.isLimit G H) (AddCommGroupCat.binaryProductLimitCone G H).isLimit).inv x) = ↑(AddMonoidHom.snd ↑G ↑H) x

@[simp]

theorem AddCommGroupCat.biprodIsoProd_inv_comp_snd (G : AddCommGroupCat) (H : AddCommGroupCat) : CategoryTheory.CategoryStruct.comp (AddCommGroupCat.biprodIsoProd G H).inv CategoryTheory.Limits.biprod.snd = AddMonoidHom.snd ↑G ↑H

@[simp]

theorem AddCommGroupCat.HasLimit.lift_apply {J : Type w} (f : J → AddCommGroupCat) (s : CategoryTheory.Limits.Fan f) (x : ↑s.pt) (j : J) : ↑(AddCommGroupCat.HasLimit.lift f s) x j = ↑(s.π.app { as := j }) x

def AddCommGroupCat.HasLimit.lift {J : Type w} (f : J → AddCommGroupCat) (s : CategoryTheory.Limits.Fan f) : 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.

@[simp]

theorem AddCommGroupCat.HasLimit.productLimitCone_cone_π {J : Type w} (f : J → AddCommGroupCat) : (AddCommGroupCat.HasLimit.productLimitCone f).cone.π = CategoryTheory.Discrete.natTrans fun j => Pi.evalAddMonoidHom (fun j => ↑(f j)) j.as

@[simp]

theorem AddCommGroupCat.HasLimit.productLimitCone_cone_pt {J : Type w} (f : J → AddCommGroupCat) : (AddCommGroupCat.HasLimit.productLimitCone f).cone.pt = AddCommGroupCat.of ((j : J) → ↑(f j))

@[simp]

theorem AddCommGroupCat.HasLimit.productLimitCone_isLimit_lift {J : Type w} (f : J → AddCommGroupCat) (s : CategoryTheory.Limits.Fan f) : CategoryTheory.Limits.IsLimit.lift (AddCommGroupCat.HasLimit.productLimitCone f).isLimit s = AddCommGroupCat.HasLimit.lift f s

def AddCommGroupCat.HasLimit.productLimitCone {J : Type w} (f : J → AddCommGroupCat) : CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor f)

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

@[simp]

theorem AddCommGroupCat.biproductIsoPi_hom_apply {J : Type} [Fintype J] (f : J → AddCommGroupCat) (x : ↑(CategoryTheory.Limits.Bicone.toCone (CategoryTheory.Limits.biproduct.bicone f)).pt) (j : J) : ↑(AddCommGroupCat.biproductIsoPi f).hom x j = ↑(CategoryTheory.Limits.biproduct.π f j) x

noncomputable def AddCommGroupCat.biproductIsoPi {J : Type} [Fintype J] (f : J → AddCommGroupCat) : ⨁ 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.

theorem AddCommGroupCat.biproductIsoPi_inv_comp_π_apply {J : Type} [Fintype J] (f : J → AddCommGroupCat) (j : J) (x : (CategoryTheory.forget AddCommGroupCat).obj (AddCommGroupCat.HasLimit.productLimitCone f).cone.pt) : ↑(CategoryTheory.Limits.biproduct.π f j) (↑(CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso (CategoryTheory.Limits.biproduct.isLimit f) (AddCommGroupCat.HasLimit.productLimitCone f).isLimit).inv x) = ↑(Pi.evalAddMonoidHom (fun j => ↑(f j)) j) x

@[simp]

theorem AddCommGroupCat.biproductIsoPi_inv_comp_π {J : Type} [Fintype J] (f : J → AddCommGroupCat) (j : J) : CategoryTheory.CategoryStruct.comp (AddCommGroupCat.biproductIsoPi f).inv (CategoryTheory.Limits.biproduct.π f j) = Pi.evalAddMonoidHom (fun j => ↑(f j)) j