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
    @[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.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[implicit_reducible]
    noncomputable instance GrpCat.instBraidedCategory :
    CategoryTheory.BraidedCategory GrpCat
    Equations
    source
    @[implicit_reducible]
    noncomputable instance GrpCat.instBraidedForgetMonoidHomCarrier :
    (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.ConcreteCategory.hom (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_cone_pt (G H : AddGrpCat) :
      (G.binaryProductLimitCone H).cone.pt = of (↑G × ↑H)
      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
      @[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.

      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[implicit_reducible]
      noncomputable instance AddGrpCat.instBraidedCategory :
      CategoryTheory.BraidedCategory AddGrpCat
      Equations
      source
      @[implicit_reducible]
      noncomputable instance AddGrpCat.instBraidedForgetAddMonoidHomCarrier :
      (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.ConcreteCategory.hom (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
        @[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.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[implicit_reducible]
        noncomputable instance CommGrpCat.instBraidedCategory :
        CategoryTheory.BraidedCategory CommGrpCat
        Equations
        source
        @[implicit_reducible]
        noncomputable instance CommGrpCat.instBraidedForgetMonoidHomCarrier :
        (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.ConcreteCategory.hom (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.forget CommGrpCat) G H)) (p, q) = (p, q)
        source
        @[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.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[implicit_reducible]
          noncomputable instance AddCommGrpCat.instBraidedCategory :
          CategoryTheory.BraidedCategory AddCommGrpCat
          Equations
          source
          @[implicit_reducible]
          noncomputable instance AddCommGrpCat.instBraidedForgetAddMonoidHomCarrier :
          (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.ConcreteCategory.hom (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.forget AddCommGrpCat) G H)) (p, q) = (p, q)