The category of abelian groups has finite biproducts

instance AddCommGrpCat.instHasBinaryBiproducts : CategoryTheory.Limits.HasBinaryBiproducts AddCommGrpCat

instance AddCommGrpCat.instHasFiniteBiproducts : CategoryTheory.Limits.HasFiniteBiproducts AddCommGrpCat

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddCommGrpCat.binaryProductLimitCone_cone_pt (G H : AddCommGrpCat) : (G.binaryProductLimitCone H).cone.pt = ↧(↑G × ↑H)

@[simp]

theorem AddCommGrpCat.binaryProductLimitCone_isLimit_lift (G H : AddCommGrpCat) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair G H)) : (G.binaryProductLimitCone H).isLimit.lift t = ofHom ((Hom.hom (CategoryTheory.Limits.BinaryFan.fst t)).prod (Hom.hom (CategoryTheory.Limits.BinaryFan.snd t)))

@[simp]

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

@[simp]

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

noncomputable def AddCommGrpCat.biprodIsoProd (G H : AddCommGrpCat) : G ⊞ H ≅ ↧(↑G × ↑H)

We verify that the biproduct in AddCommGrpCat is isomorphic to the Cartesian product of the underlying types:

Equations

• G.biprodIsoProd H = (CategoryTheory.Limits.BinaryBiproduct.isLimit G H).conePointUniqueUpToIso (G.binaryProductLimitCone H).isLimit

@[simp]

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

theorem AddCommGrpCat.biprodIsoProd_inv_comp_fst_apply (G H : AddCommGrpCat) (x : ↑G × ↑H) : (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.biprod.fst) ((CategoryTheory.ConcreteCategory.hom (G.biprodIsoProd H).inv) x) = x.1

@[simp]

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

theorem AddCommGrpCat.biprodIsoProd_inv_comp_snd_apply (G H : AddCommGrpCat) (x : ↑G × ↑H) : (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.biprod.snd) ((CategoryTheory.ConcreteCategory.hom (G.biprodIsoProd H).inv) x) = x.2

theorem AddCommGrpCat.biprodIsoProd_inv_comp_desc {G H K : AddCommGrpCat} (f : G ⟶ K) (g : H ⟶ K) : CategoryTheory.CategoryStruct.comp (G.biprodIsoProd H).inv (CategoryTheory.Limits.biprod.desc f g) = CategoryTheory.CategoryStruct.comp (ofHom (AddMonoidHom.fst ↑G ↑H)) f + CategoryTheory.CategoryStruct.comp (ofHom (AddMonoidHom.snd ↑G ↑H)) g

theorem AddCommGrpCat.biprodIsoProd_inv_comp_desc_apply {G H K : AddCommGrpCat} (f : G ⟶ K) (g : H ⟶ K) (x : ↑G × ↑H) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.biprod.desc f g)) ((CategoryTheory.ConcreteCategory.hom (G.biprodIsoProd H).inv) x) = (Hom.hom f) x.1 + (Hom.hom g) x.2

def AddCommGrpCat.HasLimit.lift {J : Type w} (f : J → AddCommGrpCat) (s : CategoryTheory.Limits.Fan f) : s.pt ⟶ ↧((j : J) → ↑(f j))

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

Equations

• AddCommGrpCat.HasLimit.lift f s = AddCommGrpCat.ofHom { toFun := fun (x : ↑s.1) (j : J) => (CategoryTheory.ConcreteCategory.hom (s.π.app { as := j })) x, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AddCommGrpCat.HasLimit.lift_hom_apply {J : Type w} (f : J → AddCommGrpCat) (s : CategoryTheory.Limits.Fan f) (x : ↑s.1) (j : J) : (Hom.hom (lift f s)) x j = (CategoryTheory.ConcreteCategory.hom (s.π.app { as := j })) x

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

theorem AddCommGrpCat.HasLimit.productLimitCone_cone_pt_coe {J : Type w} (f : J → AddCommGrpCat) : ↑(productLimitCone f).cone.pt = ((j : J) → ↑(f j))

noncomputable def AddCommGrpCat.biproductIsoPi {J : Type} [Finite J] (f : J → AddCommGrpCat) : ⨁ f ≅ ↧((j : J) → ↑(f j))

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

Equations

• AddCommGrpCat.biproductIsoPi f = (CategoryTheory.Limits.biproduct.isLimit f).conePointUniqueUpToIso (AddCommGrpCat.HasLimit.productLimitCone f).isLimit

@[simp]

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

theorem AddCommGrpCat.biproductIsoPi_inv_comp_π_apply {J : Type} [Finite J] (f : J → AddCommGrpCat) (j : J) (x : (j : J) → ↑(f j)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.biproduct.π f j)) ((CategoryTheory.ConcreteCategory.hom (biproductIsoPi f).inv) x) = x j