Documentation

Mathlib.Algebra.Category.Grp.Biproducts

The category of abelian groups has finite biproducts #

source
instance AddCommGrp.instHasBinaryBiproducts :
CategoryTheory.Limits.HasBinaryBiproducts AddCommGrp
Equations
source
instance AddCommGrp.instHasFiniteBiproducts :
CategoryTheory.Limits.HasFiniteBiproducts AddCommGrp
Equations
source
def AddCommGrp.binaryProductLimitCone (G H : AddCommGrp) :
CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair G H)

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem AddCommGrp.binaryProductLimitCone_isLimit_lift (G H : AddCommGrp) (s : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair G H)) :
    (G.binaryProductLimitCone H).isLimit.lift s = AddMonoidHom.prod (s.π.app { as := CategoryTheory.Limits.WalkingPair.left }) (s.π.app { as := CategoryTheory.Limits.WalkingPair.right })
    source
    @[simp]
    theorem AddCommGrp.binaryProductLimitCone_cone_pt (G H : AddCommGrp) :
    (G.binaryProductLimitCone H).cone.pt = AddCommGrp.of (↑G × ↑H)
    source
    @[simp]
    theorem AddCommGrp.binaryProductLimitCone_cone_π_app_left (G H : AddCommGrp) :
    (G.binaryProductLimitCone H).cone.π.app { as := CategoryTheory.Limits.WalkingPair.left } = AddMonoidHom.fst ↑G ↑H
    source
    @[simp]
    theorem AddCommGrp.binaryProductLimitCone_cone_π_app_right (G H : AddCommGrp) :
    (G.binaryProductLimitCone H).cone.π.app { as := CategoryTheory.Limits.WalkingPair.right } = AddMonoidHom.snd ↑G ↑H
    source
    noncomputable def AddCommGrp.biprodIsoProd (G H : AddCommGrp) :
    G ⊞ H ≅ AddCommGrp.of (↑G × ↑H)

    We verify that the biproduct in AddCommGrp is isomorphic to the cartesian product of the underlying types:

    Equations
    Instances For
      source
      @[simp]
      theorem AddCommGrp.biprodIsoProd_inv_comp_fst (G H : AddCommGrp) :
      CategoryTheory.CategoryStruct.comp (G.biprodIsoProd H).inv CategoryTheory.Limits.biprod.fst = AddMonoidHom.fst ↑G ↑H
      source
      theorem AddCommGrp.biprodIsoProd_inv_comp_fst_apply (G H : AddCommGrp) (x : (CategoryTheory.forget AddCommGrp).obj (AddCommGrp.of (↑G × ↑H))) :
      CategoryTheory.Limits.biprod.fst ((G.biprodIsoProd H).inv x) = (AddMonoidHom.fst ↑G ↑H) x
      source
      @[simp]
      theorem AddCommGrp.biprodIsoProd_inv_comp_snd (G H : AddCommGrp) :
      CategoryTheory.CategoryStruct.comp (G.biprodIsoProd H).inv CategoryTheory.Limits.biprod.snd = AddMonoidHom.snd ↑G ↑H
      source
      theorem AddCommGrp.biprodIsoProd_inv_comp_snd_apply (G H : AddCommGrp) (x : (CategoryTheory.forget AddCommGrp).obj (AddCommGrp.of (↑G × ↑H))) :
      CategoryTheory.Limits.biprod.snd ((G.biprodIsoProd H).inv x) = (AddMonoidHom.snd ↑G ↑H) x
      source
      def AddCommGrp.HasLimit.lift {J : Type w} (f : J → AddCommGrp) (s : CategoryTheory.Limits.Fan f) :
      s.pt ⟶ AddCommGrp.of ((j : J) → ↑(f j))

      The map from an arbitrary cone over an indexed family of abelian groups to the cartesian product of those groups.

      Equations
      • AddCommGrp.HasLimit.lift f s = { toFun := fun (x : ↑s.pt) (j : J) => (s.π.app { as := j }) x, map_zero' := ⋯, map_add' := ⋯ }
      Instances For
        source
        def AddCommGrp.HasLimit.productLimitCone {J : Type w} (f : J → AddCommGrp) :
        CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor f)

        Construct limit data for a product in AddCommGrp, using AddCommGrp.of (∀ j, F.obj j).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem AddCommGrp.HasLimit.productLimitCone_isLimit_lift {J : Type w} (f : J → AddCommGrp) (s : CategoryTheory.Limits.Fan f) :
          (AddCommGrp.HasLimit.productLimitCone f).isLimit.lift s = AddCommGrp.HasLimit.lift f s
          source
          @[simp]
          theorem AddCommGrp.HasLimit.productLimitCone_cone_π {J : Type w} (f : J → AddCommGrp) :
          (AddCommGrp.HasLimit.productLimitCone f).cone.π = CategoryTheory.Discrete.natTrans fun (j : CategoryTheory.Discrete J) => Pi.evalAddMonoidHom (fun (j : J) => ↑(f j)) j.as
          source
          @[simp]
          theorem AddCommGrp.HasLimit.productLimitCone_cone_pt {J : Type w} (f : J → AddCommGrp) :
          (AddCommGrp.HasLimit.productLimitCone f).cone.pt = AddCommGrp.of ((j : J) → ↑(f j))
          source
          noncomputable def AddCommGrp.biproductIsoPi {J : Type} [Finite J] (f : J → AddCommGrp) :
          ⨁ f ≅ AddCommGrp.of ((j : J) → ↑(f j))

          We verify that the biproduct we've just defined is isomorphic to the AddCommGrp structure on the dependent function type.

          Equations
          Instances For
            source
            @[simp]
            theorem AddCommGrp.biproductIsoPi_inv_comp_π {J : Type} [Finite J] (f : J → AddCommGrp) (j : J) :
            CategoryTheory.CategoryStruct.comp (AddCommGrp.biproductIsoPi f).inv (CategoryTheory.Limits.biproduct.π f j) = Pi.evalAddMonoidHom (fun (j : J) => ↑(f j)) j
            source
            theorem AddCommGrp.biproductIsoPi_inv_comp_π_apply {J : Type} [Finite J] (f : J → AddCommGrp) (j : J) (x : (CategoryTheory.forget AddCommGrp).obj (AddCommGrp.of ((j : J) → ↑(f j)))) :
            (CategoryTheory.Limits.biproduct.π f j) ((AddCommGrp.biproductIsoPi f).inv x) = (Pi.evalAddMonoidHom (fun (j : J) => ↑(f j)) j) x