Chosen finite products in Grp and friends

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

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

@[simp]

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

noncomputable instance Grp.cartesianMonoidalCategoryGrp : CategoryTheory.CartesianMonoidalCategory Grp

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

noncomputable instance Grp.instBraidedCategory : CategoryTheory.BraidedCategory Grp

noncomputable instance Grp.instBraidedForget : (CategoryTheory.forget Grp).Braided

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

@[simp]

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

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

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

@[simp]

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

noncomputable instance AddGrp.cartesianMonoidalCategoryAddGrp : CategoryTheory.CartesianMonoidalCategory AddGrp

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

noncomputable instance AddGrp.instBraidedCategory : CategoryTheory.BraidedCategory AddGrp

noncomputable instance AddGrp.instBraidedForget : (CategoryTheory.forget AddGrp).Braided

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

@[simp]

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

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

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

@[simp]

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

noncomputable instance CommGrp.cartesianMonoidalCategoryCommGrp : CategoryTheory.CartesianMonoidalCategory CommGrp

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

noncomputable instance CommGrp.instBraidedCategory : CategoryTheory.BraidedCategory CommGrp

noncomputable instance CommGrp.instBraidedForget : (CategoryTheory.forget CommGrp).Braided

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

@[simp]

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

noncomputable def AddCommGrp.cartesianMonoidalCategoryAddCommGrp : CategoryTheory.CartesianMonoidalCategory AddCommGrp

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

@[deprecated AddCommGrp.cartesianMonoidalCategoryAddCommGrp (since := "2025-05-15")]

def AddCommGrp.chosenFiniteProductsAddCommGrp : CategoryTheory.CartesianMonoidalCategory AddCommGrp

Alias of AddCommGrp.cartesianMonoidalCategoryAddCommGrp.

---

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

noncomputable instance AddCommGrp.instBraidedCategory : CategoryTheory.BraidedCategory AddCommGrp

noncomputable instance AddCommGrp.instBraidedForget : (CategoryTheory.forget AddCommGrp).Braided

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

@[simp]

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