mathlib3documentation

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

• Any biproduct satisfies the equality `total : ∑ j : J, biproduct.π f j ≫ biproduct.ι f j = 𝟙 (⨁ f)`, or, in the binary case, `total : fst ≫ inl + snd ≫ inr = 𝟙 X`.

• Any (binary) `product` or (binary) `coproduct` is a (binary) `biproduct`.

• In any category (with zero morphisms), if `biprod.map f g` is an isomorphism, then both `f` and `g` are isomorphisms.

• If `f` is a morphism `X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂` whose `X₁ ⟶ Y₁` entry is an isomorphism, then we can construct isomorphisms `L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂` and `R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂` so that `L.hom ≫ g ≫ R.hom` is diagonal (with `X₁ ⟶ Y₁` component still `f`), via Gaussian elimination.

• As a corollary of the previous two facts, if we have an isomorphism `X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂` whose `X₁ ⟶ Y₁` entry is an isomorphism, we can construct an isomorphism `X₂ ≅ Y₂`.

• If `f : W ⊞ X ⟶ Y ⊞ Z` is an isomorphism, either `𝟙 W = 0`, or at least one of the component maps `W ⟶ Y` and `W ⟶ Z` is nonzero.

• If `f : ⨁ S ⟶ ⨁ T` is an isomorphism, then every column (corresponding to a nonzero summand in the domain) has some nonzero matrix entry.

• A functor preserves a biproduct if and only if it preserves the corresponding product if and only if it preserves the corresponding coproduct.

There are connections between this material and the special case of the category whose morphisms are matrices over a ring, in particular the Schur complement (see `linear_algebra.matrix.schur_complement`). In particular, the declarations `category_theory.biprod.iso_elim`, `category_theory.biprod.gaussian` and `matrix.invertible_of_from_blocks₁₁_invertible` are all closely related.

def category_theory.limits.is_bilimit_of_total {C : Type u} {J : Type} [fintype J] {f : J C} (total : finset.univ.sum (λ (j : J), b.π j b.ι j) = 𝟙 b.X) :

In a preadditive category, we can construct a biproduct for `f : J → C` from any bicone `b` for `f` satisfying `total : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.X`.

(That is, such a bicone is a limit cone and a colimit cocone.)

Equations
theorem category_theory.limits.is_bilimit.total {C : Type u} {J : Type} [fintype J] {f : J C} (i : b.is_bilimit) :
finset.univ.sum (λ (j : J), b.π j b.ι j) = 𝟙 b.X
theorem category_theory.limits.has_biproduct_of_total {C : Type u} {J : Type} [fintype J] {f : J C} (total : finset.univ.sum (λ (j : J), b.π j b.ι j) = 𝟙 b.X) :

In a preadditive category, we can construct a biproduct for `f : J → C` from any bicone `b` for `f` satisfying `total : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.X`.

(That is, such a bicone is a limit cone and a colimit cocone.)

def category_theory.limits.is_bilimit_of_is_limit {C : Type u} {J : Type} [fintype J] {f : J C}  :

In a preadditive category, any finite bicone which is a limit cone is in fact a bilimit bicone.

Equations
noncomputable def category_theory.limits.bicone_is_bilimit_of_limit_cone_of_is_limit {C : Type u} {J : Type} [fintype J] {f : J C}  :

We can turn any limit cone over a pair into a bilimit bicone.

Equations
theorem category_theory.limits.has_biproduct.of_has_product {C : Type u} {J : Type} [finite J] (f : J C)  :

In a preadditive category, if the product over `f : J → C` exists, then the biproduct over `f` exists.

In a preadditive category, any finite bicone which is a colimit cocone is in fact a bilimit bicone.

Equations

We can turn any limit cone over a pair into a bilimit bicone.

Equations

In a preadditive category, if the coproduct over `f : J → C` exists, then the biproduct over `f` exists.

A preadditive category with finite products has finite biproducts.

A preadditive category with finite coproducts has finite biproducts.

@[simp]
theorem category_theory.limits.biproduct.total {C : Type u} {J : Type} [fintype J] {f : J C}  :
finset.univ.sum (λ (j : J), = 𝟙 ( f)

In any preadditive category, any biproduct satsifies `∑ j : J, biproduct.π f j ≫ biproduct.ι f j = 𝟙 (⨁ f)`

theorem category_theory.limits.biproduct.lift_eq {C : Type u} {J : Type} [fintype J] {f : J C} {T : C} {g : Π (j : J), T f j} :
= finset.univ.sum (λ (j : J),
theorem category_theory.limits.biproduct.desc_eq {C : Type u} {J : Type} [fintype J] {f : J C} {T : C} {g : Π (j : J), f j T} :
= finset.univ.sum (λ (j : J),
@[simp]
theorem category_theory.limits.biproduct.lift_desc {C : Type u} {J : Type} [fintype J] {f : J C} {T U : C} {g : Π (j : J), T f j} {h : Π (j : J), f j U} :
= finset.univ.sum (λ (j : J), g j h j)
@[simp]
theorem category_theory.limits.biproduct.lift_desc_assoc {C : Type u} {J : Type} [fintype J] {f : J C} {T U : C} {g : Π (j : J), T f j} {h : Π (j : J), f j U} {X' : C} (f' : U X') :
= finset.univ.sum (λ (j : J), g j h j) f'
theorem category_theory.limits.biproduct.map_eq {C : Type u} {J : Type} [fintype J] {f g : J C} {h : Π (j : J), f j g j} :
= finset.univ.sum (λ (j : J),
@[simp]
theorem category_theory.limits.biproduct.matrix_desc_assoc {C : Type u} {J : Type} [fintype J] {K : Type} [fintype K] {f : J C} {g : K C} (m : Π (j : J) (k : K), f j g k) {P : C} (x : Π (k : K), g k P) {X' : C} (f' : P X') :
= category_theory.limits.biproduct.desc (λ (j : J), finset.univ.sum (λ (k : K), m j k x k)) f'
@[simp]
theorem category_theory.limits.biproduct.matrix_desc {C : Type u} {J : Type} [fintype J] {K : Type} [fintype K] {f : J C} {g : K C} (m : Π (j : J) (k : K), f j g k) {P : C} (x : Π (k : K), g k P) :
= category_theory.limits.biproduct.desc (λ (j : J), finset.univ.sum (λ (k : K), m j k x k))
@[simp]
theorem category_theory.limits.biproduct.lift_matrix {C : Type u} {J : Type} [fintype J] {K : Type} [fintype K] {f : J C} {g : K C} {P : C} (x : Π (j : J), P f j) (m : Π (j : J) (k : K), f j g k) :
= category_theory.limits.biproduct.lift (λ (k : K), finset.univ.sum (λ (j : J), x j m j k))
@[simp]
theorem category_theory.limits.biproduct.lift_matrix_assoc {C : Type u} {J : Type} [fintype J] {K : Type} [fintype K] {f : J C} {g : K C} {P : C} (x : Π (j : J), P f j) (m : Π (j : J) (k : K), f j g k) {X' : C} (f' : ( λ (k : K), g k) X') :
= category_theory.limits.biproduct.lift (λ (k : K), finset.univ.sum (λ (j : J), x j m j k)) f'
theorem category_theory.limits.biproduct.matrix_map_assoc {C : Type u} {J : Type} [fintype J] {K : Type} [fintype K] {f : J C} {g h : K C} (m : Π (j : J) (k : K), f j g k) (n : Π (k : K), g k h k) {X' : C} (f' : ( λ (k : K), h k) X') :
= category_theory.limits.biproduct.matrix (λ (j : J) (k : K), m j k n k) f'
theorem category_theory.limits.biproduct.matrix_map {C : Type u} {J : Type} [fintype J] {K : Type} [fintype K] {f : J C} {g h : K C} (m : Π (j : J) (k : K), f j g k) (n : Π (k : K), g k h k) :
= category_theory.limits.biproduct.matrix (λ (j : J) (k : K), m j k n k)
theorem category_theory.limits.biproduct.map_matrix {C : Type u} {J : Type} [fintype J] {K : Type} [fintype K] {f g : J C} {h : K C} (m : Π (k : J), f k g k) (n : Π (j : J) (k : K), g j h k) :
= category_theory.limits.biproduct.matrix (λ (j : J) (k : K), m j n j k)
theorem category_theory.limits.biproduct.map_matrix_assoc {C : Type u} {J : Type} [fintype J] {K : Type} [fintype K] {f g : J C} {h : K C} (m : Π (k : J), f k g k) (n : Π (j : J) (k : K), g j h k) {X' : C} (f' : ( λ (k : K), h k) X') :
= category_theory.limits.biproduct.matrix (λ (j : J) (k : K), m j n j k) f'
@[simp]
theorem category_theory.limits.biproduct.reindex_inv {C : Type u} {β γ : Type} [fintype β] [decidable_eq β] [decidable_eq γ] (ε : β γ) (f : γ C)  :
@[simp]
theorem category_theory.limits.biproduct.reindex_hom {C : Type u} {β γ : Type} [fintype β] [decidable_eq β] [decidable_eq γ] (ε : β γ) (f : γ C)  :
noncomputable def category_theory.limits.biproduct.reindex {C : Type u} {β γ : Type} [fintype β] [decidable_eq β] [decidable_eq γ] (ε : β γ) (f : γ C)  :
f ε f

Reindex a categorical biproduct via an equivalence of the index types.

Equations
def category_theory.limits.is_binary_bilimit_of_total {C : Type u} {X Y : C} (total : b.fst b.inl + b.snd b.inr = 𝟙 b.X) :

In a preadditive category, we can construct a binary biproduct for `X Y : C` from any binary bicone `b` satisfying `total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.X`.

(That is, such a bicone is a limit cone and a colimit cocone.)

Equations
theorem category_theory.limits.is_bilimit.binary_total {C : Type u} {X Y : C} (i : b.is_bilimit) :
b.fst b.inl + b.snd b.inr = 𝟙 b.X
theorem category_theory.limits.has_binary_biproduct_of_total {C : Type u} {X Y : C} (total : b.fst b.inl + b.snd b.inr = 𝟙 b.X) :

In a preadditive category, we can construct a binary biproduct for `X Y : C` from any binary bicone `b` satisfying `total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.X`.

(That is, such a bicone is a limit cone and a colimit cocone.)

@[simp]
@[simp]

We can turn any limit cone over a pair into a bicone.

Equations
@[simp]
theorem category_theory.limits.inl_of_is_limit {C : Type u} {X Y : C}  :
t.inl = ht.lift
theorem category_theory.limits.inr_of_is_limit {C : Type u} {X Y : C}  :
t.inr = ht.lift

In a preadditive category, any binary bicone which is a limit cone is in fact a bilimit bicone.

Equations

We can turn any limit cone over a pair into a bilimit bicone.

Equations

In a preadditive category, if the product of `X` and `Y` exists, then the binary biproduct of `X` and `Y` exists.

In a preadditive category, if all binary products exist, then all binary biproducts exist.

@[simp]

We can turn any colimit cocone over a pair into a bicone.

Equations
@[simp]
theorem category_theory.limits.fst_of_is_colimit {C : Type u} {X Y : C}  :
t.fst = ht.desc
theorem category_theory.limits.snd_of_is_colimit {C : Type u} {X Y : C}  :
t.snd = ht.desc

In a preadditive category, any binary bicone which is a colimit cocone is in fact a bilimit bicone.

Equations

We can turn any colimit cocone over a pair into a bilimit bicone.

Equations

In a preadditive category, if the coproduct of `X` and `Y` exists, then the binary biproduct of `X` and `Y` exists.

In a preadditive category, if all binary coproducts exist, then all binary biproducts exist.

@[simp]

In any preadditive category, any binary biproduct satsifies `biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr = 𝟙 (X ⊞ Y)`.

theorem category_theory.limits.biprod.lift_eq {C : Type u} {X Y : C} {T : C} {f : T X} {g : T Y} :
theorem category_theory.limits.biprod.desc_eq {C : Type u} {X Y : C} {T : C} {f : X T} {g : Y T} :
@[simp]
theorem category_theory.limits.biprod.lift_desc {C : Type u} {X Y : C} {T U : C} {f : T X} {g : T Y} {h : X U} {i : Y U} :
= f h + g i
@[simp]
theorem category_theory.limits.biprod.lift_desc_assoc {C : Type u} {X Y : C} {T U : C} {f : T X} {g : T Y} {h : X U} {i : Y U} {X' : C} (f' : U X') :
= (f h + g i) f'
theorem category_theory.limits.biprod.map_eq {C : Type u} {W X Y Z : C} {f : W Y} {g : X Z} :
noncomputable def category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel {C : Type u} {X Y : C} {f : X Y}  :

Every split mono `f` with a cokernel induces a binary bicone with `f` as its `inl` and the cokernel map as its `snd`. We will show in `is_bilimit_binary_bicone_of_split_mono_of_cokernel` that this binary bicone is in fact already a biproduct.

Equations
• = {X := Y, fst := _inst_5, snd := , inl := f, inr := let c' : := category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel._proof_1, i' : := category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel._proof_3, i'' : := in category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel._proof_4 i'').section_, inl_fst' := _, inl_snd' := _, inr_fst' := _, inr_snd' := _}
@[simp]
@[simp]
@[simp]
@[simp]
theorem category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel_inr {C : Type u} {X Y : C} {f : X Y}  :
@[simp]

The bicone constructed in `binary_bicone_of_split_mono_of_cokernel` is a bilimit. This is a version of the splitting lemma that holds in all preadditive categories.

Equations

If `b` is a binary bicone such that `b.inl` is a kernel of `b.snd`, then `b` is a bilimit bicone.

Equations

If `b` is a binary bicone such that `b.inr` is a kernel of `b.fst`, then `b` is a bilimit bicone.

Equations

If `b` is a binary bicone such that `b.fst` is a cokernel of `b.inr`, then `b` is a bilimit bicone.

Equations

If `b` is a binary bicone such that `b.snd` is a cokernel of `b.inl`, then `b` is a bilimit bicone.

Equations
@[simp]
noncomputable def category_theory.limits.binary_bicone_of_is_split_epi_of_kernel {C : Type u} {X Y : C} {f : X Y}  :

Every split epi `f` with a kernel induces a binary bicone with `f` as its `snd` and the kernel map as its `inl`. We will show in `binary_bicone_of_is_split_mono_of_cokernel` that this binary bicone is in fact already a biproduct.

Equations
@[simp]
@[simp]
@[simp]
@[simp]
theorem category_theory.limits.binary_bicone_of_is_split_epi_of_kernel_fst {C : Type u} {X Y : C} {f : X Y}  :
noncomputable def category_theory.limits.is_bilimit_binary_bicone_of_is_split_epi_of_kernel {C : Type u} {X Y : C} {f : X Y}  :

The bicone constructed in `binary_bicone_of_is_split_epi_of_kernel` is a bilimit. This is a version of the splitting lemma that holds in all preadditive categories.

Equations
theorem category_theory.limits.biprod.add_eq_lift_id_desc {C : Type u} {X Y : C} (f g : X Y)  :
f + g =

The existence of binary biproducts implies that there is at most one preadditive structure.

theorem category_theory.limits.biprod.add_eq_lift_desc_id {C : Type u} {X Y : C} (f g : X Y)  :
f + g =

The existence of binary biproducts implies that there is at most one preadditive structure.

@[protected, instance]

The existence of binary biproducts implies that there is at most one preadditive structure.

noncomputable def category_theory.biprod.of_components {C : Type u} {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) :
X₁ X₂ Y₁ Y₂

The "matrix" morphism `X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂` with specified components.

Equations
@[simp]
theorem category_theory.biprod.inl_of_components {C : Type u} {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) :
@[simp]
theorem category_theory.biprod.inr_of_components {C : Type u} {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) :
@[simp]
theorem category_theory.biprod.of_components_fst {C : Type u} {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) :
@[simp]
theorem category_theory.biprod.of_components_snd {C : Type u} {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) :
@[simp]
@[simp]
theorem category_theory.biprod.of_components_comp {C : Type u} {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) (g₁₁ : Y₁ Z₁) (g₁₂ : Y₁ Z₂) (g₂₁ : Y₂ Z₁) (g₂₂ : Y₂ Z₂) :
f₂₁ f₂₂ g₂₁ g₂₂ = category_theory.biprod.of_components (f₁₁ g₁₁ + f₁₂ g₂₁) (f₁₁ g₁₂ + f₁₂ g₂₂) (f₂₁ g₁₁ + f₂₂ g₂₁) (f₂₁ g₁₂ + f₂₂ g₂₂)
noncomputable def category_theory.biprod.unipotent_upper {C : Type u} {X₁ X₂ : C} (r : X₁ X₂) :
X₁ X₂ X₁ X₂

The unipotent upper triangular matrix

``````(1 r)
(0 1)
``````

as an isomorphism.

Equations
@[simp]
theorem category_theory.biprod.unipotent_upper_hom {C : Type u} {X₁ X₂ : C} (r : X₁ X₂) :
= (𝟙 X₂)
@[simp]
theorem category_theory.biprod.unipotent_upper_inv {C : Type u} {X₁ X₂ : C} (r : X₁ X₂) :
= 0 (𝟙 X₂)
@[simp]
theorem category_theory.biprod.unipotent_lower_inv {C : Type u} {X₁ X₂ : C} (r : X₂ X₁) :
= (-r) (𝟙 X₂)
@[simp]
theorem category_theory.biprod.unipotent_lower_hom {C : Type u} {X₁ X₂ : C} (r : X₂ X₁) :
= (𝟙 X₂)
noncomputable def category_theory.biprod.unipotent_lower {C : Type u} {X₁ X₂ : C} (r : X₂ X₁) :
X₁ X₂ X₁ X₂

The unipotent lower triangular matrix

``````(1 0)
(r 1)
``````

as an isomorphism.

Equations
noncomputable def category_theory.biprod.gaussian' {C : Type u} {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂)  :
Σ' (L : X₁ X₂ X₁ X₂) (R : Y₁ Y₂ Y₁ Y₂) (g₂₂ : X₂ Y₂), L.hom f₂₁ f₂₂ R.hom =

If `f` is a morphism `X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂` whose `X₁ ⟶ Y₁` entry is an isomorphism, then we can construct isomorphisms `L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂` and `R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂` so that `L.hom ≫ g ≫ R.hom` is diagonal (with `X₁ ⟶ Y₁` component still `f`), via Gaussian elimination.

(This is the version of `biprod.gaussian` written in terms of components.)

Equations
noncomputable def category_theory.biprod.gaussian {C : Type u} {X₁ X₂ Y₁ Y₂ : C} (f : X₁ X₂ Y₁ Y₂)  :
Σ' (L : X₁ X₂ X₁ X₂) (R : Y₁ Y₂ Y₁ Y₂) (g₂₂ : X₂ Y₂),

If `f` is a morphism `X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂` whose `X₁ ⟶ Y₁` entry is an isomorphism, then we can construct isomorphisms `L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂` and `R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂` so that `L.hom ≫ g ≫ R.hom` is diagonal (with `X₁ ⟶ Y₁` component still `f`), via Gaussian elimination.

Equations
noncomputable def category_theory.biprod.iso_elim' {C : Type u} {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) [category_theory.is_iso f₂₁ f₂₂)] :
X₂ Y₂

If `X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂` via a two-by-two matrix whose `X₁ ⟶ Y₁` entry is an isomorphism, then we can construct an isomorphism `X₂ ≅ Y₂`, via Gaussian elimination.

Equations
• f₂₁ f₂₂ = f₁₂ f₂₁ f₂₂).cases_on (λ (L : X₁ X₂ X₁ X₂) (snd : Σ' (R : Y₁ Y₂ Y₁ Y₂) (g₂₂ : X₂ Y₂), L.hom f₂₁ f₂₂ R.hom = , snd.cases_on (λ (R : Y₁ Y₂ Y₁ Y₂) (snd_snd : Σ' (g₂₂ : X₂ Y₂), L.hom f₂₁ f₂₂ R.hom = , snd_snd.cases_on (λ (g : X₂ Y₂) (w : L.hom f₂₁ f₂₂ R.hom = , let _inst : := _, _inst_6 : := _ in
noncomputable def category_theory.biprod.iso_elim {C : Type u} {X₁ X₂ Y₁ Y₂ : C} (f : X₁ X₂ Y₁ Y₂)  :
X₂ Y₂

If `f` is an isomorphism `X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂` whose `X₁ ⟶ Y₁` entry is an isomorphism, then we can construct an isomorphism `X₂ ≅ Y₂`, via Gaussian elimination.

Equations
theorem category_theory.biprod.column_nonzero_of_iso {C : Type u} {W X Y Z : C} (f : W X Y Z)  :
theorem category_theory.biproduct.column_nonzero_of_iso' {C : Type u} {σ τ : Type} [finite τ] {S : σ C} {T : τ C} (s : σ) (f : S T)  :
( (t : τ), 𝟙 (S s) = 0
noncomputable def category_theory.biproduct.column_nonzero_of_iso {C : Type u} {σ τ : Type} [fintype τ] {S : σ C} {T : τ C} (s : σ) (nz : 𝟙 (S s) 0) (f : S T)  :
trunc (Σ' (t : τ),

If `f : ⨁ S ⟶ ⨁ T` is an isomorphism, and `s` is a non-trivial summand of the source, then there is some `t` in the target so that the `s, t` matrix entry of `f` is nonzero.

Equations
noncomputable def category_theory.limits.preserves_product_of_preserves_biproduct {C : Type u} {D : Type u'} (F : C D) {J : Type} [fintype J] {f : J C}  :

A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite products.

Equations

A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite products.

Equations
def category_theory.limits.preserves_biproduct_of_preserves_product {C : Type u} {D : Type u'} (F : C D) {J : Type} [fintype J] {f : J C}  :

A functor between preadditive categories that preserves (zero morphisms and) finite products preserves finite biproducts.

Equations
noncomputable def category_theory.limits.preserves_biproduct_of_mono_biproduct_comparison {C : Type u} {D : Type u'} (F : C D) {J : Type} [fintype J] {f : J C}  :

If the (product-like) biproduct comparison for `F` and `f` is a monomorphism, then `F` preserves the biproduct of `f`. For the converse, see `map_biproduct`.

Equations
noncomputable def category_theory.limits.preserves_biproduct_of_epi_biproduct_comparison' {C : Type u} {D : Type u'} (F : C D) {J : Type} [fintype J] {f : J C}  :

If the (coproduct-like) biproduct comparison for `F` and `f` is an epimorphism, then `F` preserves the biproduct of `F` and `f`. For the converse, see `map_biproduct`.

Equations

A functor between preadditive categories that preserves (zero morphisms and) finite products preserves finite biproducts.

Equations
noncomputable def category_theory.limits.preserves_coproduct_of_preserves_biproduct {C : Type u} {D : Type u'} (F : C D) {J : Type} [fintype J] {f : J C}  :

A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite coproducts.

Equations

A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite coproducts.

Equations
def category_theory.limits.preserves_biproduct_of_preserves_coproduct {C : Type u} {D : Type u'} (F : C D) {J : Type} [fintype J] {f : J C}  :

A functor between preadditive categories that preserves (zero morphisms and) finite coproducts preserves finite biproducts.

Equations

A functor between preadditive categories that preserves (zero morphisms and) finite coproducts preserves finite biproducts.

Equations

A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary products.

Equations

A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary products.

Equations

A functor between preadditive categories that preserves (zero morphisms and) binary products preserves binary biproducts.

Equations
noncomputable def category_theory.limits.preserves_binary_biproduct_of_mono_biprod_comparison {C : Type u} {D : Type u'} (F : C D) {X Y : C} [ (F.obj Y)] [category_theory.mono Y)] :

If the (product-like) biproduct comparison for `F`, `X` and `Y` is a monomorphism, then `F` preserves the biproduct of `X` and `Y`. For the converse, see `map_biprod`.

Equations
noncomputable def category_theory.limits.preserves_binary_biproduct_of_epi_biprod_comparison' {C : Type u} {D : Type u'} (F : C D) {X Y : C} [ (F.obj Y)] [category_theory.epi Y)] :

If the (coproduct-like) biproduct comparison for `F`, `X` and `Y` is an epimorphism, then `F` preserves the biproduct of `X` and `Y`. For the converse, see `map_biprod`.

Equations

A functor between preadditive categories that preserves (zero morphisms and) binary products preserves binary biproducts.

Equations

A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary coproducts.

Equations

A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary coproducts.

Equations

A functor between preadditive categories that preserves (zero morphisms and) binary coproducts preserves binary biproducts.

Equations

A functor between preadditive categories that preserves (zero morphisms and) binary coproducts preserves binary biproducts.

Equations