Preservation of biproducts

We define the image of a (binary) bicone under a functor that preserves zero morphisms and define classes PreservesBiproduct and PreservesBinaryBiproduct. We then

• show that a functor that preserves biproducts of a two-element type preserves binary biproducts,
• construct the comparison morphisms between the image of a biproduct and the biproduct of the images and show that the biproduct is preserved if one of them is an isomorphism,
• give the canonical isomorphism between the image of a biproduct and the biproduct of the images in case that the biproduct is preserved.

def CategoryTheory.Functor.mapBicone {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} {f : J → C} (b : Limits.Bicone f) : Limits.Bicone (F.obj ∘ f)

The image of a bicone under a functor.

Equations

• F.mapBicone b = { pt := F.obj b.pt, π := fun (j : J) => F.map (b.π j), ι := fun (j : J) => F.map (b.ι j), ι_π := ⋯ }

@[simp]

theorem CategoryTheory.Functor.mapBicone_ι {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} {f : J → C} (b : Limits.Bicone f) (j : J) : (F.mapBicone b).ι j = F.map (b.ι j)

@[simp]

theorem CategoryTheory.Functor.mapBicone_pt {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} {f : J → C} (b : Limits.Bicone f) : (F.mapBicone b).pt = F.obj b.pt

@[simp]

theorem CategoryTheory.Functor.mapBicone_π {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} {f : J → C} (b : Limits.Bicone f) (j : J) : (F.mapBicone b).π j = F.map (b.π j)

theorem CategoryTheory.Functor.mapBicone_whisker {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} {K : Type w₂} {g : K ≃ J} {f : J → C} (c : Limits.Bicone f) : F.mapBicone (c.whisker g) = (F.mapBicone c).whisker g

def CategoryTheory.Functor.mapBinaryBicone {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (b : Limits.BinaryBicone X Y) : Limits.BinaryBicone (F.obj X) (F.obj Y)

The image of a binary bicone under a functor.

Equations

• F.mapBinaryBicone b = (CategoryTheory.Limits.BinaryBicones.functoriality X Y F).obj b

@[simp]

theorem CategoryTheory.Functor.mapBinaryBicone_inl {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (b : Limits.BinaryBicone X Y) : (F.mapBinaryBicone b).inl = F.map b.inl

@[simp]

theorem CategoryTheory.Functor.mapBinaryBicone_snd {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (b : Limits.BinaryBicone X Y) : (F.mapBinaryBicone b).snd = F.map b.snd

@[simp]

theorem CategoryTheory.Functor.mapBinaryBicone_fst {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (b : Limits.BinaryBicone X Y) : (F.mapBinaryBicone b).fst = F.map b.fst

@[simp]

theorem CategoryTheory.Functor.mapBinaryBicone_inr {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (b : Limits.BinaryBicone X Y) : (F.mapBinaryBicone b).inr = F.map b.inr

@[simp]

theorem CategoryTheory.Functor.mapBinaryBicone_pt {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (b : Limits.BinaryBicone X Y) : (F.mapBinaryBicone b).pt = F.obj b.pt

class CategoryTheory.Limits.PreservesBiproduct {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] {J : Type w₁} (f : J → C) (F : Functor C D) [F.PreservesZeroMorphisms] : Prop

A functor F preserves biproducts of f if F maps every bilimit bicone over f to a bilimit bicone over F.obj ∘ f.

• preserves {b : Bicone f} : b.IsBilimit → Nonempty (F.mapBicone b).IsBilimit

  A functor F preserves biproducts of f if F maps every bilimit bicone over f to a bilimit bicone over F.obj ∘ f.

def CategoryTheory.Limits.isBilimitOfPreserves {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] {J : Type w₁} {f : J → C} (F : Functor C D) [F.PreservesZeroMorphisms] [PreservesBiproduct f F] {b : Bicone f} (hb : b.IsBilimit) : (F.mapBicone b).IsBilimit

A functor F preserves biproducts of f if F maps every bilimit bicone over f to a bilimit bicone over F.obj ∘ f.

Equations

• CategoryTheory.Limits.isBilimitOfPreserves F hb = ⋯.some

class CategoryTheory.Limits.PreservesBiproductsOfShape {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (J : Type w₁) (F : Functor C D) [F.PreservesZeroMorphisms] : Prop

A functor F preserves biproducts of shape J if it preserves biproducts of f for every f : J → C.

• preserves {f : J → C} : PreservesBiproduct f F

  A functor F preserves biproducts of shape J if it preserves biproducts of f for every f : J → C.

class CategoryTheory.Limits.PreservesFiniteBiproducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] : Prop

A functor F preserves finite biproducts if it preserves biproducts of shape J whenever J is a fintype.

• preserves {J : Type} [Fintype J] : PreservesBiproductsOfShape J F

  A functor F preserves finite biproducts if it preserves biproducts of shape J whenever J is a fintype.

class CategoryTheory.Limits.PreservesBiproducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] : Prop

A functor F preserves biproducts if it preserves biproducts of any shape J of size w. The usual notion of preservation of biproducts is recovered by choosing w to be the universe of the morphisms of C.

• preserves {J : Type w₁} : PreservesBiproductsOfShape J F

  A functor F preserves biproducts if it preserves biproducts of any shape J of size w. The usual notion of preservation of biproducts is recovered by choosing w to be the universe of the morphisms of C.

theorem CategoryTheory.Limits.preservesBiproducts_shrink {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] [PreservesBiproducts F] : PreservesBiproducts F

Preserving biproducts at a bigger universe level implies preserving biproducts at a smaller universe level.

@[instance 100]

instance CategoryTheory.Limits.preservesFiniteBiproductsOfPreservesBiproducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] [PreservesBiproducts F] : PreservesFiniteBiproducts F

class CategoryTheory.Limits.PreservesBinaryBiproduct {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (X Y : C) (F : Functor C D) [F.PreservesZeroMorphisms] : Prop

A functor F preserves binary biproducts of X and Y if F maps every bilimit bicone over X and Y to a bilimit bicone over F.obj X and F.obj Y.

• preserves {b : BinaryBicone X Y} : b.IsBilimit → Nonempty (F.mapBinaryBicone b).IsBilimit

  A functor F preserves binary biproducts of X and Y if F maps every bilimit bicone over X and Y to a bilimit bicone over F.obj X and F.obj Y.

def CategoryTheory.Limits.isBinaryBilimitOfPreserves {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] {X Y : C} (F : Functor C D) [F.PreservesZeroMorphisms] [PreservesBinaryBiproduct X Y F] {b : BinaryBicone X Y} (hb : b.IsBilimit) : (F.mapBinaryBicone b).IsBilimit

A functor F preserves binary biproducts of X and Y if F maps every bilimit bicone over X and Y to a bilimit bicone over F.obj X and F.obj Y.

Equations

• CategoryTheory.Limits.isBinaryBilimitOfPreserves F hb = ⋯.some

class CategoryTheory.Limits.PreservesBinaryBiproducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] : Prop

A functor F preserves binary biproducts if it preserves the binary biproduct of X and Y for all X and Y.

• preserves {X Y : C} : PreservesBinaryBiproduct X Y F

  A functor F preserves binary biproducts if it preserves the binary biproduct of X and Y for all X and Y.

theorem CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBiproduct {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] (X Y : C) [PreservesBiproduct (pairFunction X Y) F] : PreservesBinaryBiproduct X Y F

A functor that preserves biproducts of a pair preserves binary biproducts.

theorem CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBiproducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] [PreservesBiproductsOfShape WalkingPair F] : PreservesBinaryBiproducts F

A functor that preserves biproducts of a pair preserves binary biproducts.

def CategoryTheory.Functor.biproductComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] : F.obj (⨁ f) ⟶ ⨁ F.obj ∘ f

As for products, any functor between categories with biproducts gives rise to a morphism F.obj (⨁ f) ⟶ ⨁ (F.obj ∘ f).

Equations

• F.biproductComparison f = CategoryTheory.Limits.biproduct.lift fun (j : J) => F.map (CategoryTheory.Limits.biproduct.π f j)

@[simp]

theorem CategoryTheory.Functor.biproductComparison_π {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] (j : J) : CategoryStruct.comp (F.biproductComparison f) (Limits.biproduct.π (F.obj ∘ f) j) = F.map (Limits.biproduct.π f j)

@[simp]

theorem CategoryTheory.Functor.biproductComparison_π_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] (j : J) {Z : D} (h : (F.obj ∘ f) j ⟶ Z) : CategoryStruct.comp (F.biproductComparison f) (CategoryStruct.comp (Limits.biproduct.π (F.obj ∘ f) j) h) = CategoryStruct.comp (F.map (Limits.biproduct.π f j)) h

def CategoryTheory.Functor.biproductComparison' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] : ⨁ F.obj ∘ f ⟶ F.obj (⨁ f)

As for coproducts, any functor between categories with biproducts gives rise to a morphism ⨁ (F.obj ∘ f) ⟶ F.obj (⨁ f)

Equations

• F.biproductComparison' f = CategoryTheory.Limits.biproduct.desc fun (j : J) => F.map (CategoryTheory.Limits.biproduct.ι f j)

@[simp]

theorem CategoryTheory.Functor.ι_biproductComparison' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] (j : J) : CategoryStruct.comp (Limits.biproduct.ι (F.obj ∘ f) j) (F.biproductComparison' f) = F.map (Limits.biproduct.ι f j)

@[simp]

theorem CategoryTheory.Functor.ι_biproductComparison'_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] (j : J) {Z : D} (h : F.obj (⨁ f) ⟶ Z) : CategoryStruct.comp (Limits.biproduct.ι (F.obj ∘ f) j) (CategoryStruct.comp (F.biproductComparison' f) h) = CategoryStruct.comp (F.map (Limits.biproduct.ι f j)) h

@[simp]

theorem CategoryTheory.Functor.biproductComparison'_comp_biproductComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] [F.PreservesZeroMorphisms] : CategoryStruct.comp (F.biproductComparison' f) (F.biproductComparison f) = CategoryStruct.id (⨁ F.obj ∘ f)

The composition in the opposite direction is equal to the identity if and only if F preserves the biproduct, see preservesBiproduct_of_monoBiproductComparison.

@[simp]

theorem CategoryTheory.Functor.biproductComparison'_comp_biproductComparison_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] [F.PreservesZeroMorphisms] {Z : D} (h : ⨁ F.obj ∘ f ⟶ Z) : CategoryStruct.comp (F.biproductComparison' f) (CategoryStruct.comp (F.biproductComparison f) h) = h

def CategoryTheory.Functor.splitEpiBiproductComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] [F.PreservesZeroMorphisms] : SplitEpi (F.biproductComparison f)

biproduct_comparison F f is a split epimorphism.

Equations

• F.splitEpiBiproductComparison f = { section_ := F.biproductComparison' f, id := ⋯ }

@[simp]

theorem CategoryTheory.Functor.splitEpiBiproductComparison_section_ {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] [F.PreservesZeroMorphisms] : (F.splitEpiBiproductComparison f).section_ = F.biproductComparison' f

instance CategoryTheory.Functor.instIsSplitEpiBiproductComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] [F.PreservesZeroMorphisms] : IsSplitEpi (F.biproductComparison f)

def CategoryTheory.Functor.splitMonoBiproductComparison' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] [F.PreservesZeroMorphisms] : SplitMono (F.biproductComparison' f)

biproduct_comparison' F f is a split monomorphism.

Equations

• F.splitMonoBiproductComparison' f = { retraction := F.biproductComparison f, id := ⋯ }

@[simp]

theorem CategoryTheory.Functor.splitMonoBiproductComparison'_retraction {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] [F.PreservesZeroMorphisms] : (F.splitMonoBiproductComparison' f).retraction = F.biproductComparison f

instance CategoryTheory.Functor.instIsSplitMonoBiproductComparison' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] [F.PreservesZeroMorphisms] : IsSplitMono (F.biproductComparison' f)

instance CategoryTheory.Functor.hasBiproduct_of_preserves {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [F.PreservesZeroMorphisms] [Limits.PreservesBiproduct f F] : Limits.HasBiproduct (F.obj ∘ f)

def CategoryTheory.Functor.mapBiproduct {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [F.PreservesZeroMorphisms] [Limits.PreservesBiproduct f F] : F.obj (⨁ f) ≅ ⨁ F.obj ∘ f

If F preserves a biproduct, we get a definitionally nice isomorphism F.obj (⨁ f) ≅ ⨁ (F.obj ∘ f).

Equations

• F.mapBiproduct f = CategoryTheory.Limits.biproduct.uniqueUpToIso (F.obj ∘ f) (CategoryTheory.Limits.isBilimitOfPreserves F (CategoryTheory.Limits.biproduct.isBilimit f))

theorem CategoryTheory.Functor.mapBiproduct_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [F.PreservesZeroMorphisms] [Limits.PreservesBiproduct f F] : (F.mapBiproduct f).hom = Limits.biproduct.lift fun (j : J) => F.map (Limits.biproduct.π f j)

theorem CategoryTheory.Functor.mapBiproduct_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [F.PreservesZeroMorphisms] [Limits.PreservesBiproduct f F] : (F.mapBiproduct f).inv = Limits.biproduct.desc fun (j : J) => F.map (Limits.biproduct.ι f j)

def CategoryTheory.Functor.biprodComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] : F.obj (X ⊞ Y) ⟶ F.obj X ⊞ F.obj Y

As for products, any functor between categories with binary biproducts gives rise to a morphism F.obj (X ⊞ Y) ⟶ F.obj X ⊞ F.obj Y.

Equations

• F.biprodComparison X Y = CategoryTheory.Limits.biprod.lift (F.map CategoryTheory.Limits.biprod.fst) (F.map CategoryTheory.Limits.biprod.snd)

@[simp]

theorem CategoryTheory.Functor.biprodComparison_fst {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] : CategoryStruct.comp (F.biprodComparison X Y) Limits.biprod.fst = F.map Limits.biprod.fst

@[simp]

theorem CategoryTheory.Functor.biprodComparison_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] {Z : D} (h : F.obj X ⟶ Z) : CategoryStruct.comp (F.biprodComparison X Y) (CategoryStruct.comp Limits.biprod.fst h) = CategoryStruct.comp (F.map Limits.biprod.fst) h

@[simp]

theorem CategoryTheory.Functor.biprodComparison_snd {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] : CategoryStruct.comp (F.biprodComparison X Y) Limits.biprod.snd = F.map Limits.biprod.snd

@[simp]

theorem CategoryTheory.Functor.biprodComparison_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] {Z : D} (h : F.obj Y ⟶ Z) : CategoryStruct.comp (F.biprodComparison X Y) (CategoryStruct.comp Limits.biprod.snd h) = CategoryStruct.comp (F.map Limits.biprod.snd) h

def CategoryTheory.Functor.biprodComparison' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] : F.obj X ⊞ F.obj Y ⟶ F.obj (X ⊞ Y)

As for coproducts, any functor between categories with binary biproducts gives rise to a morphism F.obj X ⊞ F.obj Y ⟶ F.obj (X ⊞ Y).

Equations

• F.biprodComparison' X Y = CategoryTheory.Limits.biprod.desc (F.map CategoryTheory.Limits.biprod.inl) (F.map CategoryTheory.Limits.biprod.inr)

@[simp]

theorem CategoryTheory.Functor.inl_biprodComparison' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] : CategoryStruct.comp Limits.biprod.inl (F.biprodComparison' X Y) = F.map Limits.biprod.inl

@[simp]

theorem CategoryTheory.Functor.inl_biprodComparison'_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] {Z : D} (h : F.obj (X ⊞ Y) ⟶ Z) : CategoryStruct.comp Limits.biprod.inl (CategoryStruct.comp (F.biprodComparison' X Y) h) = CategoryStruct.comp (F.map Limits.biprod.inl) h

@[simp]

theorem CategoryTheory.Functor.inr_biprodComparison' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] : CategoryStruct.comp Limits.biprod.inr (F.biprodComparison' X Y) = F.map Limits.biprod.inr

@[simp]

theorem CategoryTheory.Functor.inr_biprodComparison'_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] {Z : D} (h : F.obj (X ⊞ Y) ⟶ Z) : CategoryStruct.comp Limits.biprod.inr (CategoryStruct.comp (F.biprodComparison' X Y) h) = CategoryStruct.comp (F.map Limits.biprod.inr) h

@[simp]

theorem CategoryTheory.Functor.biprodComparison'_comp_biprodComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [F.PreservesZeroMorphisms] : CategoryStruct.comp (F.biprodComparison' X Y) (F.biprodComparison X Y) = CategoryStruct.id (F.obj X ⊞ F.obj Y)

The composition in the opposite direction is equal to the identity if and only if F preserves the biproduct, see preservesBinaryBiproduct_of_monoBiprodComparison.

@[simp]

theorem CategoryTheory.Functor.biprodComparison'_comp_biprodComparison_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [F.PreservesZeroMorphisms] {Z : D} (h : F.obj X ⊞ F.obj Y ⟶ Z) : CategoryStruct.comp (F.biprodComparison' X Y) (CategoryStruct.comp (F.biprodComparison X Y) h) = h

def CategoryTheory.Functor.splitEpiBiprodComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [F.PreservesZeroMorphisms] : SplitEpi (F.biprodComparison X Y)

biprodComparison F X Y is a split epi.

Equations

• F.splitEpiBiprodComparison X Y = { section_ := F.biprodComparison' X Y, id := ⋯ }

@[simp]

theorem CategoryTheory.Functor.splitEpiBiprodComparison_section_ {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [F.PreservesZeroMorphisms] : (F.splitEpiBiprodComparison X Y).section_ = F.biprodComparison' X Y

instance CategoryTheory.Functor.instIsSplitEpiBiprodComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [F.PreservesZeroMorphisms] : IsSplitEpi (F.biprodComparison X Y)

def CategoryTheory.Functor.splitMonoBiprodComparison' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [F.PreservesZeroMorphisms] : SplitMono (F.biprodComparison' X Y)

biprodComparison' F X Y is a split mono.

Equations

• F.splitMonoBiprodComparison' X Y = { retraction := F.biprodComparison X Y, id := ⋯ }

@[simp]

theorem CategoryTheory.Functor.splitMonoBiprodComparison'_retraction {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [F.PreservesZeroMorphisms] : (F.splitMonoBiprodComparison' X Y).retraction = F.biprodComparison X Y

instance CategoryTheory.Functor.instIsSplitMonoBiprodComparison' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [F.PreservesZeroMorphisms] : IsSplitMono (F.biprodComparison' X Y)

instance CategoryTheory.Functor.hasBinaryBiproduct_of_preserves {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [F.PreservesZeroMorphisms] [Limits.PreservesBinaryBiproduct X Y F] : Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)

def CategoryTheory.Functor.mapBiprod {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [F.PreservesZeroMorphisms] [Limits.PreservesBinaryBiproduct X Y F] : F.obj (X ⊞ Y) ≅ F.obj X ⊞ F.obj Y

If F preserves a binary biproduct, we get a definitionally nice isomorphism F.obj (X ⊞ Y) ≅ F.obj X ⊞ F.obj Y.

Equations

• F.mapBiprod X Y = CategoryTheory.Limits.biprod.uniqueUpToIso (F.obj X) (F.obj Y) (CategoryTheory.Limits.isBinaryBilimitOfPreserves F (CategoryTheory.Limits.BinaryBiproduct.isBilimit X Y))

theorem CategoryTheory.Functor.mapBiprod_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [F.PreservesZeroMorphisms] [Limits.PreservesBinaryBiproduct X Y F] : (F.mapBiprod X Y).hom = Limits.biprod.lift (F.map Limits.biprod.fst) (F.map Limits.biprod.snd)

theorem CategoryTheory.Functor.mapBiprod_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [F.PreservesZeroMorphisms] [Limits.PreservesBinaryBiproduct X Y F] : (F.mapBiprod X Y).inv = Limits.biprod.desc (F.map Limits.biprod.inl) (F.map Limits.biprod.inr)

theorem CategoryTheory.Limits.biproduct.map_lift_mapBiprod {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} (f : J → C) [HasBiproduct f] [PreservesBiproduct f F] {W : C} (g : (j : J) → W ⟶ f j) : CategoryStruct.comp (F.map (lift g)) (F.mapBiproduct f).hom = lift fun (j : J) => F.map (g j)

theorem CategoryTheory.Limits.biproduct.mapBiproduct_inv_map_desc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} (f : J → C) [HasBiproduct f] [PreservesBiproduct f F] {W : C} (g : (j : J) → f j ⟶ W) : CategoryStruct.comp (F.mapBiproduct f).inv (F.map (desc g)) = desc fun (j : J) => F.map (g j)

theorem CategoryTheory.Limits.biproduct.mapBiproduct_hom_desc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} (f : J → C) [HasBiproduct f] [PreservesBiproduct f F] {W : C} (g : (j : J) → f j ⟶ W) : CategoryStruct.comp (F.mapBiproduct f).hom (desc fun (j : J) => F.map (g j)) = F.map (desc g)

theorem CategoryTheory.Limits.biprod.map_lift_mapBiprod {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] (X Y : C) [HasBinaryBiproduct X Y] [PreservesBinaryBiproduct X Y F] {W : C} (f : W ⟶ X) (g : W ⟶ Y) : CategoryStruct.comp (F.map (lift f g)) (F.mapBiprod X Y).hom = lift (F.map f) (F.map g)

theorem CategoryTheory.Limits.biprod.lift_mapBiprod {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] (X Y : C) [HasBinaryBiproduct X Y] [PreservesBinaryBiproduct X Y F] {W : C} (f : W ⟶ X) (g : W ⟶ Y) : CategoryStruct.comp (lift (F.map f) (F.map g)) (F.mapBiprod X Y).inv = F.map (lift f g)

theorem CategoryTheory.Limits.biprod.mapBiprod_inv_map_desc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] (X Y : C) [HasBinaryBiproduct X Y] [PreservesBinaryBiproduct X Y F] {W : C} (f : X ⟶ W) (g : Y ⟶ W) : CategoryStruct.comp (F.mapBiprod X Y).inv (F.map (desc f g)) = desc (F.map f) (F.map g)

theorem CategoryTheory.Limits.biprod.mapBiprod_hom_desc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] (X Y : C) [HasBinaryBiproduct X Y] [PreservesBinaryBiproduct X Y F] {W : C} (f : X ⟶ W) (g : Y ⟶ W) : CategoryStruct.comp (F.mapBiprod X Y).hom (desc (F.map f) (F.map g)) = F.map (desc f g)