Chosen finite products in GrpCat and friends

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

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

@[simp]

theorem GrpCat.binaryProductLimitCone_isLimit_lift (G H : GrpCat) (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 GrpCat.binaryProductLimitCone_cone_pt (G H : GrpCat) : (G.binaryProductLimitCone H).cone.pt = of (↑G × ↑H)

@[implicit_reducible]

noncomputable instance GrpCat.cartesianMonoidalCategoryGrp : CategoryTheory.CartesianMonoidalCategory GrpCat

We choose GrpCat.of (G × H) as the product of G and H and GrpCat.of PUnit as the terminal object.

@[implicit_reducible]

noncomputable instance GrpCat.instBraidedCategory : CategoryTheory.BraidedCategory GrpCat

@[implicit_reducible]

noncomputable instance GrpCat.instBraidedForgetMonoidHomCarrier : (CategoryTheory.forget GrpCat).Braided

theorem GrpCat.tensorObj_eq (G H : GrpCat) : CategoryTheory.MonoidalCategoryStruct.tensorObj G H = of (↑G × ↑H)

@[simp]

theorem GrpCat.μ_forget_apply {G H : GrpCat} (p : ↑G) (q : ↑H) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.forget GrpCat) G H (p, q) = (p, q)

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

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

@[simp]

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

@[simp]

theorem AddGrpCat.binaryProductLimitCone_isLimit_lift (G H : AddGrpCat) (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)))

@[implicit_reducible]

noncomputable instance AddGrpCat.cartesianMonoidalCategoryAddGrp : CategoryTheory.CartesianMonoidalCategory AddGrpCat

We choose AddGrpCat.of (G × H) as the product of G and H and AddGrpCat.of PUnit as the terminal object.

@[implicit_reducible]

noncomputable instance AddGrpCat.instBraidedCategory : CategoryTheory.BraidedCategory AddGrpCat

@[implicit_reducible]

noncomputable instance AddGrpCat.instBraidedForgetAddMonoidHomCarrier : (CategoryTheory.forget AddGrpCat).Braided

theorem AddGrpCat.tensorObj_eq (G H : AddGrpCat) : CategoryTheory.MonoidalCategoryStruct.tensorObj G H = of (↑G × ↑H)

@[simp]

theorem AddGrpCat.μ_forget_apply {G H : AddGrpCat} (p : ↑G) (q : ↑H) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.forget AddGrpCat) G H (p, q) = (p, q)

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

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

@[simp]

theorem CommGrpCat.binaryProductLimitCone_isLimit_lift (G H : CommGrpCat) (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 CommGrpCat.binaryProductLimitCone_cone_pt (G H : CommGrpCat) : (G.binaryProductLimitCone H).cone.pt = of (↑G × ↑H)

@[implicit_reducible]

noncomputable instance CommGrpCat.cartesianMonoidalCategory : CategoryTheory.CartesianMonoidalCategory CommGrpCat

We choose CommGrpCat.of (G × H) as the product of G and H and CommGrpCat.of PUnit as the terminal object.

@[implicit_reducible]

noncomputable instance CommGrpCat.instBraidedCategory : CategoryTheory.BraidedCategory CommGrpCat

@[implicit_reducible]

noncomputable instance CommGrpCat.instBraidedForgetMonoidHomCarrier : (CategoryTheory.forget CommGrpCat).Braided

theorem CommGrpCat.tensorObj_eq (G H : CommGrpCat) : CategoryTheory.MonoidalCategoryStruct.tensorObj G H = of (↑G × ↑H)

@[simp]

theorem CommGrpCat.μ_forget_apply {G H : CommGrpCat} (p : ↑G) (q : ↑H) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.forget CommGrpCat) G H (p, q) = (p, q)

@[implicit_reducible]

noncomputable def AddCommGrpCat.cartesianMonoidalCategory : CategoryTheory.CartesianMonoidalCategory AddCommGrpCat

We choose AddCommGrpCat.of (G × H) as the product of G and H and AddCommGrpCat.of PUnit as the terminal object.

@[implicit_reducible, deprecated AddCommGrpCat.cartesianMonoidalCategory (since := "2025-10-10")]

def AddCommGrpCat.cartesianMonoidalCategoryAddCommGrp : CategoryTheory.CartesianMonoidalCategory AddCommGrpCat

Alias of AddCommGrpCat.cartesianMonoidalCategory.

---

We choose AddCommGrpCat.of (G × H) as the product of G and H and AddCommGrpCat.of PUnit as the terminal object.

@[implicit_reducible]

noncomputable instance AddCommGrpCat.instBraidedCategory : CategoryTheory.BraidedCategory AddCommGrpCat

@[implicit_reducible]

noncomputable instance AddCommGrpCat.instBraidedForgetAddMonoidHomCarrier : (CategoryTheory.forget AddCommGrpCat).Braided

theorem AddCommGrpCat.tensorObj_eq (G H : AddCommGrpCat) : CategoryTheory.MonoidalCategoryStruct.tensorObj G H = of (↑G × ↑H)

@[simp]

theorem AddCommGrpCat.μ_forget_apply {G H : AddCommGrpCat} (p : ↑G) (q : ↑H) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.forget AddCommGrpCat) G H (p, q) = (p, q)