Documentation

Mathlib.Algebra.Category.Grp.CartesianMonoidal

Chosen finite products in GrpCat and friends #

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

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

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

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

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

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

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

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

          Equations
          Instances For
            source
            @[deprecated AddCommGrpCat.cartesianMonoidalCategory (since := "2025-05-15")]
            def AddCommGrpCat.chosenFiniteProductsAddCommGrp :
            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.

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