Biproducts in functor categories

We show that if C has binary biproducts, then the functor category D ⥤ C also has binary biproducts (CategoryTheory.Limits.BinaryBiproduct.functorCategoryHasBinaryBiproducts).

noncomputable def CategoryTheory.Limits.pointwiseBinaryBicone {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {D : Type u_2} [Category.{v_2, u_2} D] (F G : Functor D C) : BinaryBicone F G

The binary bicone associated to the biproduct of functors F and G

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.pointwiseBinaryBicone_snd_app {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {D : Type u_2} [Category.{v_2, u_2} D] (F G : Functor D C) (X : D) : (pointwiseBinaryBicone F G).snd.app X = biprod.snd

@[simp]

theorem CategoryTheory.Limits.pointwiseBinaryBicone_inl_app {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {D : Type u_2} [Category.{v_2, u_2} D] (F G : Functor D C) (X : D) : (pointwiseBinaryBicone F G).inl.app X = biprod.inl

@[simp]

theorem CategoryTheory.Limits.pointwiseBinaryBicone_fst_app {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {D : Type u_2} [Category.{v_2, u_2} D] (F G : Functor D C) (X : D) : (pointwiseBinaryBicone F G).fst.app X = biprod.fst

@[simp]

theorem CategoryTheory.Limits.pointwiseBinaryBicone_inr_app {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {D : Type u_2} [Category.{v_2, u_2} D] (F G : Functor D C) (X : D) : (pointwiseBinaryBicone F G).inr.app X = biprod.inr

@[simp]

theorem CategoryTheory.Limits.pointwiseBinaryBicone_pt_obj {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {D : Type u_2} [Category.{v_2, u_2} D] (F G : Functor D C) (P : D) : (pointwiseBinaryBicone F G).pt.obj P = (F.obj P ⊞ G.obj P)

@[simp]

theorem CategoryTheory.Limits.pointwiseBinaryBicone_pt_map {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {D : Type u_2} [Category.{v_2, u_2} D] (F G : Functor D C) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : (pointwiseBinaryBicone F G).pt.map f = biprod.map (F.map f) (G.map f)

noncomputable def CategoryTheory.Limits.pointwiseBinaryBicone.isBilimit {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {D : Type u_2} [Category.{v_2, u_2} D] (F G : Functor D C) : (pointwiseBinaryBicone F G).IsBilimit

The bicone associated with F and G is a bilimit bicone.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.pointwiseBinaryBicone.isBilimit_isColimit {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {D : Type u_2} [Category.{v_2, u_2} D] (F G : Functor D C) : (isBilimit F G).isColimit = evaluationJointlyReflectsColimits (pointwiseBinaryBicone F G).toCocone fun (d : D) => (IsColimit.equivOfNatIsoOfIso (pairComp F G ((evaluation D C).obj d)).symm (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone (((evaluation D C).obj d).mapCocone (pointwiseBinaryBicone F G).toCocone) (Cocone.ext (Iso.refl ((Cocone.precompose (pairComp F G ((evaluation D C).obj d)).symm.inv).obj (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).pt) ⋯)) (BinaryBiproduct.isColimit (F.obj d) (G.obj d))

@[simp]

theorem CategoryTheory.Limits.pointwiseBinaryBicone.isBilimit_isLimit {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {D : Type u_2} [Category.{v_2, u_2} D] (F G : Functor D C) : (isBilimit F G).isLimit = evaluationJointlyReflectsLimits (pointwiseBinaryBicone F G).toCone fun (d : D) => (IsLimit.equivOfNatIsoOfIso (pairComp F G ((evaluation D C).obj d)).symm (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone (((evaluation D C).obj d).mapCone (pointwiseBinaryBicone F G).toCone) (Cone.ext (Iso.refl ((Cone.postcompose (pairComp F G ((evaluation D C).obj d)).symm.hom).obj (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone).pt) ⋯)) (BinaryBiproduct.isLimit (F.obj d) (G.obj d))

noncomputable def CategoryTheory.Limits.pointwiseBinaryBiproductData {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {D : Type u_2} [Category.{v_2, u_2} D] (F G : Functor D C) : BinaryBiproductData F G

Construction of the binary biproduct data for functors F and G

Equations

• CategoryTheory.Limits.pointwiseBinaryBiproductData F G = { bicone := CategoryTheory.Limits.pointwiseBinaryBicone F G, isBilimit := CategoryTheory.Limits.pointwiseBinaryBicone.isBilimit F G }

@[simp]

theorem CategoryTheory.Limits.pointwiseBinaryBiproductData_bicone {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {D : Type u_2} [Category.{v_2, u_2} D] (F G : Functor D C) : (pointwiseBinaryBiproductData F G).bicone = pointwiseBinaryBicone F G

instance CategoryTheory.Limits.functorCategoryHasBinaryBiproducts {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {D : Type u_2} [Category.{v_2, u_2} D] : HasBinaryBiproducts (Functor D C)

If C has binary biproducts, then the functor category D ⥤ C does too.