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.

@[simp]

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

@[simp]

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

@[simp]

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

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

The image of a bicone under a functor.

Equations

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The image of a binary bicone under a functor.

Equations

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

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

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 : CategoryTheory.Limits.Bicone f} → CategoryTheory.Limits.Bicone.IsBilimit b → CategoryTheory.Limits.Bicone.IsBilimit (CategoryTheory.Functor.mapBicone F b)

  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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁} {f : J → C} (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Limits.PreservesBiproduct f F] {b : CategoryTheory.Limits.Bicone f} (hb : CategoryTheory.Limits.Bicone.IsBilimit b) : CategoryTheory.Limits.Bicone.IsBilimit (CategoryTheory.Functor.mapBicone F b)

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 = CategoryTheory.Limits.PreservesBiproduct.preserves hb

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

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

• preserves : {f : J → C} → CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] : Type (max (max (max (max 1 u₁) u₂) v₁) v₂)

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

• preserves : {J : Type} → [inst : Fintype J] → CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] : Type (max (max (max (max u₁ u₂) v₁) v₂) (w₁ + 1))

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₁} → CategoryTheory.Limits.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.

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

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

Equations

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

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

Equations

• CategoryTheory.Limits.preservesFiniteBiproductsOfPreservesBiproducts F = { preserves := fun {J : Type} (x : Fintype J) => inferInstance }

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

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 : CategoryTheory.Limits.BinaryBicone X Y} → CategoryTheory.Limits.BinaryBicone.IsBilimit b → CategoryTheory.Limits.BinaryBicone.IsBilimit (CategoryTheory.Functor.mapBinaryBicone F b)

  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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {X : C} {Y : C} (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Limits.PreservesBinaryBiproduct X Y F] {b : CategoryTheory.Limits.BinaryBicone X Y} (hb : CategoryTheory.Limits.BinaryBicone.IsBilimit b) : CategoryTheory.Limits.BinaryBicone.IsBilimit (CategoryTheory.Functor.mapBinaryBicone F b)

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 = CategoryTheory.Limits.PreservesBinaryBiproduct.preserves hb

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

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} → CategoryTheory.Limits.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.

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

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

Equations

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

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

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

Equations

• CategoryTheory.Limits.preservesBinaryBiproductsOfPreservesBiproducts F = { preserves := fun {X : C} (Y : C) => CategoryTheory.Limits.preservesBinaryBiproductOfPreservesBiproduct F X Y }

def CategoryTheory.Functor.biproductComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁} (F : CategoryTheory.Functor C D) (f : J → C) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.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

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

@[simp]

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

@[simp]

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

def CategoryTheory.Functor.biproductComparison' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁} (F : CategoryTheory.Functor C D) (f : J → C) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Functor.biproductComparison'_comp_biproductComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁} (F : CategoryTheory.Functor C D) (f : J → C) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)] [CategoryTheory.Functor.PreservesZeroMorphisms F] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.biproductComparison' F f) (CategoryTheory.Functor.biproductComparison F f) = CategoryTheory.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.splitEpiBiproductComparison_section_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁} (F : CategoryTheory.Functor C D) (f : J → C) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)] [CategoryTheory.Functor.PreservesZeroMorphisms F] : (CategoryTheory.Functor.splitEpiBiproductComparison F f).section_ = CategoryTheory.Functor.biproductComparison' F f

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

biproduct_comparison F f is a split epimorphism.

Equations

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

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

Equations

• ⋯ = ⋯

@[simp]

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

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

biproduct_comparison' F f is a split monomorphism.

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

def CategoryTheory.Functor.mapBiproduct {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁} (F : CategoryTheory.Functor C D) (f : J → C) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.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

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

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

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

def CategoryTheory.Functor.biprodComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] [CategoryTheory.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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Functor.biprodComparison' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] [CategoryTheory.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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Functor.biprodComparison'_comp_biprodComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] [CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [CategoryTheory.Functor.PreservesZeroMorphisms F] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.biprodComparison' F X Y) (CategoryTheory.Functor.biprodComparison F X Y) = CategoryTheory.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.splitEpiBiprodComparison_section_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] [CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [CategoryTheory.Functor.PreservesZeroMorphisms F] : (CategoryTheory.Functor.splitEpiBiprodComparison F X Y).section_ = CategoryTheory.Functor.biprodComparison' F X Y

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

biprodComparison F X Y is a split epi.

Equations

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

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

Equations

• ⋯ = ⋯

@[simp]

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

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

biprodComparison' F X Y is a split mono.

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

def CategoryTheory.Functor.mapBiprod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.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

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

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

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

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

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

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

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

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

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

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