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 : ∑ j : J, CategoryTheory.CategoryStruct.comp (b.π j) (b.ι j) = CategoryTheory.CategoryStruct.id b.pt)
:
b.IsBilimit
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
- One or more equations did not get rendered due to their size.
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 : b.IsBilimit)
:
∑ j : J, CategoryTheory.CategoryStruct.comp (b.π j) (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 : ∑ j : J, CategoryTheory.CategoryStruct.comp (b.π j) (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 t.toCone)
:
t.IsBilimit
In a preadditive category, any finite bicone which is a limit cone is in fact a bilimit bicone.
Equations
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)
:
(CategoryTheory.Limits.Bicone.ofLimitCone ht).IsBilimit
We can turn any limit cone over a pair into a bilimit bicone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 t.toCocone)
:
t.IsBilimit
In a preadditive category, any finite bicone which is a colimit cocone is in fact a bilimit bicone.
Equations
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)
:
(CategoryTheory.Limits.Bicone.ofColimitCocone ht).IsBilimit
We can turn any limit cone over a pair into a bilimit bicone.
Equations
- One or more equations did not get rendered due to their size.
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.
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]
:
In any preadditive category, any biproduct satisfies
∑ 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 = ∑ j : 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 = ∑ j : J, CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j) (g j)
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 U : C}
{g : (j : J) → T ⟶ f j}
{h : (j : J) → f j ⟶ U}
:
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 U : C}
{g : (j : J) → T ⟶ f j}
{h : (j : J) → f j ⟶ U}
{Z : C}
(h✝ : U ⟶ Z)
:
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 g : J → C}
{h : (j : J) → f j ⟶ g j}
:
theorem
CategoryTheory.Limits.biproduct.lift_matrix
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type}
[Fintype J]
{K : Type}
[Finite 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 : K) => ∑ j : J, CategoryTheory.CategoryStruct.comp (x j) (m j 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}
[Finite 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 : ⨁ g ⟶ 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 : K) => ∑ j : J, CategoryTheory.CategoryStruct.comp (x j) (m j k)) h
theorem
CategoryTheory.Limits.biproduct.matrix_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J K : Type}
[Finite J]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[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)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m) (CategoryTheory.Limits.biproduct.desc x) = CategoryTheory.Limits.biproduct.desc fun (j : J) => ∑ k : K, CategoryTheory.CategoryStruct.comp (m j k) (x k)
theorem
CategoryTheory.Limits.biproduct.matrix_desc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J K : Type}
[Finite J]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[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)
{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 : J) => ∑ k : K, CategoryTheory.CategoryStruct.comp (m j k) (x k)) h
theorem
CategoryTheory.Limits.biproduct.matrix_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J K : Type}
[Finite J]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[Finite K]
{f : J → C}
{g h : K → C}
(m : (j : J) → (k : K) → f j ⟶ g k)
(n : (k : K) → g k ⟶ h k)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m) (CategoryTheory.Limits.biproduct.map n) = CategoryTheory.Limits.biproduct.matrix fun (j : J) (k : K) => CategoryTheory.CategoryStruct.comp (m j k) (n k)
theorem
CategoryTheory.Limits.biproduct.matrix_map_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J K : Type}
[Finite J]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[Finite K]
{f : J → C}
{g h : K → C}
(m : (j : J) → (k : K) → f j ⟶ g k)
(n : (k : K) → g k ⟶ h k)
{Z : C}
(h✝ : ⨁ h ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map n) h✝) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.biproduct.matrix fun (j : J) (k : K) => CategoryTheory.CategoryStruct.comp (m j k) (n k)) h✝
theorem
CategoryTheory.Limits.biproduct.map_matrix
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J K : Type}
[Finite J]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[Finite K]
{f g : J → C}
{h : K → C}
(m : (k : J) → f k ⟶ g k)
(n : (j : J) → (k : K) → g j ⟶ h k)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map m) (CategoryTheory.Limits.biproduct.matrix n) = CategoryTheory.Limits.biproduct.matrix fun (j : J) (k : K) => CategoryTheory.CategoryStruct.comp (m j) (n j k)
theorem
CategoryTheory.Limits.biproduct.map_matrix_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J K : Type}
[Finite J]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[Finite K]
{f 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✝ : ⨁ h ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map m)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix n) h✝) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.biproduct.matrix fun (j : J) (k : K) => CategoryTheory.CategoryStruct.comp (m j) (n j k)) h✝
def
CategoryTheory.Limits.biproduct.reindex
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{β γ : Type}
[Finite β]
(ε : β ≃ γ)
(f : γ → C)
[CategoryTheory.Limits.HasBiproduct f]
[CategoryTheory.Limits.HasBiproduct (f ∘ ⇑ε)]
:
Reindex a categorical biproduct via an equivalence of the index types.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.biproduct.reindex_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{β γ : Type}
[Finite β]
(ε : β ≃ γ)
(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)
@[simp]
theorem
CategoryTheory.Limits.biproduct.reindex_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{β γ : Type}
[Finite β]
(ε : β ≃ γ)
(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)
def
CategoryTheory.Limits.isBinaryBilimitOfTotal
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X 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)
:
b.IsBilimit
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
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Limits.IsBilimit.binary_total
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
{b : CategoryTheory.Limits.BinaryBicone X Y}
(i : b.IsBilimit)
:
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 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.)
def
CategoryTheory.Limits.BinaryBicone.ofLimitCone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.BinaryBicone.ofLimitCone_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
{t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)}
(ht : CategoryTheory.Limits.IsLimit t)
:
(CategoryTheory.Limits.BinaryBicone.ofLimitCone ht).pt = t.pt
@[simp]
theorem
CategoryTheory.Limits.BinaryBicone.ofLimitCone_inl
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
{t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)}
(ht : CategoryTheory.Limits.IsLimit t)
:
@[simp]
theorem
CategoryTheory.Limits.BinaryBicone.ofLimitCone_inr
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X 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 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_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X 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 }
theorem
CategoryTheory.Limits.inl_of_isLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
{t : CategoryTheory.Limits.BinaryBicone X Y}
(ht : CategoryTheory.Limits.IsLimit t.toCone)
:
t.inl = ht.lift (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.id X) 0)
theorem
CategoryTheory.Limits.inr_of_isLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
{t : CategoryTheory.Limits.BinaryBicone X Y}
(ht : CategoryTheory.Limits.IsLimit t.toCone)
:
t.inr = ht.lift (CategoryTheory.Limits.BinaryFan.mk 0 (CategoryTheory.CategoryStruct.id Y))
def
CategoryTheory.Limits.isBinaryBilimitOfIsLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
(t : CategoryTheory.Limits.BinaryBicone X Y)
(ht : CategoryTheory.Limits.IsLimit t.toCone)
:
t.IsBilimit
In a preadditive category, any binary bicone which is a limit cone is in fact a bilimit bicone.
Equations
Instances For
def
CategoryTheory.Limits.binaryBiconeIsBilimitOfLimitConeOfIsLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
{t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)}
(ht : CategoryTheory.Limits.IsLimit t)
:
(CategoryTheory.Limits.BinaryBicone.ofLimitCone ht).IsBilimit
We can turn any limit cone over a pair into a bilimit bicone.
Equations
Instances For
theorem
CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryProduct
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(X 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.
def
CategoryTheory.Limits.BinaryBicone.ofColimitCocone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.BinaryBicone.ofColimitCocone_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X 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 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_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
{t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)}
(ht : CategoryTheory.Limits.IsColimit t)
:
@[simp]
theorem
CategoryTheory.Limits.BinaryBicone.ofColimitCocone_inl
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X 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_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
{t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)}
(ht : CategoryTheory.Limits.IsColimit t)
:
(CategoryTheory.Limits.BinaryBicone.ofColimitCocone ht).pt = t.pt
theorem
CategoryTheory.Limits.fst_of_isColimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
{t : CategoryTheory.Limits.BinaryBicone X Y}
(ht : CategoryTheory.Limits.IsColimit t.toCocone)
:
t.fst = ht.desc (CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.CategoryStruct.id X) 0)
theorem
CategoryTheory.Limits.snd_of_isColimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
{t : CategoryTheory.Limits.BinaryBicone X Y}
(ht : CategoryTheory.Limits.IsColimit t.toCocone)
:
t.snd = ht.desc (CategoryTheory.Limits.BinaryCofan.mk 0 (CategoryTheory.CategoryStruct.id Y))
def
CategoryTheory.Limits.isBinaryBilimitOfIsColimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
(t : CategoryTheory.Limits.BinaryBicone X Y)
(ht : CategoryTheory.Limits.IsColimit t.toCocone)
:
t.IsBilimit
In a preadditive category, any binary bicone which is a colimit cocone is in fact a bilimit bicone.
Equations
Instances For
def
CategoryTheory.Limits.binaryBiconeIsBilimitOfColimitCoconeOfIsColimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
{t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)}
(ht : CategoryTheory.Limits.IsColimit t)
:
(CategoryTheory.Limits.BinaryBicone.ofColimitCocone ht).IsBilimit
We can turn any colimit cocone over a pair into a bilimit bicone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryCoproduct
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(X 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 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 satisfies
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 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 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
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
[CategoryTheory.Limits.HasBinaryBiproduct X Y]
{T U : C}
{f : T ⟶ X}
{g : T ⟶ Y}
{h : X ⟶ U}
{i : Y ⟶ U}
:
@[simp]
theorem
CategoryTheory.Limits.biprod.lift_desc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
[CategoryTheory.Limits.HasBinaryBiproduct X Y]
{T U : C}
{f : T ⟶ X}
{g : T ⟶ Y}
{h : X ⟶ U}
{i : Y ⟶ U}
{Z : C}
(h✝ : U ⟶ Z)
:
theorem
CategoryTheory.Limits.biprod.map_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{W X Y 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)
def
CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X 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 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) ⋯;
let i' := CategoryTheory.Limits.isCokernelEpiComp i (CategoryTheory.retraction f) ⋯;
let i'' := CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork i';
(CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork C ⋯ i'').section_
@[simp]
theorem
CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
{f : X ⟶ Y}
[CategoryTheory.IsSplitMono f]
{c : CategoryTheory.Limits.CokernelCofork f}
(i : CategoryTheory.Limits.IsColimit c)
:
@[simp]
theorem
CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_inl
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X 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 Y : C}
{f : X ⟶ Y}
[CategoryTheory.IsSplitMono f]
{c : CategoryTheory.Limits.CokernelCofork f}
(i : CategoryTheory.Limits.IsColimit c)
:
def
CategoryTheory.Limits.isBilimitBinaryBiconeOfIsSplitMonoOfCokernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X 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.
Equations
Instances For
def
CategoryTheory.Limits.BinaryBicone.isBilimitOfKernelInl
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
(b : CategoryTheory.Limits.BinaryBicone X Y)
(hb : CategoryTheory.Limits.IsLimit b.sndKernelFork)
:
b.IsBilimit
If b is a binary bicone such that b.inl is a kernel of b.snd, then b is a bilimit
bicone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Limits.BinaryBicone.isBilimitOfKernelInr
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
(b : CategoryTheory.Limits.BinaryBicone X Y)
(hb : CategoryTheory.Limits.IsLimit b.fstKernelFork)
:
b.IsBilimit
If b is a binary bicone such that b.inr is a kernel of b.fst, then b is a bilimit
bicone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Limits.BinaryBicone.isBilimitOfCokernelFst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
(b : CategoryTheory.Limits.BinaryBicone X Y)
(hb : CategoryTheory.Limits.IsColimit b.inrCokernelCofork)
:
b.IsBilimit
If b is a binary bicone such that b.fst is a cokernel of b.inr, then b is a bilimit
bicone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Limits.BinaryBicone.isBilimitOfCokernelSnd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
(b : CategoryTheory.Limits.BinaryBicone X Y)
(hb : CategoryTheory.Limits.IsColimit b.inlCokernelCofork)
:
b.IsBilimit
If b is a binary bicone such that b.snd is a cokernel of b.inl, then b is a bilimit
bicone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X 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) ⋯;
let i' := CategoryTheory.Limits.isKernelCompMono i (CategoryTheory.section_ f) ⋯;
let i'' := CategoryTheory.Preadditive.isLimitForkOfKernelFork i';
(CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork C ⋯ i'').retraction
@[simp]
theorem
CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_inr
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X 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 Y : C}
{f : X ⟶ Y}
[CategoryTheory.IsSplitEpi f]
{c : CategoryTheory.Limits.KernelFork f}
(i : CategoryTheory.Limits.IsLimit c)
:
@[simp]
theorem
CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_inl
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
{f : X ⟶ Y}
[CategoryTheory.IsSplitEpi f]
{c : CategoryTheory.Limits.KernelFork f}
(i : CategoryTheory.Limits.IsLimit c)
:
@[simp]
theorem
CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
{f : X ⟶ Y}
[CategoryTheory.IsSplitEpi f]
{c : CategoryTheory.Limits.KernelFork f}
(i : CategoryTheory.Limits.IsLimit c)
:
def
CategoryTheory.Limits.isBilimitBinaryBiconeOfIsSplitEpiOfKernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
{f : X ⟶ Y}
[CategoryTheory.IsSplitEpi f]
{c : CategoryTheory.Limits.KernelFork f}
(i : CategoryTheory.Limits.IsLimit c)
:
(CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel i).IsBilimit
The bicone constructed in binaryBiconeOfIsSplitEpiOfKernel is a bilimit.
This is a version of the splitting lemma that holds in all preadditive categories.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Limits.biprod.add_eq_lift_id_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
(f 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 Y : C}
(f 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}
(homGroup : CategoryTheory.Preadditive.homGroup = CategoryTheory.Preadditive.homGroup)
:
x = y
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₁ X₂ Y₁ Y₂ : C}
(f₁₁ : X₁ ⟶ Y₁)
(f₁₂ : X₁ ⟶ Y₂)
(f₂₁ : X₂ ⟶ Y₁)
(f₂₂ : X₂ ⟶ Y₂)
:
The "matrix" morphism X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂ with specified components.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Biprod.inl_ofComponents
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ X₂ Y₁ 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₁ X₂ Y₁ 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₁ X₂ Y₁ 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₁ X₂ Y₁ 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₁ X₂ Y₁ 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₁ 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₂)
:
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₂₂)
def
CategoryTheory.Biprod.unipotentUpper
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ X₂ : C}
(r : X₁ ⟶ X₂)
:
The unipotent upper triangular matrix
(1 r)
(0 1)
as an isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Biprod.unipotentUpper_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ 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₁ 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₁ X₂ : C}
(r : X₂ ⟶ X₁)
:
The unipotent lower triangular matrix
(1 0)
(r 1)
as an isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Biprod.unipotentLower_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ 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₁ X₂ : C}
(r : X₂ ⟶ X₁)
:
def
CategoryTheory.Biprod.gaussian'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ X₂ Y₁ 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.)
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Biprod.gaussian
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ X₂ Y₁ 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Biprod.isoElim'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ X₂ Y₁ 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Biprod.isoElim
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X₁ X₂ Y₁ 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.
Equations
- One or more equations did not get rendered due to their size.
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 X Y 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}
[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}
[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.
Equations
Instances For
theorem
CategoryTheory.Limits.preservesProduct_of_preservesBiproduct
{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)
[F.PreservesZeroMorphisms]
{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.
theorem
CategoryTheory.Limits.preservesProductsOfShape_of_preservesBiproductsOfShape
{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)
[F.PreservesZeroMorphisms]
{J : Type}
[Fintype J]
[CategoryTheory.Limits.PreservesBiproductsOfShape J F]
:
A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite products.
theorem
CategoryTheory.Limits.preservesBiproduct_of_preservesProduct
{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)
[F.PreservesZeroMorphisms]
{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.
theorem
CategoryTheory.Limits.preservesBiproduct_of_mono_biproductComparison
{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)
[F.PreservesZeroMorphisms]
{J : Type}
[Fintype J]
{f : J → C}
[CategoryTheory.Limits.HasBiproduct f]
[CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)]
[CategoryTheory.Mono (F.biproductComparison 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.
theorem
CategoryTheory.Limits.preservesBiproduct_of_epi_biproductComparison'
{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)
[F.PreservesZeroMorphisms]
{J : Type}
[Fintype J]
{f : J → C}
[CategoryTheory.Limits.HasBiproduct f]
[CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)]
[CategoryTheory.Epi (F.biproductComparison' 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.
theorem
CategoryTheory.Limits.preservesBiproductsOfShape_of_preservesProductsOfShape
{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)
[F.PreservesZeroMorphisms]
{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.
theorem
CategoryTheory.Limits.preservesCoproduct_of_preservesBiproduct
{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)
[F.PreservesZeroMorphisms]
{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.
theorem
CategoryTheory.Limits.preservesCoproductsOfShape_of_preservesBiproductsOfShape
{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)
[F.PreservesZeroMorphisms]
{J : Type}
[Fintype J]
[CategoryTheory.Limits.PreservesBiproductsOfShape J F]
:
A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite coproducts.
theorem
CategoryTheory.Limits.preservesBiproduct_of_preservesCoproduct
{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)
[F.PreservesZeroMorphisms]
{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.
theorem
CategoryTheory.Limits.preservesBiproductsOfShape_of_preservesCoproductsOfShape
{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)
[F.PreservesZeroMorphisms]
{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.
theorem
CategoryTheory.Limits.preservesBinaryProduct_of_preservesBinaryBiproduct
{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)
[F.PreservesZeroMorphisms]
{X Y : C}
[CategoryTheory.Limits.PreservesBinaryBiproduct X Y F]
:
A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary products.
theorem
CategoryTheory.Limits.preservesBinaryProducts_of_preservesBinaryBiproducts
{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)
[F.PreservesZeroMorphisms]
[CategoryTheory.Limits.PreservesBinaryBiproducts F]
:
A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary products.
theorem
CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBinaryProduct
{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)
[F.PreservesZeroMorphisms]
{X 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.
theorem
CategoryTheory.Limits.preservesBinaryBiproduct_of_mono_biprodComparison
{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)
[F.PreservesZeroMorphisms]
{X Y : C}
[CategoryTheory.Limits.HasBinaryBiproduct X Y]
[CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)]
[CategoryTheory.Mono (F.biprodComparison 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.
theorem
CategoryTheory.Limits.preservesBinaryBiproduct_of_epi_biprodComparison'
{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)
[F.PreservesZeroMorphisms]
{X Y : C}
[CategoryTheory.Limits.HasBinaryBiproduct X Y]
[CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)]
[CategoryTheory.Epi (F.biprodComparison' 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.
theorem
CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBinaryProducts
{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)
[F.PreservesZeroMorphisms]
[CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
:
A functor between preadditive categories that preserves (zero morphisms and) binary products preserves binary biproducts.
theorem
CategoryTheory.Limits.preservesBinaryCoproduct_of_preservesBinaryBiproduct
{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)
[F.PreservesZeroMorphisms]
{X Y : C}
[CategoryTheory.Limits.PreservesBinaryBiproduct X Y F]
:
A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary coproducts.
theorem
CategoryTheory.Limits.preservesBinaryCoproducts_of_preservesBinaryBiproducts
{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)
[F.PreservesZeroMorphisms]
[CategoryTheory.Limits.PreservesBinaryBiproducts F]
:
A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary coproducts.
theorem
CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBinaryCoproduct
{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)
[F.PreservesZeroMorphisms]
{X 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.
theorem
CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBinaryCoproducts
{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)
[F.PreservesZeroMorphisms]
[CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
:
A functor between preadditive categories that preserves (zero morphisms and) binary coproducts preserves binary biproducts.