Documentation

Mathlib.Algebra.Category.Grp.CartesianMonoidal

Chosen finite products in Grp and friends #

source
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)

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[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)))
    source
    @[simp]
    theorem Grp.binaryProductLimitCone_cone_pt (G H : Grp) :
    (G.binaryProductLimitCone H).cone.pt = of (↑G × ↑H)
    source
    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.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    noncomputable instance Grp.instBraidedCategory :
    CategoryTheory.BraidedCategory Grp
    Equations
    source
    noncomputable instance Grp.instBraidedForget :
    (CategoryTheory.forget Grp).Braided
    Equations
    source
    theorem Grp.tensorObj_eq (G H : Grp) :
    CategoryTheory.MonoidalCategoryStruct.tensorObj G H = of (↑G × ↑H)
    source
    @[simp]
    theorem Grp.μ_forget_apply {G H : Grp} (p : ↑G) (q : ↑H) :
    CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.forget Grp) G H (p, q) = (p, q)
    source
    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)

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[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)))
      source
      @[simp]
      theorem AddGrp.binaryProductLimitCone_cone_pt (G H : AddGrp) :
      (G.binaryProductLimitCone H).cone.pt = of (↑G × ↑H)
      source
      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.

      Equations
      • One or more equations did not get rendered due to their size.
      source
      noncomputable instance AddGrp.instBraidedCategory :
      CategoryTheory.BraidedCategory AddGrp
      Equations
      source
      noncomputable instance AddGrp.instBraidedForget :
      (CategoryTheory.forget AddGrp).Braided
      Equations
      source
      theorem AddGrp.tensorObj_eq (G H : AddGrp) :
      CategoryTheory.MonoidalCategoryStruct.tensorObj G H = of (↑G × ↑H)
      source
      @[simp]
      theorem AddGrp.μ_forget_apply {G H : AddGrp} (p : ↑G) (q : ↑H) :
      CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.forget AddGrp) G H (p, q) = (p, q)
      source
      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)

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[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)))
        source
        @[simp]
        theorem CommGrp.binaryProductLimitCone_cone_pt (G H : CommGrp) :
        (G.binaryProductLimitCone H).cone.pt = of (↑G × ↑H)
        source
        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.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        noncomputable instance CommGrp.instBraidedCategory :
        CategoryTheory.BraidedCategory CommGrp
        Equations
        source
        noncomputable instance CommGrp.instBraidedForget :
        (CategoryTheory.forget CommGrp).Braided
        Equations
        source
        theorem CommGrp.tensorObj_eq (G H : CommGrp) :
        CategoryTheory.MonoidalCategoryStruct.tensorObj G H = of (↑G × ↑H)
        source
        @[simp]
        theorem CommGrp.μ_forget_apply {G H : CommGrp} (p : ↑G) (q : ↑H) :
        CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.forget CommGrp) G H (p, q) = (p, q)
        source
        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.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[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.

          Equations
          Instances For
            source
            noncomputable instance AddCommGrp.instBraidedCategory :
            CategoryTheory.BraidedCategory AddCommGrp
            Equations
            source
            noncomputable instance AddCommGrp.instBraidedForget :
            (CategoryTheory.forget AddCommGrp).Braided
            Equations
            source
            theorem AddCommGrp.tensorObj_eq (G H : AddCommGrp) :
            CategoryTheory.MonoidalCategoryStruct.tensorObj G H = of (↑G × ↑H)
            source
            @[simp]
            theorem AddCommGrp.μ_forget_apply {G H : AddCommGrp} (p : ↑G) (q : ↑H) :
            CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.forget AddCommGrp) G H (p, q) = (p, q)