Basic facts about biproducts in preadditive categories. #
In (or between) preadditive categories,
-
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)
productor (binary)coproductis a (binary)biproduct. -
In any category (with zero morphisms), if
biprod.map f gis an isomorphism, then bothfandgare isomorphisms. -
If
fis a morphismX₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂whoseX₁ ⟶ Y₁entry is an isomorphism, then we can construct isomorphismsL : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂andR : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂so thatL.hom ≫ g ≫ R.homis diagonal (withX₁ ⟶ Y₁component stillf), via Gaussian elimination. -
As a corollary of the previous two facts, if we have an isomorphism
X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂whoseX₁ ⟶ Y₁entry is an isomorphism, we can construct an isomorphismX₂ ≅ Y₂. -
If
f : W ⊞ X ⟶ Y ⊞ Zis an isomorphism, either𝟙 W = 0, or at least one of the component mapsW ⟶ YandW ⟶ Zis nonzero. -
If
f : ⨁ S ⟶ ⨁ Tis 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
Mathlib.LinearAlgebra.Matrix.SchurComplement). In particular, the declarations
CategoryTheory.Biprod.isoElim, CategoryTheory.Biprod.gaussian
and Matrix.invertibleOfFromBlocks₁₁Invertible are all closely related.
def
CategoryTheory.Limits.isBilimitOfTotal
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
{f : J → C}
(b : CategoryTheory.Limits.Bicone f)
(total : (Finset.sum Finset.univ fun j =>
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Bicone.π b j) (CategoryTheory.Limits.Bicone.ι b j)) = CategoryTheory.CategoryStruct.id b.pt)
:
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.)
Instances For
theorem
CategoryTheory.Limits.IsBilimit.total
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
{f : J → C}
{b : CategoryTheory.Limits.Bicone f}
(i : CategoryTheory.Limits.Bicone.IsBilimit b)
:
(Finset.sum Finset.univ fun j =>
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Bicone.π b j) (CategoryTheory.Limits.Bicone.ι b j)) = CategoryTheory.CategoryStruct.id b.pt
theorem
CategoryTheory.Limits.hasBiproduct_of_total
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
{f : J → C}
(b : CategoryTheory.Limits.Bicone f)
(total : (Finset.sum Finset.univ fun j =>
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Bicone.π b j) (CategoryTheory.Limits.Bicone.ι b j)) = CategoryTheory.CategoryStruct.id b.pt)
:
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
CategoryTheory.Limits.isBilimitOfIsLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
{f : J → C}
(t : CategoryTheory.Limits.Bicone f)
(ht : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Bicone.toCone t))
:
In a preadditive category, any finite bicone which is a limit cone is in fact a bilimit bicone.
Instances For
def
CategoryTheory.Limits.biconeIsBilimitOfLimitConeOfIsLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
{f : J → C}
{t : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)}
(ht : CategoryTheory.Limits.IsLimit t)
:
We can turn any limit cone over a pair into a bilimit bicone.
Instances For
theorem
CategoryTheory.Limits.HasBiproduct.of_hasProduct
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Finite J]
(f : J → C)
[CategoryTheory.Limits.HasProduct f]
:
In a preadditive category, if the product over f : J → C exists,
then the biproduct over f exists.
def
CategoryTheory.Limits.isBilimitOfIsColimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
{f : J → C}
(t : CategoryTheory.Limits.Bicone f)
(ht : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Bicone.toCocone t))
:
In a preadditive category, any finite bicone which is a colimit cocone is in fact a bilimit bicone.
Instances For
def
CategoryTheory.Limits.biconeIsBilimitOfColimitCoconeOfIsColimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
{f : J → C}
{t : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)}
(ht : CategoryTheory.Limits.IsColimit t)
:
We can turn any limit cone over a pair into a bilimit bicone.
Instances For
theorem
CategoryTheory.Limits.HasBiproduct.of_hasCoproduct
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Finite J]
(f : J → C)
[CategoryTheory.Limits.HasCoproduct f]
:
In a preadditive category, if the coproduct over f : J → C exists,
then the biproduct over f exists.
theorem
CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteProducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteProducts C]
:
A preadditive category with finite products has finite biproducts.
theorem
CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteCoproducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
A preadditive category with finite coproducts has finite biproducts.
@[simp]
theorem
CategoryTheory.Limits.biproduct.total
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
{f : J → C}
[CategoryTheory.Limits.HasBiproduct f]
:
(Finset.sum Finset.univ fun j =>
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j)
(CategoryTheory.Limits.biproduct.ι f j)) = CategoryTheory.CategoryStruct.id (⨁ f)
In any preadditive category, any biproduct satsifies
∑ j : J, biproduct.π f j ≫ biproduct.ι f j = 𝟙 (⨁ f)
theorem
CategoryTheory.Limits.biproduct.lift_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
{f : J → C}
[CategoryTheory.Limits.HasBiproduct f]
{T : C}
{g : (j : J) → T ⟶ f j}
:
CategoryTheory.Limits.biproduct.lift g = Finset.sum Finset.univ fun j => CategoryTheory.CategoryStruct.comp (g j) (CategoryTheory.Limits.biproduct.ι f j)
theorem
CategoryTheory.Limits.biproduct.desc_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
{f : J → C}
[CategoryTheory.Limits.HasBiproduct f]
{T : C}
{g : (j : J) → f j ⟶ T}
:
CategoryTheory.Limits.biproduct.desc g = Finset.sum Finset.univ fun j => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j) (g j)
theorem
CategoryTheory.Limits.biproduct.lift_desc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
{f : J → C}
[CategoryTheory.Limits.HasBiproduct f]
{T : C}
{U : C}
{g : (j : J) → T ⟶ f j}
{h : (j : J) → f j ⟶ U}
{Z : C}
(h : U ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift g)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.desc h) h) = CategoryTheory.CategoryStruct.comp (Finset.sum Finset.univ fun j => CategoryTheory.CategoryStruct.comp (g j) (h j)) h
theorem
CategoryTheory.Limits.biproduct.lift_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
{f : J → C}
[CategoryTheory.Limits.HasBiproduct f]
{T : C}
{U : C}
{g : (j : J) → T ⟶ f j}
{h : (j : J) → f j ⟶ U}
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift g) (CategoryTheory.Limits.biproduct.desc h) = Finset.sum Finset.univ fun j => CategoryTheory.CategoryStruct.comp (g j) (h j)
theorem
CategoryTheory.Limits.biproduct.map_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
[CategoryTheory.Limits.HasFiniteBiproducts C]
{f : J → C}
{g : J → C}
{h : (j : J) → f j ⟶ g j}
:
CategoryTheory.Limits.biproduct.map h = Finset.sum Finset.univ fun j =>
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j)
(CategoryTheory.CategoryStruct.comp (h j) (CategoryTheory.Limits.biproduct.ι g j))
theorem
CategoryTheory.Limits.biproduct.matrix_desc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
{K : Type}
[Fintype K]
[CategoryTheory.Limits.HasFiniteBiproducts C]
{f : J → C}
{g : K → C}
(m : (j : J) → (k : K) → f j ⟶ g k)
{P : C}
(x : (k : K) → g k ⟶ P)
{Z : C}
(h : P ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.desc x) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.biproduct.desc fun j =>
Finset.sum Finset.univ fun k => CategoryTheory.CategoryStruct.comp (m j k) (x k))
h
theorem
CategoryTheory.Limits.biproduct.matrix_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
{K : Type}
[Fintype K]
[CategoryTheory.Limits.HasFiniteBiproducts C]
{f : J → C}
{g : K → C}
(m : (j : J) → (k : K) → f j ⟶ g k)
{P : C}
(x : (k : K) → g k ⟶ P)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m) (CategoryTheory.Limits.biproduct.desc x) = CategoryTheory.Limits.biproduct.desc fun j =>
Finset.sum Finset.univ fun k => CategoryTheory.CategoryStruct.comp (m j k) (x k)
theorem
CategoryTheory.Limits.biproduct.lift_matrix_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
{K : Type}
[Fintype K]
[CategoryTheory.Limits.HasFiniteBiproducts C]
{f : J → C}
{g : K → C}
{P : C}
(x : (j : J) → P ⟶ f j)
(m : (j : J) → (k : K) → f j ⟶ g k)
{Z : C}
(h : (⨁ fun k => g k) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift x)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.biproduct.lift fun k =>
Finset.sum Finset.univ fun j => CategoryTheory.CategoryStruct.comp (x j) (m j k))
h
theorem
CategoryTheory.Limits.biproduct.lift_matrix
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
{K : Type}
[Fintype K]
[CategoryTheory.Limits.HasFiniteBiproducts C]
{f : J → C}
{g : K → C}
{P : C}
(x : (j : J) → P ⟶ f j)
(m : (j : J) → (k : K) → f j ⟶ g k)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift x) (CategoryTheory.Limits.biproduct.matrix m) = CategoryTheory.Limits.biproduct.lift fun k =>
Finset.sum Finset.univ fun j => CategoryTheory.CategoryStruct.comp (x j) (m j k)
theorem
CategoryTheory.Limits.biproduct.matrix_map_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
{K : Type}
[Fintype K]
[CategoryTheory.Limits.HasFiniteBiproducts C]
{f : J → C}
{g : K → C}
{h : K → C}
(m : (j : J) → (k : K) → f j ⟶ g k)
(n : (k : K) → g k ⟶ h k)
{Z : C}
(h : (⨁ fun b => h b) ⟶ Z)
:
theorem
CategoryTheory.Limits.biproduct.matrix_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
{K : Type}
[Fintype K]
[CategoryTheory.Limits.HasFiniteBiproducts C]
{f : J → C}
{g : K → C}
{h : K → C}
(m : (j : J) → (k : K) → f j ⟶ g k)
(n : (k : K) → g k ⟶ h k)
:
theorem
CategoryTheory.Limits.biproduct.map_matrix_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
{K : Type}
[Fintype K]
[CategoryTheory.Limits.HasFiniteBiproducts C]
{f : J → C}
{g : J → C}
{h : K → C}
(m : (k : J) → f k ⟶ g k)
(n : (j : J) → (k : K) → g j ⟶ h k)
{Z : C}
(h : (⨁ fun k => h k) ⟶ Z)
:
theorem
CategoryTheory.Limits.biproduct.map_matrix
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
{K : Type}
[Fintype K]
[CategoryTheory.Limits.HasFiniteBiproducts C]
{f : J → C}
{g : J → C}
{h : K → C}
(m : (k : J) → f k ⟶ g k)
(n : (j : J) → (k : K) → g j ⟶ h k)
:
@[simp]
theorem
CategoryTheory.Limits.biproduct.reindex_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{β : Type}
{γ : Type}
[Fintype β]
[DecidableEq β]
[DecidableEq γ]
(ε : β ≃ γ)
(f : γ → C)
[CategoryTheory.Limits.HasBiproduct f]
[CategoryTheory.Limits.HasBiproduct (f ∘ ↑ε)]
:
(CategoryTheory.Limits.biproduct.reindex ε f).hom = CategoryTheory.Limits.biproduct.desc fun b => CategoryTheory.Limits.biproduct.ι f (↑ε b)
@[simp]
theorem
CategoryTheory.Limits.biproduct.reindex_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{β : Type}
{γ : Type}
[Fintype β]
[DecidableEq β]
[DecidableEq γ]
(ε : β ≃ γ)
(f : γ → C)
[CategoryTheory.Limits.HasBiproduct f]
[CategoryTheory.Limits.HasBiproduct (f ∘ ↑ε)]
:
(CategoryTheory.Limits.biproduct.reindex ε f).inv = CategoryTheory.Limits.biproduct.lift fun b => CategoryTheory.Limits.biproduct.π f (↑ε b)
def
CategoryTheory.Limits.biproduct.reindex
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{β : Type}
{γ : Type}
[Fintype β]
[DecidableEq β]
[DecidableEq γ]
(ε : β ≃ γ)
(f : γ → C)
[CategoryTheory.Limits.HasBiproduct f]
[CategoryTheory.Limits.HasBiproduct (f ∘ ↑ε)]
:
Reindex a categorical biproduct via an equivalence of the index types.
Instances For
def
CategoryTheory.Limits.isBinaryBilimitOfTotal
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
(b : CategoryTheory.Limits.BinaryBicone X Y)
(total : CategoryTheory.CategoryStruct.comp b.fst b.inl + CategoryTheory.CategoryStruct.comp b.snd b.inr = CategoryTheory.CategoryStruct.id b.pt)
:
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.)
Instances For
theorem
CategoryTheory.Limits.IsBilimit.binary_total
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{b : CategoryTheory.Limits.BinaryBicone X Y}
(i : CategoryTheory.Limits.BinaryBicone.IsBilimit b)
:
CategoryTheory.CategoryStruct.comp b.fst b.inl + CategoryTheory.CategoryStruct.comp b.snd b.inr = CategoryTheory.CategoryStruct.id b.pt
theorem
CategoryTheory.Limits.hasBinaryBiproduct_of_total
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
(b : CategoryTheory.Limits.BinaryBicone X Y)
(total : CategoryTheory.CategoryStruct.comp b.fst b.inl + CategoryTheory.CategoryStruct.comp b.snd b.inr = CategoryTheory.CategoryStruct.id b.pt)
:
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]
theorem
CategoryTheory.Limits.BinaryBicone.ofLimitCone_inr
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)}
(ht : CategoryTheory.Limits.IsLimit t)
:
@[simp]
theorem
CategoryTheory.Limits.BinaryBicone.ofLimitCone_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)}
(ht : CategoryTheory.Limits.IsLimit t)
:
(CategoryTheory.Limits.BinaryBicone.ofLimitCone ht).fst = t.π.app { as := CategoryTheory.Limits.WalkingPair.left }
@[simp]
theorem
CategoryTheory.Limits.BinaryBicone.ofLimitCone_inl
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)}
(ht : CategoryTheory.Limits.IsLimit t)
:
@[simp]
theorem
CategoryTheory.Limits.BinaryBicone.ofLimitCone_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)}
(ht : CategoryTheory.Limits.IsLimit t)
:
(CategoryTheory.Limits.BinaryBicone.ofLimitCone ht).snd = t.π.app { as := CategoryTheory.Limits.WalkingPair.right }
@[simp]
theorem
CategoryTheory.Limits.BinaryBicone.ofLimitCone_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)}
(ht : CategoryTheory.Limits.IsLimit t)
:
(CategoryTheory.Limits.BinaryBicone.ofLimitCone ht).pt = t.pt
def
CategoryTheory.Limits.BinaryBicone.ofLimitCone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)}
(ht : CategoryTheory.Limits.IsLimit t)
:
We can turn any limit cone over a pair into a bicone.
Instances For
theorem
CategoryTheory.Limits.inl_of_isLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{t : CategoryTheory.Limits.BinaryBicone X Y}
(ht : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryBicone.toCone t))
:
theorem
CategoryTheory.Limits.inr_of_isLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{t : CategoryTheory.Limits.BinaryBicone X Y}
(ht : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryBicone.toCone t))
:
def
CategoryTheory.Limits.isBinaryBilimitOfIsLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
(t : CategoryTheory.Limits.BinaryBicone X Y)
(ht : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryBicone.toCone t))
:
In a preadditive category, any binary bicone which is a limit cone is in fact a bilimit bicone.
Instances For
def
CategoryTheory.Limits.binaryBiconeIsBilimitOfLimitConeOfIsLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)}
(ht : CategoryTheory.Limits.IsLimit t)
:
We can turn any limit cone over a pair into a bilimit bicone.
Instances For
theorem
CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryProduct
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(X : C)
(Y : C)
[CategoryTheory.Limits.HasBinaryProduct X Y]
:
In a preadditive category, if the product of X and Y exists, then the
binary biproduct of X and Y exists.
theorem
CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryProducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryProducts C]
:
In a preadditive category, if all binary products exist, then all binary biproducts exist.
@[simp]
theorem
CategoryTheory.Limits.BinaryBicone.ofColimitCocone_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)}
(ht : CategoryTheory.Limits.IsColimit t)
:
@[simp]
theorem
CategoryTheory.Limits.BinaryBicone.ofColimitCocone_inr
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)}
(ht : CategoryTheory.Limits.IsColimit t)
:
(CategoryTheory.Limits.BinaryBicone.ofColimitCocone ht).inr = t.ι.app { as := CategoryTheory.Limits.WalkingPair.right }
@[simp]
theorem
CategoryTheory.Limits.BinaryBicone.ofColimitCocone_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)}
(ht : CategoryTheory.Limits.IsColimit t)
:
(CategoryTheory.Limits.BinaryBicone.ofColimitCocone ht).pt = t.pt
@[simp]
theorem
CategoryTheory.Limits.BinaryBicone.ofColimitCocone_inl
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)}
(ht : CategoryTheory.Limits.IsColimit t)
:
(CategoryTheory.Limits.BinaryBicone.ofColimitCocone ht).inl = t.ι.app { as := CategoryTheory.Limits.WalkingPair.left }
@[simp]
theorem
CategoryTheory.Limits.BinaryBicone.ofColimitCocone_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)}
(ht : CategoryTheory.Limits.IsColimit t)
:
def
CategoryTheory.Limits.BinaryBicone.ofColimitCocone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)}
(ht : CategoryTheory.Limits.IsColimit t)
:
We can turn any colimit cocone over a pair into a bicone.
Instances For
theorem
CategoryTheory.Limits.fst_of_isColimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{t : CategoryTheory.Limits.BinaryBicone X Y}
(ht : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryBicone.toCocone t))
:
theorem
CategoryTheory.Limits.snd_of_isColimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{t : CategoryTheory.Limits.BinaryBicone X Y}
(ht : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryBicone.toCocone t))
:
def
CategoryTheory.Limits.isBinaryBilimitOfIsColimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
(t : CategoryTheory.Limits.BinaryBicone X Y)
(ht : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryBicone.toCocone t))
:
In a preadditive category, any binary bicone which is a colimit cocone is in fact a bilimit bicone.
Instances For
def
CategoryTheory.Limits.binaryBiconeIsBilimitOfColimitCoconeOfIsColimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)}
(ht : CategoryTheory.Limits.IsColimit t)
:
We can turn any colimit cocone over a pair into a bilimit bicone.
Instances For
theorem
CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryCoproduct
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(X : C)
(Y : C)
[CategoryTheory.Limits.HasBinaryCoproduct X Y]
:
In a preadditive category, if the coproduct of X and Y exists, then the
binary biproduct of X and Y exists.
theorem
CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryCoproducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryCoproducts C]
:
In a preadditive category, if all binary coproducts exist, then all binary biproducts exist.
@[simp]
theorem
CategoryTheory.Limits.biprod.total
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasBinaryBiproduct X Y]
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.inl + CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.inr = CategoryTheory.CategoryStruct.id (X ⊞ Y)
In any preadditive category, any binary biproduct satsifies
biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr = 𝟙 (X ⊞ Y).
theorem
CategoryTheory.Limits.biprod.lift_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasBinaryBiproduct X Y]
{T : C}
{f : T ⟶ X}
{g : T ⟶ Y}
:
CategoryTheory.Limits.biprod.lift f g = CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.inl + CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.inr
theorem
CategoryTheory.Limits.biprod.desc_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasBinaryBiproduct X Y]
{T : C}
{f : X ⟶ T}
{g : Y ⟶ T}
:
CategoryTheory.Limits.biprod.desc f g = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst f + CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd g
@[simp]
theorem
CategoryTheory.Limits.biprod.lift_desc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasBinaryBiproduct X Y]
{T : C}
{U : C}
{f : T ⟶ X}
{g : T ⟶ Y}
{h : X ⟶ U}
{i : Y ⟶ U}
{Z : C}
(h : U ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.biprod.lift_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasBinaryBiproduct X Y]
{T : C}
{U : C}
{f : T ⟶ X}
{g : T ⟶ Y}
{h : X ⟶ U}
{i : Y ⟶ U}
:
theorem
CategoryTheory.Limits.biprod.map_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : W ⟶ Y}
{g : X ⟶ Z}
:
CategoryTheory.Limits.biprod.map f g = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst
(CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.inl) + CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd
(CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.inr)
@[simp]
theorem
CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_inl
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.IsSplitMono f]
{c : CategoryTheory.Limits.CokernelCofork f}
(i : CategoryTheory.Limits.IsColimit c)
:
@[simp]
theorem
CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_inr
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.IsSplitMono f]
{c : CategoryTheory.Limits.CokernelCofork f}
(i : CategoryTheory.Limits.IsColimit c)
:
(CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel i).inr = let c' :=
CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.Cofork.π c)
(_ :
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.id Y - (CategoryTheory.CategoryStruct.id Y - CategoryTheory.CategoryStruct.comp (CategoryTheory.retraction f) f))
(CategoryTheory.Limits.Cofork.π c) = 0);
let i' :=
CategoryTheory.Limits.isCokernelEpiComp i (CategoryTheory.retraction f)
(_ :
CategoryTheory.CategoryStruct.id Y - (CategoryTheory.CategoryStruct.id Y - CategoryTheory.CategoryStruct.comp (CategoryTheory.retraction f) f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.retraction f) f);
let i'' := CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork i';
(CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork C
(_ :
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.id Y - CategoryTheory.CategoryStruct.comp (CategoryTheory.retraction f) f)
(CategoryTheory.CategoryStruct.id Y - CategoryTheory.CategoryStruct.comp (CategoryTheory.retraction f) f) = CategoryTheory.CategoryStruct.id Y - CategoryTheory.CategoryStruct.comp (CategoryTheory.retraction f) f)
i'').section_
@[simp]
theorem
CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.IsSplitMono f]
{c : CategoryTheory.Limits.CokernelCofork f}
(i : CategoryTheory.Limits.IsColimit c)
:
@[simp]
theorem
CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.IsSplitMono f]
{c : CategoryTheory.Limits.CokernelCofork f}
(i : CategoryTheory.Limits.IsColimit c)
:
@[simp]
theorem
CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.IsSplitMono f]
{c : CategoryTheory.Limits.CokernelCofork f}
(i : CategoryTheory.Limits.IsColimit c)
:
def
CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.IsSplitMono f]
{c : CategoryTheory.Limits.CokernelCofork f}
(i : CategoryTheory.Limits.IsColimit c)
:
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.
Instances For
def
CategoryTheory.Limits.isBilimitBinaryBiconeOfIsSplitMonoOfCokernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.IsSplitMono f]
{c : CategoryTheory.Limits.CokernelCofork f}
(i : CategoryTheory.Limits.IsColimit c)
:
The bicone constructed in binaryBiconeOfSplitMonoOfCokernel is a bilimit.
This is a version of the splitting lemma that holds in all preadditive categories.
Instances For
def
CategoryTheory.Limits.BinaryBicone.isBilimitOfKernelInl
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
(b : CategoryTheory.Limits.BinaryBicone X Y)
(hb : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryBicone.sndKernelFork b))
:
If b is a binary bicone such that b.inl is a kernel of b.snd, then b is a bilimit
bicone.
Instances For
def
CategoryTheory.Limits.BinaryBicone.isBilimitOfKernelInr
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
(b : CategoryTheory.Limits.BinaryBicone X Y)
(hb : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryBicone.fstKernelFork b))
:
If b is a binary bicone such that b.inr is a kernel of b.fst, then b is a bilimit
bicone.
Instances For
def
CategoryTheory.Limits.BinaryBicone.isBilimitOfCokernelFst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
(b : CategoryTheory.Limits.BinaryBicone X Y)
(hb : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryBicone.inrCokernelCofork b))
:
If b is a binary bicone such that b.fst is a cokernel of b.inr, then b is a bilimit
bicone.
Instances For
def
CategoryTheory.Limits.BinaryBicone.isBilimitOfCokernelSnd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
(b : CategoryTheory.Limits.BinaryBicone X Y)
(hb : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryBicone.inlCokernelCofork b))
:
If b is a binary bicone such that b.snd is a cokernel of b.inl, then b is a bilimit
bicone.
Instances For
@[simp]
theorem
CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.IsSplitEpi f]
{c : CategoryTheory.Limits.KernelFork f}
(i : CategoryTheory.Limits.IsLimit c)
:
@[simp]
theorem
CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.IsSplitEpi f]
{c : CategoryTheory.Limits.KernelFork f}
(i : CategoryTheory.Limits.IsLimit c)
:
(CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel i).fst = let c' :=
CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.Fork.ι c)
(_ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c)
(CategoryTheory.CategoryStruct.id X - (CategoryTheory.CategoryStruct.id X - CategoryTheory.CategoryStruct.comp f (CategoryTheory.section_ f))) = 0);
let i' :=
CategoryTheory.Limits.isKernelCompMono i (CategoryTheory.section_ f)
(_ :
CategoryTheory.CategoryStruct.id X - (CategoryTheory.CategoryStruct.id X - CategoryTheory.CategoryStruct.comp f (CategoryTheory.section_ f)) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.section_ f));
let i'' := CategoryTheory.Preadditive.isLimitForkOfKernelFork i';
(CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork C
(_ :
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.id X - CategoryTheory.CategoryStruct.comp f (CategoryTheory.section_ f))
(CategoryTheory.CategoryStruct.id X - CategoryTheory.CategoryStruct.comp f (CategoryTheory.section_ f)) = CategoryTheory.CategoryStruct.id X - CategoryTheory.CategoryStruct.comp f (CategoryTheory.section_ f))
i'').retraction
@[simp]
theorem
CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_inl
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.IsSplitEpi f]
{c : CategoryTheory.Limits.KernelFork f}
(i : CategoryTheory.Limits.IsLimit c)
:
@[simp]
theorem
CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.IsSplitEpi f]
{c : CategoryTheory.Limits.KernelFork f}
(i : CategoryTheory.Limits.IsLimit c)
:
@[simp]
theorem
CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_inr
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.IsSplitEpi f]
{c : CategoryTheory.Limits.KernelFork f}
(i : CategoryTheory.Limits.IsLimit c)
:
def
CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.IsSplitEpi f]
{c : CategoryTheory.Limits.KernelFork f}
(i : CategoryTheory.Limits.IsLimit c)
:
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.
Instances For
def
CategoryTheory.Limits.isBilimitBinaryBiconeOfIsSplitEpiOfKernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.IsSplitEpi f]
{c : CategoryTheory.Limits.KernelFork f}
(i : CategoryTheory.Limits.IsLimit c)
:
The bicone constructed in binaryBiconeOfIsSplitEpiOfKernel is a bilimit.
This is a version of the splitting lemma that holds in all preadditive categories.
Instances For
theorem
CategoryTheory.Limits.biprod.add_eq_lift_id_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasBinaryBiproduct X X]
:
The existence of binary biproducts implies that there is at most one preadditive structure.
theorem
CategoryTheory.Limits.biprod.add_eq_lift_desc_id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasBinaryBiproduct Y Y]
:
The existence of binary biproducts implies that there is at most one preadditive structure.
theorem
CategoryTheory.Preadditive.ext
{C : Type u}
:
∀ {inst : CategoryTheory.Category.{v, u} C} (x y : CategoryTheory.Preadditive C),
CategoryTheory.Preadditive.homGroup = CategoryTheory.Preadditive.homGroup → x = y
theorem
CategoryTheory.Preadditive.ext_iff
{C : Type u}
:
∀ {inst : CategoryTheory.Category.{v, u} C} (x y : CategoryTheory.Preadditive C),
x = y ↔ CategoryTheory.Preadditive.homGroup = CategoryTheory.Preadditive.homGroup
instance
CategoryTheory.subsingleton_preadditive_of_hasBinaryBiproducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
:
The existence of binary biproducts implies that there is at most one preadditive structure.
def
CategoryTheory.Biprod.ofComponents
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ : C}
{X₂ : C}
{Y₁ : C}
{Y₂ : C}
(f₁₁ : X₁ ⟶ Y₁)
(f₁₂ : X₁ ⟶ Y₂)
(f₂₁ : X₂ ⟶ Y₁)
(f₂₂ : X₂ ⟶ Y₂)
:
The "matrix" morphism X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂ with specified components.
Instances For
@[simp]
theorem
CategoryTheory.Biprod.inl_ofComponents
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ : C}
{X₂ : C}
{Y₁ : C}
{Y₂ : C}
(f₁₁ : X₁ ⟶ Y₁)
(f₁₂ : X₁ ⟶ Y₂)
(f₂₁ : X₂ ⟶ Y₁)
(f₂₂ : X₂ ⟶ Y₂)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
(CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂) = CategoryTheory.CategoryStruct.comp f₁₁ CategoryTheory.Limits.biprod.inl + CategoryTheory.CategoryStruct.comp f₁₂ CategoryTheory.Limits.biprod.inr
@[simp]
theorem
CategoryTheory.Biprod.inr_ofComponents
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ : C}
{X₂ : C}
{Y₁ : C}
{Y₂ : C}
(f₁₁ : X₁ ⟶ Y₁)
(f₁₂ : X₁ ⟶ Y₂)
(f₂₁ : X₂ ⟶ Y₁)
(f₂₂ : X₂ ⟶ Y₂)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
(CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂) = CategoryTheory.CategoryStruct.comp f₂₁ CategoryTheory.Limits.biprod.inl + CategoryTheory.CategoryStruct.comp f₂₂ CategoryTheory.Limits.biprod.inr
@[simp]
theorem
CategoryTheory.Biprod.ofComponents_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ : C}
{X₂ : C}
{Y₁ : C}
{Y₂ : C}
(f₁₁ : X₁ ⟶ Y₁)
(f₁₂ : X₁ ⟶ Y₂)
(f₂₁ : X₂ ⟶ Y₁)
(f₂₂ : X₂ ⟶ Y₂)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂)
CategoryTheory.Limits.biprod.fst = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst f₁₁ + CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd f₂₁
@[simp]
theorem
CategoryTheory.Biprod.ofComponents_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ : C}
{X₂ : C}
{Y₁ : C}
{Y₂ : C}
(f₁₁ : X₁ ⟶ Y₁)
(f₁₂ : X₁ ⟶ Y₂)
(f₂₁ : X₂ ⟶ Y₁)
(f₂₂ : X₂ ⟶ Y₂)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂)
CategoryTheory.Limits.biprod.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst f₁₂ + CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd f₂₂
@[simp]
theorem
CategoryTheory.Biprod.ofComponents_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ : C}
{X₂ : C}
{Y₁ : C}
{Y₂ : C}
(f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂)
:
CategoryTheory.Biprod.ofComponents
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
(CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst))
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
(CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd))
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
(CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst))
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
(CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd)) = f
@[simp]
theorem
CategoryTheory.Biprod.ofComponents_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ : C}
{X₂ : C}
{Y₁ : C}
{Y₂ : C}
{Z₁ : C}
{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₂)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂)
(CategoryTheory.Biprod.ofComponents g₁₁ g₁₂ g₂₁ g₂₂) = CategoryTheory.Biprod.ofComponents
(CategoryTheory.CategoryStruct.comp f₁₁ g₁₁ + CategoryTheory.CategoryStruct.comp f₁₂ g₂₁)
(CategoryTheory.CategoryStruct.comp f₁₁ g₁₂ + CategoryTheory.CategoryStruct.comp f₁₂ g₂₂)
(CategoryTheory.CategoryStruct.comp f₂₁ g₁₁ + CategoryTheory.CategoryStruct.comp f₂₂ g₂₁)
(CategoryTheory.CategoryStruct.comp f₂₁ g₁₂ + CategoryTheory.CategoryStruct.comp f₂₂ g₂₂)
@[simp]
theorem
CategoryTheory.Biprod.unipotentUpper_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ : C}
{X₂ : C}
(r : X₁ ⟶ X₂)
:
@[simp]
theorem
CategoryTheory.Biprod.unipotentUpper_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ : C}
{X₂ : C}
(r : X₁ ⟶ X₂)
:
def
CategoryTheory.Biprod.unipotentUpper
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ : C}
{X₂ : C}
(r : X₁ ⟶ X₂)
:
The unipotent upper triangular matrix
(1 r)
(0 1)
as an isomorphism.
Instances For
@[simp]
theorem
CategoryTheory.Biprod.unipotentLower_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ : C}
{X₂ : C}
(r : X₂ ⟶ X₁)
:
@[simp]
theorem
CategoryTheory.Biprod.unipotentLower_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ : C}
{X₂ : C}
(r : X₂ ⟶ X₁)
:
def
CategoryTheory.Biprod.unipotentLower
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ : C}
{X₂ : C}
(r : X₂ ⟶ X₁)
:
The unipotent lower triangular matrix
(1 0)
(r 1)
as an isomorphism.
Instances For
def
CategoryTheory.Biprod.gaussian'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ : C}
{X₂ : C}
{Y₁ : C}
{Y₂ : C}
(f₁₁ : X₁ ⟶ Y₁)
(f₁₂ : X₁ ⟶ Y₂)
(f₂₁ : X₂ ⟶ Y₁)
(f₂₂ : X₂ ⟶ Y₂)
[CategoryTheory.IsIso f₁₁]
:
(L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) ×'
(R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) ×'
(g₂₂ : X₂ ⟶ Y₂) ×'
CategoryTheory.CategoryStruct.comp L.hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂) R.hom) = CategoryTheory.Limits.biprod.map f₁₁ g₂₂
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.)
Instances For
def
CategoryTheory.Biprod.gaussian
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ : C}
{X₂ : C}
{Y₁ : C}
{Y₂ : C}
(f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂)
[CategoryTheory.IsIso
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
(CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst))]
:
(L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) ×'
(R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) ×'
(g₂₂ : X₂ ⟶ Y₂) ×'
CategoryTheory.CategoryStruct.comp L.hom (CategoryTheory.CategoryStruct.comp f R.hom) = CategoryTheory.Limits.biprod.map
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
(CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst))
g₂₂
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.
Instances For
def
CategoryTheory.Biprod.isoElim'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ : C}
{X₂ : C}
{Y₁ : C}
{Y₂ : C}
(f₁₁ : X₁ ⟶ Y₁)
(f₁₂ : X₁ ⟶ Y₂)
(f₂₁ : X₂ ⟶ Y₁)
(f₂₂ : X₂ ⟶ Y₂)
[CategoryTheory.IsIso f₁₁]
[CategoryTheory.IsIso (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ 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.
Instances For
def
CategoryTheory.Biprod.isoElim
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ : C}
{X₂ : C}
{Y₁ : C}
{Y₂ : C}
(f : X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂)
[CategoryTheory.IsIso
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
(CategoryTheory.CategoryStruct.comp f.hom CategoryTheory.Limits.biprod.fst))]
:
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.
Instances For
theorem
CategoryTheory.Biprod.column_nonzero_of_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : W ⊞ X ⟶ Y ⊞ Z)
[CategoryTheory.IsIso f]
:
CategoryTheory.CategoryStruct.id W = 0 ∨ CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
(CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst) ≠ 0 ∨ CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
(CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd) ≠ 0
theorem
CategoryTheory.Biproduct.column_nonzero_of_iso'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{σ : Type}
{τ : Type}
[Finite τ]
{S : σ → C}
[CategoryTheory.Limits.HasBiproduct S]
{T : τ → C}
[CategoryTheory.Limits.HasBiproduct T]
(s : σ)
(f : ⨁ S ⟶ ⨁ T)
[CategoryTheory.IsIso f]
:
(∀ (t : τ),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι S s)
(CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biproduct.π T t)) = 0) →
CategoryTheory.CategoryStruct.id (S s) = 0
def
CategoryTheory.Biproduct.columnNonzeroOfIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{σ : Type}
{τ : Type}
[Fintype τ]
{S : σ → C}
[CategoryTheory.Limits.HasBiproduct S]
{T : τ → C}
[CategoryTheory.Limits.HasBiproduct T]
(s : σ)
(nz : CategoryTheory.CategoryStruct.id (S s) ≠ 0)
(f : ⨁ S ⟶ ⨁ T)
[CategoryTheory.IsIso f]
:
Trunc
((t : τ) ×'
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι S s)
(CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biproduct.π T t)) ≠ 0)
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.
Instances For
def
CategoryTheory.Limits.preservesProductOfPreservesBiproduct
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{J : Type}
[Fintype J]
{f : J → C}
[CategoryTheory.Limits.PreservesBiproduct f F]
:
A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite products.
Instances For
def
CategoryTheory.Limits.preservesProductsOfShapeOfPreservesBiproductsOfShape
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{J : Type}
[Fintype J]
[CategoryTheory.Limits.PreservesBiproductsOfShape J F]
:
A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite products.
Instances For
def
CategoryTheory.Limits.preservesBiproductOfPreservesProduct
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{J : Type}
[Fintype J]
{f : J → C}
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) F]
:
A functor between preadditive categories that preserves (zero morphisms and) finite products preserves finite biproducts.
Instances For
def
CategoryTheory.Limits.preservesBiproductOfMonoBiproductComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{J : Type}
[Fintype J]
{f : J → C}
[CategoryTheory.Limits.HasBiproduct f]
[CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)]
[CategoryTheory.Mono (CategoryTheory.Functor.biproductComparison F f)]
:
If the (product-like) biproduct comparison for F and f is a monomorphism, then F
preserves the biproduct of f. For the converse, see mapBiproduct.
Instances For
def
CategoryTheory.Limits.preservesBiproductOfEpiBiproductComparison'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{J : Type}
[Fintype J]
{f : J → C}
[CategoryTheory.Limits.HasBiproduct f]
[CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)]
[CategoryTheory.Epi (CategoryTheory.Functor.biproductComparison' F f)]
:
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 mapBiproduct.
Instances For
def
CategoryTheory.Limits.preservesBiproductsOfShapeOfPreservesProductsOfShape
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{J : Type}
[Fintype J]
[CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) F]
:
A functor between preadditive categories that preserves (zero morphisms and) finite products preserves finite biproducts.
Instances For
def
CategoryTheory.Limits.preservesCoproductOfPreservesBiproduct
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{J : Type}
[Fintype J]
{f : J → C}
[CategoryTheory.Limits.PreservesBiproduct f F]
:
A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite coproducts.
Instances For
def
CategoryTheory.Limits.preservesCoproductsOfShapeOfPreservesBiproductsOfShape
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{J : Type}
[Fintype J]
[CategoryTheory.Limits.PreservesBiproductsOfShape J F]
:
A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite coproducts.
Instances For
def
CategoryTheory.Limits.preservesBiproductOfPreservesCoproduct
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{J : Type}
[Fintype J]
{f : J → C}
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) F]
:
A functor between preadditive categories that preserves (zero morphisms and) finite coproducts preserves finite biproducts.
Instances For
def
CategoryTheory.Limits.preservesBiproductsOfShapeOfPreservesCoproductsOfShape
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{J : Type}
[Fintype J]
[CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) F]
:
A functor between preadditive categories that preserves (zero morphisms and) finite coproducts preserves finite biproducts.
Instances For
def
CategoryTheory.Limits.preservesBinaryProductOfPreservesBinaryBiproduct
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{X : C}
{Y : C}
[CategoryTheory.Limits.PreservesBinaryBiproduct X Y F]
:
A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary products.
Instances For
def
CategoryTheory.Limits.preservesBinaryProductsOfPreservesBinaryBiproducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Limits.PreservesBinaryBiproducts F]
:
A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary products.
Instances For
def
CategoryTheory.Limits.preservesBinaryBiproductOfPreservesBinaryProduct
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{X : C}
{Y : C}
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) F]
:
A functor between preadditive categories that preserves (zero morphisms and) binary products preserves binary biproducts.
Instances For
def
CategoryTheory.Limits.preservesBinaryBiproductOfMonoBiprodComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasBinaryBiproduct X Y]
[CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)]
[CategoryTheory.Mono (CategoryTheory.Functor.biprodComparison F X 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.
Instances For
def
CategoryTheory.Limits.preservesBinaryBiproductOfEpiBiprodComparison'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasBinaryBiproduct X Y]
[CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)]
[CategoryTheory.Epi (CategoryTheory.Functor.biprodComparison' F X 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 mapBiprod.
Instances For
def
CategoryTheory.Limits.preservesBinaryBiproductsOfPreservesBinaryProducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
:
A functor between preadditive categories that preserves (zero morphisms and) binary products preserves binary biproducts.
Instances For
def
CategoryTheory.Limits.preservesBinaryCoproductOfPreservesBinaryBiproduct
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{X : C}
{Y : C}
[CategoryTheory.Limits.PreservesBinaryBiproduct X Y F]
:
A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary coproducts.
Instances For
def
CategoryTheory.Limits.preservesBinaryCoproductsOfPreservesBinaryBiproducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Limits.PreservesBinaryBiproducts F]
:
A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary coproducts.
Instances For
def
CategoryTheory.Limits.preservesBinaryBiproductOfPreservesBinaryCoproduct
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{X : C}
{Y : C}
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.pair X Y) F]
:
A functor between preadditive categories that preserves (zero morphisms and) binary coproducts preserves binary biproducts.
Instances For
def
CategoryTheory.Limits.preservesBinaryBiproductsOfPreservesBinaryCoproducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
:
A functor between preadditive categories that preserves (zero morphisms and) binary coproducts preserves binary biproducts.