Documentation

Mathlib.Algebra.Category.Grp.ChosenFiniteProducts

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.chosenFiniteProductsGrp :
    CategoryTheory.ChosenFiniteProducts 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
    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.chosenFiniteProductsAddGrp :
      CategoryTheory.ChosenFiniteProducts 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
      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.chosenFiniteProductsCommGrp :
        CategoryTheory.ChosenFiniteProducts 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
        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.chosenFiniteProductsAddCommGrp :
        CategoryTheory.ChosenFiniteProducts AddCommGrp

        We choose AddCommGrp.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.
        Instances For
          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)