Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts

CategoryTheory.Functor.mapBicone definition

{f : J → C} (b : Bicone f) : Bicone (F.obj ∘ f)

Full source

/-- The image of a bicone under a functor. -/
@[simps]
def mapBicone {f : J → C} (b : Bicone f) : Bicone (F.obj ∘ f) where
  pt := F.obj b.pt
  π j := F.map (b.π j)
  ι j := F.map (b.ι j)
  ι_π j j' := by
    rw [← F.map_comp]
    split_ifs with h
    · subst h
      simp only [bicone_ι_π_self, CategoryTheory.Functor.map_id, eqToHom_refl]; dsimp
    · rw [bicone_ι_π_ne _ h, F.map_zero]

Image of a bicone under a functor

Informal description

Given a functor $ F : C \to D $ that preserves zero morphisms, and a bicone $ b $ over a family of objects $ f : J \to C $, the image of $ b $ under $ F $ is a bicone over the family $ F \circ f : J \to D $, where: - The point of the new bicone is $ F(b.\text{pt}) $ - The projection morphisms are $ F(b.\pi_j) $ for each $ j \in J $ - The injection morphisms are $ F(b.\iota_j) $ for each $ j \in J $

CategoryTheory.Functor.mapBicone_whisker theorem

{K : Type w₂} {g : K ≃ J} {f : J → C} (c : Bicone f) : F.mapBicone (c.whisker g) = (F.mapBicone c).whisker g

Full source

theorem mapBicone_whisker {K : Type w₂} {g : K ≃ J} {f : J → C} (c : Bicone f) :
    F.mapBicone (c.whisker g) = (F.mapBicone c).whisker g :=
  rfl

Functoriality of Bicone Whiskering: $F(c \circ g) = (Fc) \circ g$

Informal description

Let $C$ and $D$ be categories with zero morphisms, and let $F : C \to D$ be a functor that preserves zero morphisms. Given an indexing type $J$, a family of objects $f : J \to C$, a bicone $c$ over $f$, and an equivalence $g : K \simeq J$ between indexing types, the image under $F$ of the whiskered bicone $c.whisker\, g$ is equal to the whiskering of $F.mapBicone\, c$ along $g$.

CategoryTheory.Functor.mapBinaryBicone definition

{X Y : C} (b : BinaryBicone X Y) : BinaryBicone (F.obj X) (F.obj Y)

Full source

/-- The image of a binary bicone under a functor. -/
@[simps!]
def mapBinaryBicone {X Y : C} (b : BinaryBicone X Y) : BinaryBicone (F.obj X) (F.obj Y) :=
  (BinaryBicones.functoriality _ _ F).obj b

Image of a binary bicone under a functor

Informal description

Given a functor $ F : C \to D $ that preserves zero morphisms, and a binary bicone $ b $ over objects $ X $ and $ Y $ in $ C $, the image of $ b $ under $ F $ is a binary bicone over $ F(X) $ and $ F(Y) $ in $ D $. This construction is obtained by applying the functoriality of binary bicones to $ b $.

CategoryTheory.Limits.PreservesBiproduct structure

(f : J → C) (F : C ⥤ D) [PreservesZeroMorphisms F]

Full source

/-- A functor `F` preserves biproducts of `f` if `F` maps every bilimit bicone over `f` to a
    bilimit bicone over `F.obj ∘ f`. -/
class PreservesBiproduct (f : J → C) (F : C ⥤ D) [PreservesZeroMorphisms F] : Prop where
  preserves : ∀ {b : Bicone f}, b.IsBilimit → Nonempty (F.mapBicone b).IsBilimit

Biproduct-preserving functor

Informal description

A functor $ F : C \to D $ preserves the biproduct of a family of objects $ f : J \to C $ if $ F $ maps every bilimit bicone over $ f $ to a bilimit bicone over $ F \circ f $. This means that $ F $ preserves both the product and coproduct structures that constitute the biproduct of $ f $.

CategoryTheory.Limits.isBilimitOfPreserves definition

 {f : J → C} (F : C ⥤ D) [PreservesZeroMorphisms F] [PreservesBiproduct f F] {b : Bicone f} (hb : b.IsBilimit) :
  (F.mapBicone b).IsBilimit

Full source

/-- A functor `F` preserves biproducts of `f` if `F` maps every bilimit bicone over `f` to a
    bilimit bicone over `F.obj ∘ f`. -/
def isBilimitOfPreserves {f : J → C} (F : C ⥤ D) [PreservesZeroMorphisms F] [PreservesBiproduct f F]
    {b : Bicone f} (hb : b.IsBilimit) : (F.mapBicone b).IsBilimit :=
  (PreservesBiproduct.preserves hb).some

Preservation of bilimit bicones under biproduct-preserving functors

Informal description

Given a functor $ F : C \to D $ that preserves zero morphisms and biproducts of a family $ f : J \to C $, and a bilimit bicone $ b $ over $ f $, the image of $ b $ under $ F $ is a bilimit bicone over $ F \circ f $.

CategoryTheory.Limits.PreservesBiproductsOfShape structure

(F : C ⥤ D) [PreservesZeroMorphisms F]

Full source

/-- A functor `F` preserves biproducts of shape `J` if it preserves biproducts of `f` for every
    `f : J → C`. -/
class PreservesBiproductsOfShape (F : C ⥤ D) [PreservesZeroMorphisms F] : Prop where
  preserves : ∀ {f : J → C}, PreservesBiproduct f F

Functor preserving biproducts of a given shape

Informal description

A functor $ F : C \to D $ preserves biproducts of shape $ J $ if for every family of objects $ f : J \to C $, the functor $ F $ maps the biproduct of $ f $ in $ C $ to the biproduct of $ F \circ f $ in $ D $. This requires that $ F $ preserves zero morphisms.

CategoryTheory.Limits.PreservesFiniteBiproducts structure

(F : C ⥤ D) [PreservesZeroMorphisms F]

Full source

/-- A functor `F` preserves finite biproducts if it preserves biproducts of shape `J`
whenever `J` is a finite type. -/
class PreservesFiniteBiproducts (F : C ⥤ D) [PreservesZeroMorphisms F] : Prop where
  preserves : ∀ {J : Type} [Finite J], PreservesBiproductsOfShape J F

Functor preserving finite biproducts

Informal description

A functor $ F : C \to D $ preserves finite biproducts if it preserves biproducts of shape $ J $ for every finite type $ J $. This means that $ F $ maps biproducts in $ C $ to biproducts in $ D $ whenever the indexing type $ J $ is finite.

CategoryTheory.Limits.PreservesBiproducts structure

(F : C ⥤ D) [PreservesZeroMorphisms F]

Full source

/-- 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`. -/
class PreservesBiproducts (F : C ⥤ D) [PreservesZeroMorphisms F] : Prop where
  preserves : ∀ {J : Type w₁}, PreservesBiproductsOfShape J F

Biproduct-preserving functor

Informal description

A functor $ F : C \to D $ between categories $ C $ and $ D $ preserves biproducts if it preserves biproducts of any shape $ J $ (of size $ w $), meaning that for any family of objects $ f : J \to C $, the functor $ F $ maps the biproduct of $ f $ in $ C $ to the biproduct of $ F \circ f $ in $ D $. This requires that $ F $ preserves zero morphisms. The standard notion of biproduct preservation is obtained by taking $ w $ to be the universe of the morphisms of $ C $.

CategoryTheory.Limits.preservesBiproducts_shrink theorem

(F : C ⥤ D) [PreservesZeroMorphisms F] [PreservesBiproducts.{max w₁ w₂} F] : PreservesBiproducts.{w₁} F

Full source

/-- Preserving biproducts at a bigger universe level implies preserving biproducts at a
smaller universe level. -/
lemma preservesBiproducts_shrink (F : C ⥤ D) [PreservesZeroMorphisms F]
    [PreservesBiproducts.{max w₁ w₂} F] : PreservesBiproducts.{w₁} F :=
  ⟨fun {_} =>
    ⟨fun {_} =>
      ⟨fun {b} ib =>
        ⟨((F.mapBicone b).whiskerIsBilimitIff _).toFun
          (isBilimitOfPreserves F ((b.whiskerIsBilimitIff Equiv.ulift.{w₂}).invFun ib))⟩⟩⟩⟩

Preservation of Biproducts Under Universe Shrinkage

Informal description

Let $F : C \to D$ be a functor between categories $C$ and $D$ that preserves zero morphisms. If $F$ preserves biproducts of any shape (indexed by types in universe level $\max(w_1, w_2)$), then $F$ also preserves biproducts of any shape indexed by types in the smaller universe level $w_1$.

CategoryTheory.Limits.preservesFiniteBiproductsOfPreservesBiproducts instance

(F : C ⥤ D) [PreservesZeroMorphisms F] [PreservesBiproducts.{w₁} F] : PreservesFiniteBiproducts F

Full source

instance (priority := 100) preservesFiniteBiproductsOfPreservesBiproducts (F : C ⥤ D)
    [PreservesZeroMorphisms F] [PreservesBiproducts.{w₁} F] : PreservesFiniteBiproducts F where
  preserves {J} _ := by letI := preservesBiproducts_shrink.{0} F; infer_instance

Preservation of Finite Biproducts by Biproduct-Preserving Functors

Informal description

For any functor $F : C \to D$ between categories $C$ and $D$ that preserves zero morphisms and preserves biproducts of any shape (indexed by types in universe level $w_1$), $F$ also preserves finite biproducts. This means that $F$ maps biproducts in $C$ to biproducts in $D$ whenever the indexing type is finite.

CategoryTheory.Limits.PreservesBinaryBiproduct structure

(X Y : C) (F : C ⥤ D) [PreservesZeroMorphisms F]

Full source

/-- 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`. -/
class PreservesBinaryBiproduct (X Y : C) (F : C ⥤ D) [PreservesZeroMorphisms F] : Prop where
  preserves : ∀ {b : BinaryBicone X Y}, b.IsBilimit → Nonempty ((F.mapBinaryBicone b).IsBilimit)

Preservation of Binary Biproducts by a Functor

Informal description

A functor $ F : C \to D $ between categories $ C $ and $ D $ preserves binary biproducts of objects $ X $ and $ Y $ in $ C $ if, for every bilimit bicone over $ X $ and $ Y $, the image of this bicone under $ F $ is a bilimit bicone over $ F(X) $ and $ F(Y) $ in $ D $. This means that $ F $ maps the biproduct structure of $ X $ and $ Y $ to the biproduct structure of $ F(X) $ and $ F(Y) $, preserving the universal properties of the biproduct.

CategoryTheory.Limits.isBinaryBilimitOfPreserves definition

 {X Y : C} (F : C ⥤ D) [PreservesZeroMorphisms F] [PreservesBinaryBiproduct X Y F] {b : BinaryBicone X Y}
  (hb : b.IsBilimit) : (F.mapBinaryBicone b).IsBilimit

Full source

/-- 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 isBinaryBilimitOfPreserves {X Y : C} (F : C ⥤ D) [PreservesZeroMorphisms F]
    [PreservesBinaryBiproduct X Y F] {b : BinaryBicone X Y} (hb : b.IsBilimit) :
    (F.mapBinaryBicone b).IsBilimit :=
  (PreservesBinaryBiproduct.preserves hb).some

Preservation of bilimit property under a functor preserving binary biproducts

Informal description

Given a functor $ F : C \to D $ that preserves zero morphisms and binary biproducts of objects $ X $ and $ Y $ in $ C $, and given a bilimit bicone $ b $ over $ X $ and $ Y $, the image of $ b $ under $ F $ is a bilimit bicone over $ F(X) $ and $ F(Y) $ in $ D $. This means that $ F $ preserves the universal property of the biproduct structure when applied to $ b $.

CategoryTheory.Limits.PreservesBinaryBiproducts structure

(F : C ⥤ D) [PreservesZeroMorphisms F]

Full source

/-- A functor `F` preserves binary biproducts if it preserves the binary biproduct of `X` and `Y`
    for all `X` and `Y`. -/
class PreservesBinaryBiproducts (F : C ⥤ D) [PreservesZeroMorphisms F] : Prop where
  preserves : ∀ {X Y : C}, PreservesBinaryBiproduct X Y F := by infer_instance

Functor Preserving Binary Biproducts

Informal description

A functor $ F : C \to D $ between categories $ C $ and $ D $ preserves binary biproducts if it preserves the binary biproduct of any two objects $ X $ and $ Y $ in $ C $. This means that for every pair of objects $ X $ and $ Y $ in $ C $, the functor $ F $ maps their biproduct structure in $ C $ to a biproduct structure in $ D $, preserving the universal properties of the biproduct.

CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBiproduct theorem

 (F : C ⥤ D) [PreservesZeroMorphisms F] (X Y : C) [PreservesBiproduct (pairFunction X Y) F] :
  PreservesBinaryBiproduct X Y F

Full source

/-- A functor that preserves biproducts of a pair preserves binary biproducts. -/
lemma preservesBinaryBiproduct_of_preservesBiproduct (F : C ⥤ D)
    [PreservesZeroMorphisms F] (X Y : C) [PreservesBiproduct (pairFunction X Y) F] :
    PreservesBinaryBiproduct X Y F where
  preserves {b} hb := ⟨{
      isLimit :=
        IsLimit.ofIsoLimit
            ((IsLimit.postcomposeHomEquiv (diagramIsoPair _) _).symm
              (isBilimitOfPreserves F (b.toBiconeIsBilimit.symm hb)).isLimit) <|
          Cones.ext (Iso.refl _) fun j => by
            rcases j with ⟨⟨⟩⟩ <;> simp
      isColimit :=
        IsColimit.ofIsoColimit
            ((IsColimit.precomposeInvEquiv (diagramIsoPair _) _).symm
              (isBilimitOfPreserves F (b.toBiconeIsBilimit.symm hb)).isColimit) <|
          Cocones.ext (Iso.refl _) fun j => by
            rcases j with ⟨⟨⟩⟩ <;> simp }⟩

Preservation of binary biproducts via preservation of pair biproducts

Informal description

Let $F \colon C \to D$ be a functor between categories with zero morphisms that preserves zero morphisms. If $F$ preserves the biproduct of the pair $(X, Y)$ (viewed as a family indexed by a two-element type), then $F$ preserves the binary biproduct of $X$ and $Y$.

CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBiproducts theorem

(F : C ⥤ D) [PreservesZeroMorphisms F] [PreservesBiproductsOfShape WalkingPair F] : PreservesBinaryBiproducts F

Full source

/-- A functor that preserves biproducts of a pair preserves binary biproducts. -/
lemma preservesBinaryBiproducts_of_preservesBiproducts (F : C ⥤ D) [PreservesZeroMorphisms F]
    [PreservesBiproductsOfShape WalkingPair F] : PreservesBinaryBiproducts F where
  preserves {X} Y := preservesBinaryBiproduct_of_preservesBiproduct F X Y

Preservation of Binary Biproducts via Preservation of Pair-Shaped Biproducts

Informal description

Let $F \colon C \to D$ be a functor between categories with zero morphisms that preserves zero morphisms. If $F$ preserves biproducts of shape `WalkingPair` (i.e., biproducts indexed by a two-element type), then $F$ preserves all binary biproducts.

CategoryTheory.Functor.biproductComparison definition

: F.obj (⨁ f) ⟶ ⨁ F.obj ∘ f

Full source

/-- As for products, any functor between categories with biproducts gives rise to a morphism
    `F.obj (⨁ f) ⟶ ⨁ (F.obj ∘ f)`. -/
def biproductComparison : F.obj (⨁ f) ⟶ ⨁ F.obj ∘ f :=
  biproduct.lift fun j => F.map (biproduct.π f j)

Comparison morphism between image of biproduct and biproduct of images

Informal description

Given a functor $F \colon C \to D$ between categories with zero morphisms and a family of objects $f \colon J \to C$ that has a biproduct, the morphism $\text{biproductComparison}\, F\, f \colon F(\bigoplus f) \to \bigoplus (F \circ f)$ is defined as the unique morphism induced by the universal property of the biproduct $\bigoplus (F \circ f)$, using the family of morphisms $F(\pi_j) \colon F(\bigoplus f) \to F(f(j))$ for each $j \in J$, where $\pi_j$ is the projection from $\bigoplus f$ to $f(j)$.

CategoryTheory.Functor.biproductComparison_π theorem

(j : J) : biproductComparison F f ≫ biproduct.π _ j = F.map (biproduct.π f j)

Full source

@[reassoc (attr := simp)]
theorem biproductComparison_π (j : J) :
    biproductComparisonbiproductComparison F f ≫ biproduct.π _ j = F.map (biproduct.π f j) :=
  biproduct.lift_π _ _

Commutativity of Biproduct Comparison with Projections: $\text{biproductComparison}\, F\, f \circ \pi_j = F(\pi_j)$

Informal description

Let $F \colon C \to D$ be a functor between categories with zero morphisms, and let $f \colon J \to C$ be a family of objects in $C$ that has a biproduct $\bigoplus f$. For any index $j \in J$, the composition of the biproduct comparison morphism $\text{biproductComparison}\, F\, f \colon F(\bigoplus f) \to \bigoplus (F \circ f)$ with the projection $\pi_j \colon \bigoplus (F \circ f) \to F(f(j))$ equals the image under $F$ of the projection $\pi_j \colon \bigoplus f \to f(j)$. That is, the following diagram commutes: \[ \text{biproductComparison}\, F\, f \circ \pi_j = F(\pi_j). \]

CategoryTheory.Functor.biproductComparison' definition

: ⨁ F.obj ∘ f ⟶ F.obj (⨁ f)

Full source

/-- As for coproducts, any functor between categories with biproducts gives rise to a morphism
    `⨁ (F.obj ∘ f) ⟶ F.obj (⨁ f)` -/
def biproductComparison' : ⨁ F.obj ∘ f⨁ F.obj ∘ f ⟶ F.obj (⨁ f) :=
  biproduct.desc fun j => F.map (biproduct.ι f j)

Comparison morphism from biproduct of images to image of biproduct

Informal description

Given a functor $F$ between categories with zero morphisms and a family of objects $f : J \to C$ with a biproduct $\bigoplus f$, the morphism $\bigoplus (F \circ f) \to F(\bigoplus f)$ is constructed by applying the universal property of the biproduct to the morphisms $F(\iota_j)$, where $\iota_j : f(j) \to \bigoplus f$ are the inclusion morphisms into the biproduct.

CategoryTheory.Functor.ι_biproductComparison' theorem

(j : J) : biproduct.ι _ j ≫ biproductComparison' F f = F.map (biproduct.ι f j)

Full source

@[reassoc (attr := simp)]
theorem ι_biproductComparison' (j : J) :
    biproduct.ιbiproduct.ι _ j ≫ biproductComparison' F f = F.map (biproduct.ι f j) :=
  biproduct.ι_desc _ _

Commutativity of Biproduct Inclusion with Comparison Morphism: $\iota_j \circ \text{biproductComparison}' F f = F(\iota_j)$

Informal description

Let $F$ be a functor between categories with zero morphisms, and let $f : J \to C$ be a family of objects in $C$ with a biproduct $\bigoplus f$. For each index $j \in J$, the composition of the inclusion morphism $\iota_j : F(f(j)) \to \bigoplus (F \circ f)$ with the comparison morphism $\bigoplus (F \circ f) \to F(\bigoplus f)$ equals the image under $F$ of the inclusion morphism $\iota_j : f(j) \to \bigoplus f$. That is, $\iota_j \circ \text{biproductComparison}' F f = F(\iota_j)$.

CategoryTheory.Functor.biproductComparison'_comp_biproductComparison theorem

: biproductComparison' F f ≫ biproductComparison F f = 𝟙 (⨁ F.obj ∘ f)

Full source

/-- The composition in the opposite direction is equal to the identity if and only if `F` preserves
    the biproduct, see `preservesBiproduct_of_monoBiproductComparison`. -/
@[reassoc (attr := simp)]
theorem biproductComparison'_comp_biproductComparison :
    biproductComparison'biproductComparison' F f ≫ biproductComparison F f = 𝟙 (⨁ F.obj ∘ f) := by
  classical
    ext
    simp [biproduct.ι_π, ← Functor.map_comp, eqToHom_map]

Identity of Composition of Biproduct Comparison Morphisms: $\text{biproductComparison}' \circ \text{biproductComparison} = \mathrm{id}$

Informal description

For a functor $F \colon C \to D$ between categories with zero morphisms and a family of objects $f \colon J \to C$ with a biproduct $\bigoplus f$, the composition of the comparison morphisms $\text{biproductComparison}'\, F\, f \colon \bigoplus (F \circ f) \to F(\bigoplus f)$ and $\text{biproductComparison}\, F\, f \colon F(\bigoplus f) \to \bigoplus (F \circ f)$ equals the identity morphism on $\bigoplus (F \circ f)$, i.e., \[ \text{biproductComparison}'\, F\, f \circ \text{biproductComparison}\, F\, f = \mathrm{id}_{\bigoplus (F \circ f)}. \]

CategoryTheory.Functor.splitEpiBiproductComparison definition

: SplitEpi (biproductComparison F f)

Full source

/-- `biproduct_comparison F f` is a split epimorphism. -/
@[simps]
def splitEpiBiproductComparison : SplitEpi (biproductComparison F f) where
  section_ := biproductComparison' F f
  id := by simp

Split epimorphism property of the biproduct comparison morphism

Informal description

Given a functor $ F \colon C \to D $ between categories with zero morphisms and a family of objects $ f \colon J \to C $ that has a biproduct, the comparison morphism $\text{biproductComparison}\, F\, f \colon F(\bigoplus f) \to \bigoplus (F \circ f)$ is a split epimorphism. This means there exists a section $ s \colon \bigoplus (F \circ f) \to F(\bigoplus f) $ such that the composition $ s \circ \text{biproductComparison}\, F\, f $ is the identity morphism on $ \bigoplus (F \circ f) $.

CategoryTheory.Functor.instIsSplitEpiBiproductComparison instance

: IsSplitEpi (biproductComparison F f)

Full source

instance : IsSplitEpi (biproductComparison F f) :=
  IsSplitEpi.mk' (splitEpiBiproductComparison F f)

The Biproduct Comparison Morphism is a Split Epimorphism

Informal description

For any functor $ F \colon C \to D $ between categories with zero morphisms and any family of objects $ f \colon J \to C $ that has a biproduct, the comparison morphism $\text{biproductComparison}\, F\, f \colon F(\bigoplus f) \to \bigoplus (F \circ f)$ is a split epimorphism. This means there exists a section $ s \colon \bigoplus (F \circ f) \to F(\bigoplus f) $ such that the composition $ \text{biproductComparison}\, F\, f \circ s $ is the identity morphism on $ \bigoplus (F \circ f) $.

CategoryTheory.Functor.splitMonoBiproductComparison' definition

: SplitMono (biproductComparison' F f)

Full source

/-- `biproduct_comparison' F f` is a split monomorphism. -/
@[simps]
def splitMonoBiproductComparison' : SplitMono (biproductComparison' F f) where
  retraction := biproductComparison F f
  id := by simp

Split monomorphism property of the comparison from biproduct of images to image of biproduct

Informal description

The morphism $\text{biproductComparison'}\, F\, f \colon \bigoplus (F \circ f) \to F(\bigoplus f)$ is a split monomorphism, meaning there exists a retraction $\text{biproductComparison}\, F\, f \colon F(\bigoplus f) \to \bigoplus (F \circ f)$ such that their composition is the identity morphism on $\bigoplus (F \circ f)$.

CategoryTheory.Functor.instIsSplitMonoBiproductComparison' instance

: IsSplitMono (biproductComparison' F f)

Full source

instance : IsSplitMono (biproductComparison' F f) :=
  IsSplitMono.mk' (splitMonoBiproductComparison' F f)

Split Monomorphism Property of Biproduct Comparison Morphism

Informal description

For any functor $F \colon C \to D$ between categories with zero morphisms and any family of objects $f \colon J \to C$ with a biproduct, the comparison morphism $\text{biproductComparison'}\, F\, f \colon \bigoplus (F \circ f) \to F(\bigoplus f)$ is a split monomorphism. This means there exists a retraction morphism such that the composition with $\text{biproductComparison'}\, F\, f$ yields the identity on $\bigoplus (F \circ f)$.

CategoryTheory.Functor.hasBiproduct_of_preserves instance

: HasBiproduct (F.obj ∘ f)

Full source

instance hasBiproduct_of_preserves : HasBiproduct (F.obj ∘ f) :=
  HasBiproduct.mk
    { bicone := F.mapBicone (biproduct.bicone f)
      isBilimit := isBilimitOfPreserves _ (biproduct.isBilimit _) }

Preservation of Biproducts by Functors

Informal description

Given a functor $F \colon C \to D$ that preserves zero morphisms and biproducts of a family of objects $f \colon J \to C$, the family $F \circ f \colon J \to D$ has a biproduct in $D$.

CategoryTheory.Functor.mapBiproduct abbrev

: F.obj (⨁ f) ≅ ⨁ F.obj ∘ f

Full source

/-- If `F` preserves a biproduct, we get a definitionally nice isomorphism
    `F.obj (⨁ f) ≅ ⨁ (F.obj ∘ f)`. -/
abbrev mapBiproduct : F.obj (⨁ f) ≅ ⨁ F.obj ∘ f :=
  biproduct.uniqueUpToIso _ (isBilimitOfPreserves _ (biproduct.isBilimit _))

Canonical isomorphism between image of biproduct and biproduct of images

Informal description

Given a functor $F \colon C \to D$ that preserves zero morphisms and biproducts of a family of objects $f \colon J \to C$, there exists a canonical isomorphism between the image of the biproduct $F(\bigoplus f)$ and the biproduct of the images $\bigoplus (F \circ f)$.

CategoryTheory.Functor.mapBiproduct_hom theorem

 :
  haveI : HasBiproduct fun j => F.obj (f j) := hasBiproduct_of_preserves F f
  (mapBiproduct F f).hom = biproduct.lift fun j => F.map (biproduct.π f j)

Full source

theorem mapBiproduct_hom :
    haveI : HasBiproduct fun j => F.obj (f j) := hasBiproduct_of_preserves F f
    (mapBiproduct F f).hom = biproduct.lift fun j => F.map (biproduct.π f j) := rfl

Homomorphism Part of Biproduct Preservation Isomorphism

Informal description

Let $F \colon C \to D$ be a functor between categories with zero morphisms that preserves biproducts of a family of objects $f \colon J \to C$. Then the homomorphism part of the canonical isomorphism $F(\bigoplus f) \cong \bigoplus (F \circ f)$ is given by the lift of the family of morphisms $F(\pi_j) \colon F(\bigoplus f) \to F(f(j))$ for each $j \in J$, where $\pi_j$ is the projection from the biproduct $\bigoplus f$ to its $j$-th component $f(j)$.

CategoryTheory.Functor.mapBiproduct_inv theorem

 :
  haveI : HasBiproduct fun j => F.obj (f j) := hasBiproduct_of_preserves F f
  (mapBiproduct F f).inv = biproduct.desc fun j => F.map (biproduct.ι f j)

Full source

theorem mapBiproduct_inv :
    haveI : HasBiproduct fun j => F.obj (f j) := hasBiproduct_of_preserves F f
    (mapBiproduct F f).inv = biproduct.desc fun j => F.map (biproduct.ι f j) := rfl

Inverse of Biproduct Preservation Isomorphism via Descending Morphisms

Informal description

Given a functor $F \colon C \to D$ that preserves zero morphisms and biproducts of a family of objects $f \colon J \to C$, the inverse of the canonical isomorphism $F(\bigoplus f) \cong \bigoplus (F \circ f)$ is equal to the morphism induced by the universal property of the biproduct $\bigoplus (F \circ f)$ applied to the family of morphisms $F(\iota_j) \colon F(f(j)) \to F(\bigoplus f)$, where $\iota_j \colon f(j) \to \bigoplus f$ are the inclusion morphisms.

CategoryTheory.Functor.biprodComparison definition

: F.obj (X ⊞ Y) ⟶ F.obj X ⊞ F.obj Y

Full source

/-- 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`. -/
def biprodComparison : F.obj (X ⊞ Y) ⟶ F.obj X ⊞ F.obj Y :=
  biprod.lift (F.map biprod.fst) (F.map biprod.snd)

Biproduct comparison morphism

Informal description

Given a functor $ F $ between categories with binary biproducts, the morphism $ F(X \oplus Y) \to F(X) \oplus F(Y) $ is defined as the lift of the pair of morphisms $ F(\text{biprod.fst}) $ and $ F(\text{biprod.snd}) $, where $ \oplus $ denotes the biproduct.

CategoryTheory.Functor.biprodComparison_fst theorem

: biprodComparison F X Y ≫ biprod.fst = F.map biprod.fst

Full source

@[reassoc (attr := simp)]
theorem biprodComparison_fst : biprodComparisonbiprodComparison F X Y ≫ biprod.fst = F.map biprod.fst :=
  biprod.lift_fst _ _

Commutativity of Biproduct Comparison with First Projection

Informal description

For a functor $F$ between categories with binary biproducts, the composition of the biproduct comparison morphism $F(X \oplus Y) \to F(X) \oplus F(Y)$ with the first projection morphism $\text{biprod.fst} : F(X) \oplus F(Y) \to F(X)$ is equal to the image under $F$ of the first projection morphism $\text{biprod.fst} : X \oplus Y \to X$. That is, the following diagram commutes: \[ F(X \oplus Y) \xrightarrow{\text{biprodComparison } F X Y} F(X) \oplus F(Y) \xrightarrow{\text{biprod.fst}} F(X) = F(X \oplus Y) \xrightarrow{F(\text{biprod.fst})} F(X) \]

CategoryTheory.Functor.biprodComparison_snd theorem

: biprodComparison F X Y ≫ biprod.snd = F.map biprod.snd

Full source

@[reassoc (attr := simp)]
theorem biprodComparison_snd : biprodComparisonbiprodComparison F X Y ≫ biprod.snd = F.map biprod.snd :=
  biprod.lift_snd _ _

Commutativity of Biproduct Comparison with Second Projection

Informal description

For a functor $F$ between categories with binary biproducts, the composition of the biproduct comparison morphism $F(X \oplus Y) \to F(X) \oplus F(Y)$ with the second projection morphism $\text{biprod.snd} : F(X) \oplus F(Y) \to F(Y)$ is equal to the image under $F$ of the second projection morphism $\text{biprod.snd} : X \oplus Y \to Y$. That is, the following diagram commutes: \[ F(X \oplus Y) \xrightarrow{\text{biprodComparison } F X Y} F(X) \oplus F(Y) \xrightarrow{\text{biprod.snd}} F(Y) = F(X \oplus Y) \xrightarrow{F(\text{biprod.snd})} F(Y) \]

CategoryTheory.Functor.biprodComparison' definition

: F.obj X ⊞ F.obj Y ⟶ F.obj (X ⊞ Y)

Full source

/-- 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)`. -/
def biprodComparison' : F.obj X ⊞ F.obj YF.obj X ⊞ F.obj Y ⟶ F.obj (X ⊞ Y) :=
  biprod.desc (F.map biprod.inl) (F.map biprod.inr)

Biproduct comparison morphism for a functor

Informal description

Given a functor $ F $ between categories with binary biproducts, the morphism $ F(X) \oplus F(Y) \to F(X \oplus Y) $ is defined as the unique morphism induced by the universal property of the biproduct, using the images of the inclusion maps $ F(\text{biprod.inl}) $ and $ F(\text{biprod.inr}) $.

CategoryTheory.Functor.inl_biprodComparison' theorem

: biprod.inl ≫ biprodComparison' F X Y = F.map biprod.inl

Full source

@[reassoc (attr := simp)]
theorem inl_biprodComparison' : biprod.inlbiprod.inl ≫ biprodComparison' F X Y = F.map biprod.inl :=
  biprod.inl_desc _ _

Commutativity of First Inclusion with Biproduct Comparison Morphism

Informal description

For a functor $F$ between categories with binary biproducts, the composition of the first inclusion morphism $\text{biprod.inl} : F(X) \to F(X) \oplus F(Y)$ with the biproduct comparison morphism $\text{biprodComparison' } F X Y : F(X) \oplus F(Y) \to F(X \oplus Y)$ is equal to the image under $F$ of the first inclusion morphism $\text{biprod.inl} : X \to X \oplus Y$. That is, the following diagram commutes: \[ F(X) \xrightarrow{\text{biprod.inl}} F(X) \oplus F(Y) \xrightarrow{\text{biprodComparison' } F X Y} F(X \oplus Y) = F(X) \xrightarrow{F(\text{biprod.inl})} F(X \oplus Y) \]

CategoryTheory.Functor.inr_biprodComparison' theorem

: biprod.inr ≫ biprodComparison' F X Y = F.map biprod.inr

Full source

@[reassoc (attr := simp)]
theorem inr_biprodComparison' : biprod.inrbiprod.inr ≫ biprodComparison' F X Y = F.map biprod.inr :=
  biprod.inr_desc _ _

Commutativity of Second Inclusion with Biproduct Comparison Morphism

Informal description

For a functor $F$ between categories with binary biproducts, the composition of the second inclusion morphism $\text{biprod.inr} : F(Y) \to F(X) \oplus F(Y)$ with the biproduct comparison morphism $\text{biprodComparison' } F X Y : F(X) \oplus F(Y) \to F(X \oplus Y)$ is equal to the image under $F$ of the second inclusion morphism $\text{biprod.inr} : Y \to X \oplus Y$. That is, the following diagram commutes: \[ F(Y) \xrightarrow{\text{biprod.inr}} F(X) \oplus F(Y) \xrightarrow{\text{biprodComparison' } F X Y} F(X \oplus Y) = F(Y) \xrightarrow{F(\text{biprod.inr})} F(X \oplus Y) \]

CategoryTheory.Functor.biprodComparison'_comp_biprodComparison theorem

: biprodComparison' F X Y ≫ biprodComparison F X Y = 𝟙 (F.obj X ⊞ F.obj Y)

Full source

/-- The composition in the opposite direction is equal to the identity if and only if `F` preserves
    the biproduct, see `preservesBinaryBiproduct_of_monoBiprodComparison`. -/
@[reassoc (attr := simp)]
theorem biprodComparison'_comp_biprodComparison :
    biprodComparison'biprodComparison' F X Y ≫ biprodComparison F X Y = 𝟙 (F.obj X ⊞ F.obj Y) := by
  ext <;> simp [← Functor.map_comp]

Identity Property of Biproduct Comparison Morphisms: $\text{biprodComparison'} \circ \text{biprodComparison} = \text{id}$

Informal description

For a functor $F$ between categories with binary biproducts, the composition of the biproduct comparison morphisms $F(X) \oplus F(Y) \xrightarrow{\text{biprodComparison' } F X Y} F(X \oplus Y) \xrightarrow{\text{biprodComparison } F X Y} F(X) \oplus F(Y)$ is equal to the identity morphism on $F(X) \oplus F(Y)$.

CategoryTheory.Functor.splitEpiBiprodComparison definition

: SplitEpi (biprodComparison F X Y)

Full source

/-- `biprodComparison F X Y` is a split epi. -/
@[simps]
def splitEpiBiprodComparison : SplitEpi (biprodComparison F X Y) where
  section_ := biprodComparison' F X Y
  id := by simp

Split epimorphism property of the biproduct comparison morphism

Informal description

The morphism `biprodComparison F X Y` is a split epimorphism, meaning there exists a section morphism `biprodComparison' F X Y` such that their composition is the identity morphism on the biproduct `F.obj X ⊞ F.obj Y`.

CategoryTheory.Functor.instIsSplitEpiBiprodComparison instance

: IsSplitEpi (biprodComparison F X Y)

Full source

instance : IsSplitEpi (biprodComparison F X Y) :=
  IsSplitEpi.mk' (splitEpiBiprodComparison F X Y)

Biproduct Comparison Morphism is a Split Epimorphism

Informal description

For any functor $F$ between categories with binary biproducts, the biproduct comparison morphism $F(X \oplus Y) \to F(X) \oplus F(Y)$ is a split epimorphism. This means there exists a section morphism $F(X) \oplus F(Y) \to F(X \oplus Y)$ whose composition with the biproduct comparison morphism is the identity on $F(X) \oplus F(Y)$.

CategoryTheory.Functor.splitMonoBiprodComparison' definition

: SplitMono (biprodComparison' F X Y)

Full source

/-- `biprodComparison' F X Y` is a split mono. -/
@[simps]
def splitMonoBiprodComparison' : SplitMono (biprodComparison' F X Y) where
  retraction := biprodComparison F X Y
  id := by simp

Split monomorphism property of the biproduct comparison morphism

Informal description

The morphism `biprodComparison' F X Y` is a split monomorphism, meaning there exists a retraction morphism `biprodComparison F X Y` such that their composition is the identity morphism on the biproduct `F.obj (X ⊞ Y)`.

CategoryTheory.Functor.instIsSplitMonoBiprodComparison' instance

: IsSplitMono (biprodComparison' F X Y)

Full source

instance : IsSplitMono (biprodComparison' F X Y) :=
  IsSplitMono.mk' (splitMonoBiprodComparison' F X Y)

Biproduct Comparison Morphism is a Split Monomorphism

Informal description

For any functor $ F $ between categories with binary biproducts, the biproduct comparison morphism $ F(X) \oplus F(Y) \to F(X \oplus Y) $ is a split monomorphism. This means there exists a retraction morphism $ F(X \oplus Y) \to F(X) \oplus F(Y) $ such that their composition is the identity morphism on $ F(X \oplus Y) $.

CategoryTheory.Functor.hasBinaryBiproduct_of_preserves instance

: HasBinaryBiproduct (F.obj X) (F.obj Y)

Full source

instance hasBinaryBiproduct_of_preserves : HasBinaryBiproduct (F.obj X) (F.obj Y) :=
  HasBinaryBiproduct.mk
    { bicone := F.mapBinaryBicone (BinaryBiproduct.bicone X Y)
      isBilimit := isBinaryBilimitOfPreserves F (BinaryBiproduct.isBilimit _ _) }

Existence of Binary Biproducts under Functor Preservation

Informal description

Given a functor $F : C \to D$ that preserves zero morphisms and binary biproducts of objects $X$ and $Y$ in $C$, the category $D$ has a binary biproduct of $F(X)$ and $F(Y)$. This means that the image of the biproduct structure under $F$ retains the universal property of a biproduct in $D$.

CategoryTheory.Functor.mapBiprod abbrev

: F.obj (X ⊞ Y) ≅ F.obj X ⊞ F.obj Y

Full source

/-- If `F` preserves a binary biproduct, we get a definitionally nice isomorphism
    `F.obj (X ⊞ Y) ≅ F.obj X ⊞ F.obj Y`. -/
abbrev mapBiprod : F.obj (X ⊞ Y) ≅ F.obj X ⊞ F.obj Y :=
  biprod.uniqueUpToIso _ _ (isBinaryBilimitOfPreserves F (BinaryBiproduct.isBilimit _ _))

Canonical isomorphism $F(X \oplus Y) \cong F(X) \oplus F(Y)$ for biproduct-preserving functors

Informal description

Given a functor $F \colon \mathcal{C} \to \mathcal{D}$ that preserves zero morphisms and binary biproducts of objects $X$ and $Y$ in $\mathcal{C}$, there is a canonical isomorphism $F(X \oplus Y) \cong F(X) \oplus F(Y)$ in $\mathcal{D}$.

CategoryTheory.Functor.mapBiprod_hom theorem

: (mapBiprod F X Y).hom = biprod.lift (F.map biprod.fst) (F.map biprod.snd)

Full source

theorem mapBiprod_hom : (mapBiprod F X Y).hom = biprod.lift (F.map biprod.fst) (F.map biprod.snd) :=
  rfl

Homomorphism part of $F(X \oplus Y) \cong F(X) \oplus F(Y)$ for biproduct-preserving functors

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories $\mathcal{C}$ and $\mathcal{D}$ that preserves zero morphisms and binary biproducts of objects $X$ and $Y$ in $\mathcal{C}$. Then the homomorphism part of the canonical isomorphism $F(X \oplus Y) \cong F(X) \oplus F(Y)$ is equal to the lift of the images of the biproduct projections under $F$, i.e., $$(F(X \oplus Y) \cong F(X) \oplus F(Y))_\text{hom} = \text{biprod.lift}(F(\pi_X), F(\pi_Y))$$ where $\pi_X \colon X \oplus Y \to X$ and $\pi_Y \colon X \oplus Y \to Y$ are the biproduct projections in $\mathcal{C}$.

CategoryTheory.Functor.mapBiprod_inv theorem

: (mapBiprod F X Y).inv = biprod.desc (F.map biprod.inl) (F.map biprod.inr)

Full source

theorem mapBiprod_inv : (mapBiprod F X Y).inv = biprod.desc (F.map biprod.inl) (F.map biprod.inr) :=
  rfl

Inverse of $F(X \oplus Y) \cong F(X) \oplus F(Y)$ for biproduct-preserving functors

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories $\mathcal{C}$ and $\mathcal{D}$ that preserves zero morphisms and binary biproducts of objects $X$ and $Y$ in $\mathcal{C}$. Then the inverse part of the canonical isomorphism $F(X \oplus Y) \cong F(X) \oplus F(Y)$ is equal to the coproduct of the images of the biproduct inclusions under $F$, i.e., $$(F(X \oplus Y) \cong F(X) \oplus F(Y))^{-1} = \text{biprod.desc}(F(\iota_X), F(\iota_Y))$$ where $\iota_X \colon X \to X \oplus Y$ and $\iota_Y \colon Y \to X \oplus Y$ are the biproduct inclusions in $\mathcal{C}$.

CategoryTheory.Limits.biproduct.map_lift_mapBiprod theorem

 (g : ∀ j, W ⟶ f j) :
  -- Porting note: we need haveI to tell Lean about hasBiproduct_of_preserves F fhaveI :
    HasBiproduct fun j => F.obj (f j) := hasBiproduct_of_preserves F f
  F.map (biproduct.lift g) ≫ (F.mapBiproduct f).hom = biproduct.lift fun j => F.map (g j)

Full source

theorem biproduct.map_lift_mapBiprod (g : ∀ j, W ⟶ f j) :
    -- Porting note: we need haveI to tell Lean about hasBiproduct_of_preserves F f
    haveI : HasBiproduct fun j => F.obj (f j) := hasBiproduct_of_preserves F f
    F.map (biproduct.lift g) ≫ (F.mapBiproduct f).hom = biproduct.lift fun j => F.map (g j) := by
  ext j
  dsimp only [Function.comp_def]
  simp only [mapBiproduct_hom, Category.assoc, biproduct.lift_π, ← F.map_comp]

Commutativity of Biproduct Lift with Biproduct-Preserving Functors: $F(\text{lift}\, g) \circ \phi = \text{lift}\, (F \circ g)$

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories with zero morphisms that preserves biproducts of a family of objects $f \colon J \to \mathcal{C}$. For any object $W$ in $\mathcal{C}$ and any family of morphisms $g_j \colon W \to f(j)$ for each $j \in J$, the composition of $F$ applied to the lifted morphism $\text{biproduct.lift}\, g$ with the canonical isomorphism $F(\bigoplus f) \cong \bigoplus (F \circ f)$ equals the lifted morphism of the family $F \circ g$, i.e., $$F(\text{biproduct.lift}\, g) \circ (F(\bigoplus f) \cong \bigoplus (F \circ f))_\text{hom} = \text{biproduct.lift}\, (F \circ g).$$

CategoryTheory.Limits.biproduct.mapBiproduct_inv_map_desc theorem

 (g : ∀ j, f j ⟶ W) :
  -- Porting note: we need haveI to tell Lean about hasBiproduct_of_preserves F fhaveI :
    HasBiproduct fun j => F.obj (f j) := hasBiproduct_of_preserves F f
  (F.mapBiproduct f).inv ≫ F.map (biproduct.desc g) = biproduct.desc fun j => F.map (g j)

Full source

theorem biproduct.mapBiproduct_inv_map_desc (g : ∀ j, f j ⟶ W) :
    -- Porting note: we need haveI to tell Lean about hasBiproduct_of_preserves F f
    haveI : HasBiproduct fun j => F.obj (f j) := hasBiproduct_of_preserves F f
    (F.mapBiproduct f).inv ≫ F.map (biproduct.desc g) = biproduct.desc fun j => F.map (g j) := by
  ext j
  dsimp only [Function.comp_def]
  simp only [mapBiproduct_inv, ← Category.assoc, biproduct.ι_desc ,← F.map_comp]

Compatibility of Biproduct Descending Morphisms with Functor and Canonical Isomorphism

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories with zero morphisms that preserves biproducts of a family of objects $f \colon J \to \mathcal{C}$. For any object $W$ in $\mathcal{C}$ and any collection of morphisms $g_j \colon f(j) \to W$ for each $j \in J$, the composition of the inverse of the canonical isomorphism $F(\bigoplus f) \cong \bigoplus (F \circ f)$ with $F$ applied to the universal morphism $\text{desc } g \colon \bigoplus f \to W$ equals the universal morphism $\text{desc } (F \circ g) \colon \bigoplus (F \circ f) \to F(W)$. That is, $$(F.\text{mapBiproduct} f)^{-1} \circ F(\text{desc } g) = \text{desc } (F \circ g).$$

CategoryTheory.Limits.biproduct.mapBiproduct_hom_desc theorem

(g : ∀ j, f j ⟶ W) : ((F.mapBiproduct f).hom ≫ biproduct.desc fun j => F.map (g j)) = F.map (biproduct.desc g)

Full source

theorem biproduct.mapBiproduct_hom_desc (g : ∀ j, f j ⟶ W) :
    ((F.mapBiproduct f).hom ≫ biproduct.desc fun j => F.map (g j)) = F.map (biproduct.desc g) := by
  rw [← biproduct.mapBiproduct_inv_map_desc, Iso.hom_inv_id_assoc]

Compatibility of Biproduct Descending Morphisms with Biproduct-Preserving Functor: $\phi \circ \text{desc}(F \circ g) = F(\text{desc}\, g)$

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories with zero morphisms that preserves biproducts of a family of objects $f \colon J \to \mathcal{C}$. For any object $W$ in $\mathcal{C}$ and any collection of morphisms $g_j \colon f(j) \to W$ for each $j \in J$, the composition of the canonical isomorphism $\bigoplus (F \circ f) \cong F(\bigoplus f)$ with the universal morphism $\text{desc } (F \circ g) \colon \bigoplus (F \circ f) \to F(W)$ equals $F$ applied to the universal morphism $\text{desc } g \colon \bigoplus f \to W$. That is, $$(F.\text{mapBiproduct} f) \circ \text{desc } (F \circ g) = F(\text{desc } g).$$

CategoryTheory.Limits.biprod.map_lift_mapBiprod theorem

(f : W ⟶ X) (g : W ⟶ Y) : F.map (biprod.lift f g) ≫ (F.mapBiprod X Y).hom = biprod.lift (F.map f) (F.map g)

Full source

theorem biprod.map_lift_mapBiprod (f : W ⟶ X) (g : W ⟶ Y) :
    F.map (biprod.lift f g) ≫ (F.mapBiprod X Y).hom = biprod.lift (F.map f) (F.map g) := by
  ext <;> simp [mapBiprod, ← F.map_comp]

Compatibility of Functor with Biproduct Lifts and Canonical Isomorphism

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories $\mathcal{C}$ and $\mathcal{D}$ that preserves zero morphisms and binary biproducts. For any morphisms $f \colon W \to X$ and $g \colon W \to Y$ in $\mathcal{C}$, the composition of $F$ applied to the biproduct lift of $f$ and $g$ with the canonical isomorphism $F(X \oplus Y) \cong F(X) \oplus F(Y)$ is equal to the biproduct lift of $F(f)$ and $F(g)$ in $\mathcal{D}$. In other words, the following diagram commutes: \[ F(\text{biprod.lift}(f, g)) \circ (F.\text{mapBiprod}(X, Y)).\text{hom} = \text{biprod.lift}(F(f), F(g)). \]

CategoryTheory.Limits.biprod.lift_mapBiprod theorem

(f : W ⟶ X) (g : W ⟶ Y) : biprod.lift (F.map f) (F.map g) ≫ (F.mapBiprod X Y).inv = F.map (biprod.lift f g)

Full source

theorem biprod.lift_mapBiprod (f : W ⟶ X) (g : W ⟶ Y) :
    biprod.liftbiprod.lift (F.map f) (F.map g) ≫ (F.mapBiprod X Y).inv = F.map (biprod.lift f g) := by
  rw [← biprod.map_lift_mapBiprod, Category.assoc, Iso.hom_inv_id, Category.comp_id]

Compatibility of Biproduct Lifts with Functorial Biproduct Preservation Isomorphism

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories with zero morphisms that preserves zero morphisms and binary biproducts of objects $X$ and $Y$ in $\mathcal{C}$. For any morphisms $f \colon W \to X$ and $g \colon W \to Y$ in $\mathcal{C}$, the composition of the biproduct lift of $F(f)$ and $F(g)$ with the inverse of the canonical isomorphism $F(X \oplus Y) \cong F(X) \oplus F(Y)$ equals $F$ applied to the biproduct lift of $f$ and $g$. That is, $$\operatorname{biprod.lift}(F(f), F(g)) \circ (F(X \oplus Y) \cong F(X) \oplus F(Y))^{-1} = F(\operatorname{biprod.lift}(f, g)).$$

CategoryTheory.Limits.biprod.mapBiprod_inv_map_desc theorem

(f : X ⟶ W) (g : Y ⟶ W) : (F.mapBiprod X Y).inv ≫ F.map (biprod.desc f g) = biprod.desc (F.map f) (F.map g)

Full source

theorem biprod.mapBiprod_inv_map_desc (f : X ⟶ W) (g : Y ⟶ W) :
    (F.mapBiprod X Y).inv ≫ F.map (biprod.desc f g) = biprod.desc (F.map f) (F.map g) := by
  ext <;> simp [mapBiprod, ← F.map_comp]

Inverse of Biproduct Preservation Isomorphism Commutes with Coproduct Morphism

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories with zero morphisms, and suppose $F$ preserves zero morphisms and binary biproducts of objects $X$ and $Y$ in $\mathcal{C}$. For any morphisms $f \colon X \to W$ and $g \colon Y \to W$ in $\mathcal{C}$, the composition of the inverse of the canonical isomorphism $F(X \oplus Y) \cong F(X) \oplus F(Y)$ with $F$ applied to the coproduct morphism $\operatorname{biprod.desc}(f, g)$ equals the coproduct morphism $\operatorname{biprod.desc}(F(f), F(g))$ in $\mathcal{D}$. That is, $$(F(X \oplus Y) \cong F(X) \oplus F(Y))^{-1} \circ F(\operatorname{biprod.desc}(f, g)) = \operatorname{biprod.desc}(F(f), F(g)).$$

CategoryTheory.Limits.biprod.mapBiprod_hom_desc theorem

(f : X ⟶ W) (g : Y ⟶ W) : (F.mapBiprod X Y).hom ≫ biprod.desc (F.map f) (F.map g) = F.map (biprod.desc f g)

Full source

theorem biprod.mapBiprod_hom_desc (f : X ⟶ W) (g : Y ⟶ W) :
    (F.mapBiprod X Y).hom ≫ biprod.desc (F.map f) (F.map g) = F.map (biprod.desc f g) := by
  rw [← biprod.mapBiprod_inv_map_desc, Iso.hom_inv_id_assoc]

Canonical isomorphism commutes with coproduct morphisms for biproduct-preserving functors

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories with zero morphisms that preserves zero morphisms and binary biproducts of objects $X$ and $Y$ in $\mathcal{C}$. For any morphisms $f \colon X \to W$ and $g \colon Y \to W$ in $\mathcal{C}$, the composition of the canonical isomorphism $F(X \oplus Y) \cong F(X) \oplus F(Y)$ with the coproduct morphism $\operatorname{biprod.desc}(F(f), F(g))$ equals $F$ applied to the coproduct morphism $\operatorname{biprod.desc}(f, g)$. That is, $$(F(X \oplus Y) \cong F(X) \oplus F(Y)) \circ \operatorname{biprod.desc}(F(f), F(g)) = F(\operatorname{biprod.desc}(f, g)).$$