Documentation

Mathlib.Algebra.Category.Grp.Biproducts

The category of abelian groups has finite biproducts #

source
instance AddCommGrp.instHasBinaryBiproducts :
CategoryTheory.Limits.HasBinaryBiproducts AddCommGrp
source
instance AddCommGrp.instHasFiniteBiproducts :
CategoryTheory.Limits.HasFiniteBiproducts AddCommGrp
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
    Instances For
      source
      @[simp]
      theorem AddCommGrp.binaryProductLimitCone_isLimit_lift (G H : AddCommGrp) (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 AddCommGrp.binaryProductLimitCone_cone_pt (G H : AddCommGrp) :
      (G.binaryProductLimitCone H).cone.pt = of (↑G × ↑H)
      source
      @[simp]
      theorem AddCommGrp.binaryProductLimitCone_cone_π_app_left (G H : AddCommGrp) :
      (G.binaryProductLimitCone H).cone.π.app { as := CategoryTheory.Limits.WalkingPair.left } = ofHom (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 } = ofHom (AddMonoidHom.snd ↑G ↑H)
      source
      noncomputable def AddCommGrp.biprodIsoProd (G H : AddCommGrp) :
      G ⊞ H ≅ 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 = ofHom (AddMonoidHom.fst ↑G ↑H)
          source
          theorem AddCommGrp.biprodIsoProd_inv_comp_fst_apply (G H : AddCommGrp) (x : CategoryTheory.ToType (of (↑G × ↑H))) :
          (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.biprod.fst) ((CategoryTheory.ConcreteCategory.hom (G.biprodIsoProd H).inv) x) = x.1
          source
          @[simp]
          theorem AddCommGrp.biprodIsoProd_inv_comp_snd (G H : AddCommGrp) :
          CategoryTheory.CategoryStruct.comp (G.biprodIsoProd H).inv CategoryTheory.Limits.biprod.snd = ofHom (AddMonoidHom.snd ↑G ↑H)
          source
          theorem AddCommGrp.biprodIsoProd_inv_comp_snd_apply (G H : AddCommGrp) (x : CategoryTheory.ToType (of (↑G × ↑H))) :
          (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.biprod.snd) ((CategoryTheory.ConcreteCategory.hom (G.biprodIsoProd H).inv) x) = x.2
          source
          def AddCommGrp.HasLimit.lift {J : Type w} (f : J → AddCommGrp) (s : CategoryTheory.Limits.Fan f) :
          s.pt ⟶ 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
            Instances For
              source
              @[simp]
              theorem AddCommGrp.HasLimit.lift_hom_apply {J : Type w} (f : J → AddCommGrp) (s : CategoryTheory.Limits.Fan f) (x : ↑s.1) (j : J) :
              (Hom.hom (lift f s)) x j = (CategoryTheory.ConcreteCategory.hom (s.π.app { as := j })) x
              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
                Instances For
                  source
                  @[simp]
                  theorem AddCommGrp.HasLimit.productLimitCone_isLimit_lift {J : Type w} (f : J → AddCommGrp) (s : CategoryTheory.Limits.Fan f) :
                  (productLimitCone f).isLimit.lift s = lift f s
                  source
                  @[simp]
                  theorem AddCommGrp.HasLimit.productLimitCone_cone_π {J : Type w} (f : J → AddCommGrp) :
                  (productLimitCone f).cone.π = CategoryTheory.Discrete.natTrans fun (j : CategoryTheory.Discrete J) => ofHom (Pi.evalAddMonoidHom (fun (j : J) => ↑(f j)) j.as)
                  source
                  @[simp]
                  theorem AddCommGrp.HasLimit.productLimitCone_cone_pt_coe {J : Type w} (f : J → AddCommGrp) :
                  ↑(productLimitCone f).cone.pt = ((j : J) → ↑(f j))
                  source
                  noncomputable def AddCommGrp.biproductIsoPi {J : Type} [Finite J] (f : J → AddCommGrp) :
                  ⨁ f ≅ 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 (biproductIsoPi f).inv (CategoryTheory.Limits.biproduct.π f j) = ofHom (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.ToType (of ((j : J) → ↑(f j)))) :
                      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.biproduct.π f j)) ((CategoryTheory.ConcreteCategory.hom (biproductIsoPi f).inv) x) = x j