Basic facts about biproducts in preadditive categories. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
linear_algebra.matrix.schur_complement). In particular, the declarations
category_theory.biprod.iso_elim, category_theory.biprod.gaussian
and matrix.invertible_of_from_blocks₁₁_invertible are all closely related.
def
category_theory.limits.is_bilimit_of_total
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[fintype J]
{f : J → C}
(b : category_theory.limits.bicone f)
(total : finset.univ.sum (λ (j : J), b.π j ≫ b.ι j) = 𝟙 b.X) :
In a preadditive category, we can construct a biproduct for f : J → C from
any bicone b for f satisfying total : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.X.
(That is, such a bicone is a limit cone and a colimit cocone.)
Equations
- category_theory.limits.is_bilimit_of_total b total = {is_limit := {lift := λ (s : category_theory.limits.cone (category_theory.discrete.functor f)), finset.univ.sum (λ (j : J), s.π.app {as := j} ≫ b.ι j), fac' := _, uniq' := _}, is_colimit := {desc := λ (s : category_theory.limits.cocone (category_theory.discrete.functor f)), finset.univ.sum (λ (j : J), b.π j ≫ s.ι.app {as := j}), fac' := _, uniq' := _}}
theorem
category_theory.limits.is_bilimit.total
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[fintype J]
{f : J → C}
{b : category_theory.limits.bicone f}
(i : b.is_bilimit) :
theorem
category_theory.limits.has_biproduct_of_total
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[fintype J]
{f : J → C}
(b : category_theory.limits.bicone f)
(total : finset.univ.sum (λ (j : J), b.π j ≫ b.ι j) = 𝟙 b.X) :
In a preadditive category, we can construct a biproduct for f : J → C from
any bicone b for f satisfying total : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.X.
(That is, such a bicone is a limit cone and a colimit cocone.)
def
category_theory.limits.is_bilimit_of_is_limit
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[fintype J]
{f : J → C}
(t : category_theory.limits.bicone f)
(ht : category_theory.limits.is_limit t.to_cone) :
In a preadditive category, any finite bicone which is a limit cone is in fact a bilimit bicone.
noncomputable
def
category_theory.limits.bicone_is_bilimit_of_limit_cone_of_is_limit
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[fintype J]
{f : J → C}
{t : category_theory.limits.cone (category_theory.discrete.functor f)}
(ht : category_theory.limits.is_limit t) :
We can turn any limit cone over a pair into a bilimit bicone.
theorem
category_theory.limits.has_biproduct.of_has_product
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[finite J]
(f : J → C)
[category_theory.limits.has_product f] :
In a preadditive category, if the product over f : J → C exists,
then the biproduct over f exists.
def
category_theory.limits.is_bilimit_of_is_colimit
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[fintype J]
{f : J → C}
(t : category_theory.limits.bicone f)
(ht : category_theory.limits.is_colimit t.to_cocone) :
In a preadditive category, any finite bicone which is a colimit cocone is in fact a bilimit bicone.
noncomputable
def
category_theory.limits.bicone_is_bilimit_of_colimit_cocone_of_is_colimit
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[fintype J]
{f : J → C}
{t : category_theory.limits.cocone (category_theory.discrete.functor f)}
(ht : category_theory.limits.is_colimit t) :
We can turn any limit cone over a pair into a bilimit bicone.
theorem
category_theory.limits.has_biproduct.of_has_coproduct
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[finite J]
(f : J → C)
[category_theory.limits.has_coproduct f] :
In a preadditive category, if the coproduct over f : J → C exists,
then the biproduct over f exists.
theorem
category_theory.limits.has_finite_biproducts.of_has_finite_products
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_products C] :
A preadditive category with finite products has finite biproducts.
theorem
category_theory.limits.has_finite_biproducts.of_has_finite_coproducts
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C] :
A preadditive category with finite coproducts has finite biproducts.
@[simp]
theorem
category_theory.limits.biproduct.total
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[fintype J]
{f : J → C}
[category_theory.limits.has_biproduct f] :
finset.univ.sum (λ (j : J), category_theory.limits.biproduct.π f j ≫ category_theory.limits.biproduct.ι f j) = 𝟙 (⨁ f)
In any preadditive category, any biproduct satsifies
∑ j : J, biproduct.π f j ≫ biproduct.ι f j = 𝟙 (⨁ f)
theorem
category_theory.limits.biproduct.lift_eq
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[fintype J]
{f : J → C}
[category_theory.limits.has_biproduct f]
{T : C}
{g : Π (j : J), T ⟶ f j} :
category_theory.limits.biproduct.lift g = finset.univ.sum (λ (j : J), g j ≫ category_theory.limits.biproduct.ι f j)
theorem
category_theory.limits.biproduct.desc_eq
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[fintype J]
{f : J → C}
[category_theory.limits.has_biproduct f]
{T : C}
{g : Π (j : J), f j ⟶ T} :
category_theory.limits.biproduct.desc g = finset.univ.sum (λ (j : J), category_theory.limits.biproduct.π f j ≫ g j)
@[simp]
theorem
category_theory.limits.biproduct.lift_desc
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[fintype J]
{f : J → C}
[category_theory.limits.has_biproduct f]
{T U : C}
{g : Π (j : J), T ⟶ f j}
{h : Π (j : J), f j ⟶ U} :
category_theory.limits.biproduct.lift g ≫ category_theory.limits.biproduct.desc h = finset.univ.sum (λ (j : J), g j ≫ h j)
@[simp]
theorem
category_theory.limits.biproduct.lift_desc_assoc
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[fintype J]
{f : J → C}
[category_theory.limits.has_biproduct f]
{T U : C}
{g : Π (j : J), T ⟶ f j}
{h : Π (j : J), f j ⟶ U}
{X' : C}
(f' : U ⟶ X') :
category_theory.limits.biproduct.lift g ≫ category_theory.limits.biproduct.desc h ≫ f' = finset.univ.sum (λ (j : J), g j ≫ h j) ≫ f'
theorem
category_theory.limits.biproduct.map_eq
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[fintype J]
[category_theory.limits.has_finite_biproducts C]
{f g : J → C}
{h : Π (j : J), f j ⟶ g j} :
category_theory.limits.biproduct.map h = finset.univ.sum (λ (j : J), category_theory.limits.biproduct.π f j ≫ h j ≫ category_theory.limits.biproduct.ι g j)
@[simp]
theorem
category_theory.limits.biproduct.matrix_desc_assoc
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[fintype J]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
{f : J → C}
{g : K → C}
(m : Π (j : J) (k : K), f j ⟶ g k)
{P : C}
(x : Π (k : K), g k ⟶ P)
{X' : C}
(f' : P ⟶ X') :
category_theory.limits.biproduct.matrix m ≫ category_theory.limits.biproduct.desc x ≫ f' = category_theory.limits.biproduct.desc (λ (j : J), finset.univ.sum (λ (k : K), m j k ≫ x k)) ≫ f'
@[simp]
theorem
category_theory.limits.biproduct.matrix_desc
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[fintype J]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
{f : J → C}
{g : K → C}
(m : Π (j : J) (k : K), f j ⟶ g k)
{P : C}
(x : Π (k : K), g k ⟶ P) :
category_theory.limits.biproduct.matrix m ≫ category_theory.limits.biproduct.desc x = category_theory.limits.biproduct.desc (λ (j : J), finset.univ.sum (λ (k : K), m j k ≫ x k))
@[simp]
theorem
category_theory.limits.biproduct.lift_matrix
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[fintype J]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
{f : J → C}
{g : K → C}
{P : C}
(x : Π (j : J), P ⟶ f j)
(m : Π (j : J) (k : K), f j ⟶ g k) :
category_theory.limits.biproduct.lift x ≫ category_theory.limits.biproduct.matrix m = category_theory.limits.biproduct.lift (λ (k : K), finset.univ.sum (λ (j : J), x j ≫ m j k))
@[simp]
theorem
category_theory.limits.biproduct.lift_matrix_assoc
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[fintype J]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
{f : J → C}
{g : K → C}
{P : C}
(x : Π (j : J), P ⟶ f j)
(m : Π (j : J) (k : K), f j ⟶ g k)
{X' : C}
(f' : (⨁ λ (k : K), g k) ⟶ X') :
category_theory.limits.biproduct.lift x ≫ category_theory.limits.biproduct.matrix m ≫ f' = category_theory.limits.biproduct.lift (λ (k : K), finset.univ.sum (λ (j : J), x j ≫ m j k)) ≫ f'
theorem
category_theory.limits.biproduct.matrix_map_assoc
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[fintype J]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
{f : J → C}
{g h : K → C}
(m : Π (j : J) (k : K), f j ⟶ g k)
(n : Π (k : K), g k ⟶ h k)
{X' : C}
(f' : (⨁ λ (k : K), h k) ⟶ X') :
category_theory.limits.biproduct.matrix m ≫ category_theory.limits.biproduct.map n ≫ f' = category_theory.limits.biproduct.matrix (λ (j : J) (k : K), m j k ≫ n k) ≫ f'
theorem
category_theory.limits.biproduct.matrix_map
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[fintype J]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
{f : J → C}
{g h : K → C}
(m : Π (j : J) (k : K), f j ⟶ g k)
(n : Π (k : K), g k ⟶ h k) :
category_theory.limits.biproduct.matrix m ≫ category_theory.limits.biproduct.map n = category_theory.limits.biproduct.matrix (λ (j : J) (k : K), m j k ≫ n k)
theorem
category_theory.limits.biproduct.map_matrix
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[fintype J]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
{f g : J → C}
{h : K → C}
(m : Π (k : J), f k ⟶ g k)
(n : Π (j : J) (k : K), g j ⟶ h k) :
category_theory.limits.biproduct.map m ≫ category_theory.limits.biproduct.matrix n = category_theory.limits.biproduct.matrix (λ (j : J) (k : K), m j ≫ n j k)
theorem
category_theory.limits.biproduct.map_matrix_assoc
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type}
[fintype J]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
{f g : J → C}
{h : K → C}
(m : Π (k : J), f k ⟶ g k)
(n : Π (j : J) (k : K), g j ⟶ h k)
{X' : C}
(f' : (⨁ λ (k : K), h k) ⟶ X') :
category_theory.limits.biproduct.map m ≫ category_theory.limits.biproduct.matrix n ≫ f' = category_theory.limits.biproduct.matrix (λ (j : J) (k : K), m j ≫ n j k) ≫ f'
@[simp]
theorem
category_theory.limits.biproduct.reindex_inv
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{β γ : Type}
[fintype β]
[decidable_eq β]
[decidable_eq γ]
(ε : β ≃ γ)
(f : γ → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (f ∘ ⇑ε)] :
(category_theory.limits.biproduct.reindex ε f).inv = category_theory.limits.biproduct.lift (λ (b : β), category_theory.limits.biproduct.π f (⇑ε b))
@[simp]
theorem
category_theory.limits.biproduct.reindex_hom
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{β γ : Type}
[fintype β]
[decidable_eq β]
[decidable_eq γ]
(ε : β ≃ γ)
(f : γ → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (f ∘ ⇑ε)] :
(category_theory.limits.biproduct.reindex ε f).hom = category_theory.limits.biproduct.desc (λ (b : β), category_theory.limits.biproduct.ι f (⇑ε b))
noncomputable
def
category_theory.limits.biproduct.reindex
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{β γ : Type}
[fintype β]
[decidable_eq β]
[decidable_eq γ]
(ε : β ≃ γ)
(f : γ → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (f ∘ ⇑ε)] :
Reindex a categorical biproduct via an equivalence of the index types.
Equations
- category_theory.limits.biproduct.reindex ε f = {hom := category_theory.limits.biproduct.desc (λ (b : β), category_theory.limits.biproduct.ι f (⇑ε b)), inv := category_theory.limits.biproduct.lift (λ (b : β), category_theory.limits.biproduct.π f (⇑ε b)), hom_inv_id' := _, inv_hom_id' := _}
def
category_theory.limits.is_binary_bilimit_of_total
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
(b : category_theory.limits.binary_bicone X Y)
(total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.X) :
In a preadditive category, we can construct a binary biproduct for X Y : C from
any binary bicone b satisfying total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.X.
(That is, such a bicone is a limit cone and a colimit cocone.)
Equations
- category_theory.limits.is_binary_bilimit_of_total b total = {is_limit := {lift := λ (s : category_theory.limits.cone (category_theory.limits.pair X Y)), category_theory.limits.binary_fan.fst s ≫ b.inl + category_theory.limits.binary_fan.snd s ≫ b.inr, fac' := _, uniq' := _}, is_colimit := {desc := λ (s : category_theory.limits.cocone (category_theory.limits.pair X Y)), b.fst ≫ category_theory.limits.binary_cofan.inl s + b.snd ≫ category_theory.limits.binary_cofan.inr s, fac' := _, uniq' := _}}
theorem
category_theory.limits.is_bilimit.binary_total
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{b : category_theory.limits.binary_bicone X Y}
(i : b.is_bilimit) :
theorem
category_theory.limits.has_binary_biproduct_of_total
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
(b : category_theory.limits.binary_bicone X Y)
(total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.X) :
In a preadditive category, we can construct a binary biproduct for X Y : C from
any binary bicone b satisfying total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.X.
(That is, such a bicone is a limit cone and a colimit cocone.)
@[simp]
theorem
category_theory.limits.binary_bicone.of_limit_cone_inl
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{t : category_theory.limits.cone (category_theory.limits.pair X Y)}
(ht : category_theory.limits.is_limit t) :
@[simp]
theorem
category_theory.limits.binary_bicone.of_limit_cone_fst
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{t : category_theory.limits.cone (category_theory.limits.pair X Y)}
(ht : category_theory.limits.is_limit t) :
@[simp]
theorem
category_theory.limits.binary_bicone.of_limit_cone_snd
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{t : category_theory.limits.cone (category_theory.limits.pair X Y)}
(ht : category_theory.limits.is_limit t) :
def
category_theory.limits.binary_bicone.of_limit_cone
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{t : category_theory.limits.cone (category_theory.limits.pair X Y)}
(ht : category_theory.limits.is_limit t) :
We can turn any limit cone over a pair into a bicone.
Equations
- category_theory.limits.binary_bicone.of_limit_cone ht = {X := t.X, fst := t.π.app {as := category_theory.limits.walking_pair.left}, snd := t.π.app {as := category_theory.limits.walking_pair.right}, inl := ht.lift (category_theory.limits.binary_fan.mk (𝟙 X) 0), inr := ht.lift (category_theory.limits.binary_fan.mk 0 (𝟙 Y)), inl_fst' := _, inl_snd' := _, inr_fst' := _, inr_snd' := _}
@[simp]
theorem
category_theory.limits.binary_bicone.of_limit_cone_X
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{t : category_theory.limits.cone (category_theory.limits.pair X Y)}
(ht : category_theory.limits.is_limit t) :
@[simp]
theorem
category_theory.limits.binary_bicone.of_limit_cone_inr
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{t : category_theory.limits.cone (category_theory.limits.pair X Y)}
(ht : category_theory.limits.is_limit t) :
theorem
category_theory.limits.inl_of_is_limit
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{t : category_theory.limits.binary_bicone X Y}
(ht : category_theory.limits.is_limit t.to_cone) :
t.inl = ht.lift (category_theory.limits.binary_fan.mk (𝟙 X) 0)
theorem
category_theory.limits.inr_of_is_limit
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{t : category_theory.limits.binary_bicone X Y}
(ht : category_theory.limits.is_limit t.to_cone) :
t.inr = ht.lift (category_theory.limits.binary_fan.mk 0 (𝟙 Y))
def
category_theory.limits.is_binary_bilimit_of_is_limit
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
(t : category_theory.limits.binary_bicone X Y)
(ht : category_theory.limits.is_limit t.to_cone) :
In a preadditive category, any binary bicone which is a limit cone is in fact a bilimit bicone.
def
category_theory.limits.binary_bicone_is_bilimit_of_limit_cone_of_is_limit
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{t : category_theory.limits.cone (category_theory.limits.pair X Y)}
(ht : category_theory.limits.is_limit t) :
We can turn any limit cone over a pair into a bilimit bicone.
theorem
category_theory.limits.has_binary_biproduct.of_has_binary_product
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
(X Y : C)
[category_theory.limits.has_binary_product X Y] :
In a preadditive category, if the product of X and Y exists, then the
binary biproduct of X and Y exists.
theorem
category_theory.limits.has_binary_biproducts.of_has_binary_products
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_products C] :
In a preadditive category, if all binary products exist, then all binary biproducts exist.
@[simp]
theorem
category_theory.limits.binary_bicone.of_colimit_cocone_inr
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{t : category_theory.limits.cocone (category_theory.limits.pair X Y)}
(ht : category_theory.limits.is_colimit t) :
@[simp]
theorem
category_theory.limits.binary_bicone.of_colimit_cocone_fst
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{t : category_theory.limits.cocone (category_theory.limits.pair X Y)}
(ht : category_theory.limits.is_colimit t) :
@[simp]
theorem
category_theory.limits.binary_bicone.of_colimit_cocone_snd
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{t : category_theory.limits.cocone (category_theory.limits.pair X Y)}
(ht : category_theory.limits.is_colimit t) :
def
category_theory.limits.binary_bicone.of_colimit_cocone
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{t : category_theory.limits.cocone (category_theory.limits.pair X Y)}
(ht : category_theory.limits.is_colimit t) :
We can turn any colimit cocone over a pair into a bicone.
Equations
- category_theory.limits.binary_bicone.of_colimit_cocone ht = {X := t.X, fst := ht.desc (category_theory.limits.binary_cofan.mk (𝟙 X) 0), snd := ht.desc (category_theory.limits.binary_cofan.mk 0 (𝟙 Y)), inl := t.ι.app {as := category_theory.limits.walking_pair.left}, inr := t.ι.app {as := category_theory.limits.walking_pair.right}, inl_fst' := _, inl_snd' := _, inr_fst' := _, inr_snd' := _}
@[simp]
theorem
category_theory.limits.binary_bicone.of_colimit_cocone_inl
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{t : category_theory.limits.cocone (category_theory.limits.pair X Y)}
(ht : category_theory.limits.is_colimit t) :
@[simp]
theorem
category_theory.limits.binary_bicone.of_colimit_cocone_X
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{t : category_theory.limits.cocone (category_theory.limits.pair X Y)}
(ht : category_theory.limits.is_colimit t) :
theorem
category_theory.limits.fst_of_is_colimit
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{t : category_theory.limits.binary_bicone X Y}
(ht : category_theory.limits.is_colimit t.to_cocone) :
t.fst = ht.desc (category_theory.limits.binary_cofan.mk (𝟙 X) 0)
theorem
category_theory.limits.snd_of_is_colimit
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{t : category_theory.limits.binary_bicone X Y}
(ht : category_theory.limits.is_colimit t.to_cocone) :
t.snd = ht.desc (category_theory.limits.binary_cofan.mk 0 (𝟙 Y))
def
category_theory.limits.is_binary_bilimit_of_is_colimit
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
(t : category_theory.limits.binary_bicone X Y)
(ht : category_theory.limits.is_colimit t.to_cocone) :
In a preadditive category, any binary bicone which is a colimit cocone is in fact a bilimit bicone.
def
category_theory.limits.binary_bicone_is_bilimit_of_colimit_cocone_of_is_colimit
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{t : category_theory.limits.cocone (category_theory.limits.pair X Y)}
(ht : category_theory.limits.is_colimit t) :
We can turn any colimit cocone over a pair into a bilimit bicone.
theorem
category_theory.limits.has_binary_biproduct.of_has_binary_coproduct
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
(X Y : C)
[category_theory.limits.has_binary_coproduct X Y] :
In a preadditive category, if the coproduct of X and Y exists, then the
binary biproduct of X and Y exists.
theorem
category_theory.limits.has_binary_biproducts.of_has_binary_coproducts
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_coproducts C] :
In a preadditive category, if all binary coproducts exist, then all binary biproducts exist.
@[simp]
theorem
category_theory.limits.biprod.total
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
In any preadditive category, any binary biproduct satsifies
biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr = 𝟙 (X ⊞ Y).
theorem
category_theory.limits.biprod.lift_eq
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
{T : C}
{f : T ⟶ X}
{g : T ⟶ Y} :
theorem
category_theory.limits.biprod.desc_eq
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
{T : C}
{f : X ⟶ T}
{g : Y ⟶ T} :
@[simp]
theorem
category_theory.limits.biprod.lift_desc
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
{T U : C}
{f : T ⟶ X}
{g : T ⟶ Y}
{h : X ⟶ U}
{i : Y ⟶ U} :
category_theory.limits.biprod.lift f g ≫ category_theory.limits.biprod.desc h i = f ≫ h + g ≫ i
@[simp]
theorem
category_theory.limits.biprod.lift_desc_assoc
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
{T U : C}
{f : T ⟶ X}
{g : T ⟶ Y}
{h : X ⟶ U}
{i : Y ⟶ U}
{X' : C}
(f' : U ⟶ X') :
category_theory.limits.biprod.lift f g ≫ category_theory.limits.biprod.desc h i ≫ f' = (f ≫ h + g ≫ i) ≫ f'
theorem
category_theory.limits.biprod.map_eq
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{W X Y Z : C}
{f : W ⟶ Y}
{g : X ⟶ Z} :
noncomputable
def
category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.is_split_mono f]
{c : category_theory.limits.cokernel_cofork f}
(i : category_theory.limits.is_colimit 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
- category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel i = {X := Y, fst := category_theory.retraction f _inst_5, snd := category_theory.limits.cofork.π c, inl := f, inr := let c' : category_theory.limits.cokernel_cofork (𝟙 Y - (𝟙 Y - category_theory.retraction f ≫ f)) := category_theory.limits.cokernel_cofork.of_π (category_theory.limits.cofork.π c) category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel._proof_1, i' : category_theory.limits.is_colimit c' := category_theory.limits.is_cokernel_epi_comp i (category_theory.retraction f) category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel._proof_3, i'' : category_theory.limits.is_colimit (category_theory.preadditive.cofork_of_cokernel_cofork c') := category_theory.preadditive.is_colimit_cofork_of_cokernel_cofork i' in (category_theory.limits.split_epi_of_idempotent_of_is_colimit_cofork C category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel._proof_4 i'').section_, inl_fst' := _, inl_snd' := _, inr_fst' := _, inr_snd' := _}
@[simp]
theorem
category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel_inl
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.is_split_mono f]
{c : category_theory.limits.cokernel_cofork f}
(i : category_theory.limits.is_colimit c) :
@[simp]
theorem
category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel_X
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.is_split_mono f]
{c : category_theory.limits.cokernel_cofork f}
(i : category_theory.limits.is_colimit c) :
@[simp]
theorem
category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel_fst
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.is_split_mono f]
{c : category_theory.limits.cokernel_cofork f}
(i : category_theory.limits.is_colimit c) :
@[simp]
theorem
category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel_inr
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.is_split_mono f]
{c : category_theory.limits.cokernel_cofork f}
(i : category_theory.limits.is_colimit c) :
(category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel i).inr = (category_theory.limits.split_epi_of_idempotent_of_is_colimit_cofork C category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel._proof_4 (category_theory.preadditive.is_colimit_cofork_of_cokernel_cofork (category_theory.limits.is_cokernel_epi_comp i (category_theory.retraction f) category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel._proof_3))).section_
@[simp]
theorem
category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel_snd
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.is_split_mono f]
{c : category_theory.limits.cokernel_cofork f}
(i : category_theory.limits.is_colimit c) :
noncomputable
def
category_theory.limits.is_bilimit_binary_bicone_of_is_split_mono_of_cokernel
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.is_split_mono f]
{c : category_theory.limits.cokernel_cofork f}
(i : category_theory.limits.is_colimit c) :
The bicone constructed in binary_bicone_of_split_mono_of_cokernel is a bilimit.
This is a version of the splitting lemma that holds in all preadditive categories.
def
category_theory.limits.binary_bicone.is_bilimit_of_kernel_inl
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
(b : category_theory.limits.binary_bicone X Y)
(hb : category_theory.limits.is_limit b.snd_kernel_fork) :
If b is a binary bicone such that b.inl is a kernel of b.snd, then b is a bilimit
bicone.
Equations
- b.is_bilimit_of_kernel_inl hb = category_theory.limits.is_binary_bilimit_of_is_limit b (category_theory.limits.binary_fan.is_limit.mk b.to_cone (λ (T : C) (f : T ⟶ X) (g : T ⟶ Y), f ≫ b.inl + g ≫ b.inr) _ _ _)
def
category_theory.limits.binary_bicone.is_bilimit_of_kernel_inr
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
(b : category_theory.limits.binary_bicone X Y)
(hb : category_theory.limits.is_limit b.fst_kernel_fork) :
If b is a binary bicone such that b.inr is a kernel of b.fst, then b is a bilimit
bicone.
Equations
- b.is_bilimit_of_kernel_inr hb = category_theory.limits.is_binary_bilimit_of_is_limit b (category_theory.limits.binary_fan.is_limit.mk b.to_cone (λ (T : C) (f : T ⟶ X) (g : T ⟶ Y), f ≫ b.inl + g ≫ b.inr) _ _ _)
def
category_theory.limits.binary_bicone.is_bilimit_of_cokernel_fst
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
(b : category_theory.limits.binary_bicone X Y)
(hb : category_theory.limits.is_colimit b.inr_cokernel_cofork) :
If b is a binary bicone such that b.fst is a cokernel of b.inr, then b is a bilimit
bicone.
Equations
- b.is_bilimit_of_cokernel_fst hb = category_theory.limits.is_binary_bilimit_of_is_colimit b (category_theory.limits.binary_cofan.is_colimit.mk b.to_cocone (λ (T : C) (f : X ⟶ T) (g : Y ⟶ T), b.fst ≫ f + b.snd ≫ g) _ _ _)
def
category_theory.limits.binary_bicone.is_bilimit_of_cokernel_snd
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
(b : category_theory.limits.binary_bicone X Y)
(hb : category_theory.limits.is_colimit b.inl_cokernel_cofork) :
If b is a binary bicone such that b.snd is a cokernel of b.inl, then b is a bilimit
bicone.
Equations
- b.is_bilimit_of_cokernel_snd hb = category_theory.limits.is_binary_bilimit_of_is_colimit b (category_theory.limits.binary_cofan.is_colimit.mk b.to_cocone (λ (T : C) (f : X ⟶ T) (g : Y ⟶ T), b.fst ≫ f + b.snd ≫ g) _ _ _)
@[simp]
theorem
category_theory.limits.binary_bicone_of_is_split_epi_of_kernel_snd
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.is_split_epi f]
{c : category_theory.limits.kernel_fork f}
(i : category_theory.limits.is_limit c) :
noncomputable
def
category_theory.limits.binary_bicone_of_is_split_epi_of_kernel
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.is_split_epi f]
{c : category_theory.limits.kernel_fork f}
(i : category_theory.limits.is_limit 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
- category_theory.limits.binary_bicone_of_is_split_epi_of_kernel i = {X := X, fst := let c' : category_theory.limits.kernel_fork (𝟙 X - (𝟙 X - f ≫ category_theory.section_ f)) := category_theory.limits.kernel_fork.of_ι (category_theory.limits.fork.ι c) category_theory.limits.binary_bicone_of_is_split_epi_of_kernel._proof_1, i' : category_theory.limits.is_limit c' := category_theory.limits.is_kernel_comp_mono i (category_theory.section_ f) category_theory.limits.binary_bicone_of_is_split_epi_of_kernel._proof_3, i'' : category_theory.limits.is_limit (category_theory.preadditive.fork_of_kernel_fork c') := category_theory.preadditive.is_limit_fork_of_kernel_fork i' in (category_theory.limits.split_mono_of_idempotent_of_is_limit_fork C category_theory.limits.binary_bicone_of_is_split_epi_of_kernel._proof_4 i'').retraction, snd := f, inl := category_theory.limits.fork.ι c, inr := category_theory.section_ f _inst_5, inl_fst' := _, inl_snd' := _, inr_fst' := _, inr_snd' := _}
@[simp]
theorem
category_theory.limits.binary_bicone_of_is_split_epi_of_kernel_inl
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.is_split_epi f]
{c : category_theory.limits.kernel_fork f}
(i : category_theory.limits.is_limit c) :
@[simp]
theorem
category_theory.limits.binary_bicone_of_is_split_epi_of_kernel_X
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.is_split_epi f]
{c : category_theory.limits.kernel_fork f}
(i : category_theory.limits.is_limit c) :
@[simp]
theorem
category_theory.limits.binary_bicone_of_is_split_epi_of_kernel_inr
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.is_split_epi f]
{c : category_theory.limits.kernel_fork f}
(i : category_theory.limits.is_limit c) :
@[simp]
theorem
category_theory.limits.binary_bicone_of_is_split_epi_of_kernel_fst
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.is_split_epi f]
{c : category_theory.limits.kernel_fork f}
(i : category_theory.limits.is_limit c) :
(category_theory.limits.binary_bicone_of_is_split_epi_of_kernel i).fst = (category_theory.limits.split_mono_of_idempotent_of_is_limit_fork C category_theory.limits.binary_bicone_of_is_split_epi_of_kernel._proof_4 (category_theory.preadditive.is_limit_fork_of_kernel_fork (category_theory.limits.is_kernel_comp_mono i (category_theory.section_ f) category_theory.limits.binary_bicone_of_is_split_epi_of_kernel._proof_3))).retraction
noncomputable
def
category_theory.limits.is_bilimit_binary_bicone_of_is_split_epi_of_kernel
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.is_split_epi f]
{c : category_theory.limits.kernel_fork f}
(i : category_theory.limits.is_limit c) :
The bicone constructed in binary_bicone_of_is_split_epi_of_kernel is a bilimit.
This is a version of the splitting lemma that holds in all preadditive categories.
theorem
category_theory.limits.biprod.add_eq_lift_id_desc
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
(f g : X ⟶ Y)
[category_theory.limits.has_binary_biproduct X X] :
f + g = category_theory.limits.biprod.lift (𝟙 X) (𝟙 X) ≫ category_theory.limits.biprod.desc f g
The existence of binary biproducts implies that there is at most one preadditive structure.
theorem
category_theory.limits.biprod.add_eq_lift_desc_id
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
(f g : X ⟶ Y)
[category_theory.limits.has_binary_biproduct Y Y] :
f + g = category_theory.limits.biprod.lift f g ≫ category_theory.limits.biprod.desc (𝟙 Y) (𝟙 Y)
The existence of binary biproducts implies that there is at most one preadditive structure.
theorem
category_theory.preadditive.ext_iff
{C : Type u}
{_inst_1 : category_theory.category C}
(x y : category_theory.preadditive C) :
theorem
category_theory.preadditive.ext
{C : Type u}
{_inst_1 : category_theory.category C}
(x y : category_theory.preadditive C)
(h : category_theory.preadditive.hom_group = category_theory.preadditive.hom_group) :
x = y
@[protected, instance]
def
category_theory.subsingleton_preadditive_of_has_binary_biproducts
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproducts C] :
The existence of binary biproducts implies that there is at most one preadditive structure.
noncomputable
def
category_theory.biprod.of_components
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts 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
- category_theory.biprod.of_components f₁₁ f₁₂ f₂₁ f₂₂ = category_theory.limits.biprod.fst ≫ f₁₁ ≫ category_theory.limits.biprod.inl + category_theory.limits.biprod.fst ≫ f₁₂ ≫ category_theory.limits.biprod.inr + category_theory.limits.biprod.snd ≫ f₂₁ ≫ category_theory.limits.biprod.inl + category_theory.limits.biprod.snd ≫ f₂₂ ≫ category_theory.limits.biprod.inr
@[simp]
theorem
category_theory.biprod.inl_of_components
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{X₁ X₂ Y₁ Y₂ : C}
(f₁₁ : X₁ ⟶ Y₁)
(f₁₂ : X₁ ⟶ Y₂)
(f₂₁ : X₂ ⟶ Y₁)
(f₂₂ : X₂ ⟶ Y₂) :
@[simp]
theorem
category_theory.biprod.inr_of_components
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{X₁ X₂ Y₁ Y₂ : C}
(f₁₁ : X₁ ⟶ Y₁)
(f₁₂ : X₁ ⟶ Y₂)
(f₂₁ : X₂ ⟶ Y₁)
(f₂₂ : X₂ ⟶ Y₂) :
@[simp]
theorem
category_theory.biprod.of_components_fst
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{X₁ X₂ Y₁ Y₂ : C}
(f₁₁ : X₁ ⟶ Y₁)
(f₁₂ : X₁ ⟶ Y₂)
(f₂₁ : X₂ ⟶ Y₁)
(f₂₂ : X₂ ⟶ Y₂) :
@[simp]
theorem
category_theory.biprod.of_components_snd
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{X₁ X₂ Y₁ Y₂ : C}
(f₁₁ : X₁ ⟶ Y₁)
(f₁₂ : X₁ ⟶ Y₂)
(f₂₁ : X₂ ⟶ Y₁)
(f₂₂ : X₂ ⟶ Y₂) :
@[simp]
theorem
category_theory.biprod.of_components_eq
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{X₁ X₂ Y₁ Y₂ : C}
(f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂) :
category_theory.biprod.of_components (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.snd) (category_theory.limits.biprod.inr ≫ f ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inr ≫ f ≫ category_theory.limits.biprod.snd) = f
@[simp]
theorem
category_theory.biprod.of_components_comp
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts 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₂) :
noncomputable
def
category_theory.biprod.unipotent_upper
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{X₁ X₂ : C}
(r : X₁ ⟶ X₂) :
The unipotent upper triangular matrix
(1 r)
(0 1)
as an isomorphism.
Equations
- category_theory.biprod.unipotent_upper r = {hom := category_theory.biprod.of_components (𝟙 X₁) r 0 (𝟙 X₂), inv := category_theory.biprod.of_components (𝟙 X₁) (-r) 0 (𝟙 X₂), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.biprod.unipotent_upper_hom
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{X₁ X₂ : C}
(r : X₁ ⟶ X₂) :
(category_theory.biprod.unipotent_upper r).hom = category_theory.biprod.of_components (𝟙 X₁) r 0 (𝟙 X₂)
@[simp]
theorem
category_theory.biprod.unipotent_upper_inv
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{X₁ X₂ : C}
(r : X₁ ⟶ X₂) :
(category_theory.biprod.unipotent_upper r).inv = category_theory.biprod.of_components (𝟙 X₁) (-r) 0 (𝟙 X₂)
@[simp]
theorem
category_theory.biprod.unipotent_lower_inv
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{X₁ X₂ : C}
(r : X₂ ⟶ X₁) :
(category_theory.biprod.unipotent_lower r).inv = category_theory.biprod.of_components (𝟙 X₁) 0 (-r) (𝟙 X₂)
@[simp]
theorem
category_theory.biprod.unipotent_lower_hom
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{X₁ X₂ : C}
(r : X₂ ⟶ X₁) :
(category_theory.biprod.unipotent_lower r).hom = category_theory.biprod.of_components (𝟙 X₁) 0 r (𝟙 X₂)
noncomputable
def
category_theory.biprod.unipotent_lower
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{X₁ X₂ : C}
(r : X₂ ⟶ X₁) :
The unipotent lower triangular matrix
(1 0)
(r 1)
as an isomorphism.
Equations
- category_theory.biprod.unipotent_lower r = {hom := category_theory.biprod.of_components (𝟙 X₁) 0 r (𝟙 X₂), inv := category_theory.biprod.of_components (𝟙 X₁) 0 (-r) (𝟙 X₂), hom_inv_id' := _, inv_hom_id' := _}
noncomputable
def
category_theory.biprod.gaussian'
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{X₁ X₂ Y₁ Y₂ : C}
(f₁₁ : X₁ ⟶ Y₁)
(f₁₂ : X₁ ⟶ Y₂)
(f₂₁ : X₂ ⟶ Y₁)
(f₂₂ : X₂ ⟶ Y₂)
[category_theory.is_iso f₁₁] :
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
- category_theory.biprod.gaussian' f₁₁ f₁₂ f₂₁ f₂₂ = ⟨category_theory.biprod.unipotent_lower (-f₂₁ ≫ category_theory.inv f₁₁), ⟨category_theory.biprod.unipotent_upper (-category_theory.inv f₁₁ ≫ f₁₂), ⟨f₂₂ - f₂₁ ≫ category_theory.inv f₁₁ ≫ f₁₂, _⟩⟩⟩
noncomputable
def
category_theory.biprod.gaussian
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{X₁ X₂ Y₁ Y₂ : C}
(f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂)
[category_theory.is_iso (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.fst)] :
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
- category_theory.biprod.gaussian f = let this : Σ' (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) (g₂₂ : X₂ ⟶ Y₂), L.hom ≫ category_theory.biprod.of_components (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.snd) (category_theory.limits.biprod.inr ≫ f ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inr ≫ f ≫ category_theory.limits.biprod.snd) ≫ R.hom = category_theory.limits.biprod.map (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.fst) g₂₂ := category_theory.biprod.gaussian' (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.snd) (category_theory.limits.biprod.inr ≫ f ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inr ≫ f ≫ category_theory.limits.biprod.snd) in _.mpr (_.mp this)
noncomputable
def
category_theory.biprod.iso_elim'
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{X₁ X₂ Y₁ Y₂ : C}
(f₁₁ : X₁ ⟶ Y₁)
(f₁₂ : X₁ ⟶ Y₂)
(f₂₁ : X₂ ⟶ Y₁)
(f₂₂ : X₂ ⟶ Y₂)
[category_theory.is_iso f₁₁]
[category_theory.is_iso (category_theory.biprod.of_components 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
- category_theory.biprod.iso_elim' f₁₁ f₁₂ f₂₁ f₂₂ = (category_theory.biprod.gaussian' f₁₁ f₁₂ f₂₁ f₂₂).cases_on (λ (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) (snd : Σ' (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) (g₂₂ : X₂ ⟶ Y₂), L.hom ≫ category_theory.biprod.of_components f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom = category_theory.limits.biprod.map f₁₁ g₂₂), snd.cases_on (λ (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) (snd_snd : Σ' (g₂₂ : X₂ ⟶ Y₂), L.hom ≫ category_theory.biprod.of_components f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom = category_theory.limits.biprod.map f₁₁ g₂₂), snd_snd.cases_on (λ (g : X₂ ⟶ Y₂) (w : L.hom ≫ category_theory.biprod.of_components f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom = category_theory.limits.biprod.map f₁₁ g), let _inst : category_theory.is_iso (category_theory.limits.biprod.map f₁₁ g) := _, _inst_6 : category_theory.is_iso g := _ in category_theory.as_iso g)))
noncomputable
def
category_theory.biprod.iso_elim
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{X₁ X₂ Y₁ Y₂ : C}
(f : X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂)
[category_theory.is_iso (category_theory.limits.biprod.inl ≫ f.hom ≫ category_theory.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
- category_theory.biprod.iso_elim f = let _inst : category_theory.is_iso (category_theory.biprod.of_components (category_theory.limits.biprod.inl ≫ f.hom ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inl ≫ f.hom ≫ category_theory.limits.biprod.snd) (category_theory.limits.biprod.inr ≫ f.hom ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inr ≫ f.hom ≫ category_theory.limits.biprod.snd)) := _ in category_theory.biprod.iso_elim' (category_theory.limits.biprod.inl ≫ f.hom ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inl ≫ f.hom ≫ category_theory.limits.biprod.snd) (category_theory.limits.biprod.inr ≫ f.hom ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inr ≫ f.hom ≫ category_theory.limits.biprod.snd)
theorem
category_theory.biprod.column_nonzero_of_iso
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{W X Y Z : C}
(f : W ⊞ X ⟶ Y ⊞ Z)
[category_theory.is_iso f] :
theorem
category_theory.biproduct.column_nonzero_of_iso'
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{σ τ : Type}
[finite τ]
{S : σ → C}
[category_theory.limits.has_biproduct S]
{T : τ → C}
[category_theory.limits.has_biproduct T]
(s : σ)
(f : ⨁ S ⟶ ⨁ T)
[category_theory.is_iso f] :
(∀ (t : τ), category_theory.limits.biproduct.ι S s ≫ f ≫ category_theory.limits.biproduct.π T t = 0) → 𝟙 (S s) = 0
noncomputable
def
category_theory.biproduct.column_nonzero_of_iso
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{σ τ : Type}
[fintype τ]
{S : σ → C}
[category_theory.limits.has_biproduct S]
{T : τ → C}
[category_theory.limits.has_biproduct T]
(s : σ)
(nz : 𝟙 (S s) ≠ 0)
(f : ⨁ S ⟶ ⨁ T)
[category_theory.is_iso f] :
trunc (Σ' (t : τ), category_theory.limits.biproduct.ι S s ≫ f ≫ category_theory.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
noncomputable
def
category_theory.limits.preserves_product_of_preserves_biproduct
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u'}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type}
[fintype J]
{f : J → C}
[category_theory.limits.preserves_biproduct f F] :
A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite products.
Equations
- category_theory.limits.preserves_product_of_preserves_biproduct F = {preserves := λ (c : category_theory.limits.cone (category_theory.discrete.functor f)) (hc : category_theory.limits.is_limit c), (⇑((category_theory.limits.is_limit.postcompose_inv_equiv (category_theory.discrete.comp_nat_iso_discrete f F) (F.map_bicone (category_theory.limits.bicone.of_limit_cone hc)).to_cone).symm) (category_theory.limits.is_bilimit_of_preserves F (category_theory.limits.bicone_is_bilimit_of_limit_cone_of_is_limit hc)).is_limit).of_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose (category_theory.discrete.comp_nat_iso_discrete f F).inv).obj (F.map_bicone (category_theory.limits.bicone.of_limit_cone hc)).to_cone).X) _)}
noncomputable
def
category_theory.limits.preserves_products_of_shape_of_preserves_biproducts_of_shape
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u'}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type}
[fintype J]
[category_theory.limits.preserves_biproducts_of_shape J F] :
A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite products.
def
category_theory.limits.preserves_biproduct_of_preserves_product
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u'}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type}
[fintype J]
{f : J → C}
[category_theory.limits.preserves_limit (category_theory.discrete.functor f) F] :
A functor between preadditive categories that preserves (zero morphisms and) finite products preserves finite biproducts.
Equations
- category_theory.limits.preserves_biproduct_of_preserves_product F = {preserves := λ (b : category_theory.limits.bicone f) (hb : b.is_bilimit), category_theory.limits.is_bilimit_of_is_limit (F.map_bicone b) ((⇑((category_theory.limits.is_limit.postcompose_hom_equiv (category_theory.discrete.comp_nat_iso_discrete f F) (F.map_cone b.to_cone)).symm) (category_theory.limits.is_limit_of_preserves F hb.is_limit)).of_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose (category_theory.discrete.comp_nat_iso_discrete f F).hom).obj (F.map_cone b.to_cone)).X) _))}
noncomputable
def
category_theory.limits.preserves_biproduct_of_mono_biproduct_comparison
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u'}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type}
[fintype J]
{f : J → C}
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (F.obj ∘ f)]
[category_theory.mono (F.biproduct_comparison 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 map_biproduct.
noncomputable
def
category_theory.limits.preserves_biproduct_of_epi_biproduct_comparison'
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u'}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type}
[fintype J]
{f : J → C}
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (F.obj ∘ f)]
[category_theory.epi (F.biproduct_comparison' 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 map_biproduct.
def
category_theory.limits.preserves_biproducts_of_shape_of_preserves_products_of_shape
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u'}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type}
[fintype J]
[category_theory.limits.preserves_limits_of_shape (category_theory.discrete J) F] :
A functor between preadditive categories that preserves (zero morphisms and) finite products preserves finite biproducts.
noncomputable
def
category_theory.limits.preserves_coproduct_of_preserves_biproduct
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u'}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type}
[fintype J]
{f : J → C}
[category_theory.limits.preserves_biproduct f F] :
A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite coproducts.
Equations
- category_theory.limits.preserves_coproduct_of_preserves_biproduct F = {preserves := λ (c : category_theory.limits.cocone (category_theory.discrete.functor f)) (hc : category_theory.limits.is_colimit c), (⇑((category_theory.limits.is_colimit.precompose_hom_equiv (category_theory.discrete.comp_nat_iso_discrete f F) (F.map_bicone (category_theory.limits.bicone.of_colimit_cocone hc)).to_cocone).symm) (category_theory.limits.is_bilimit_of_preserves F (category_theory.limits.bicone_is_bilimit_of_colimit_cocone_of_is_colimit hc)).is_colimit).of_iso_colimit (category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.limits.cocones.precompose (category_theory.discrete.comp_nat_iso_discrete f F).hom).obj (F.map_bicone (category_theory.limits.bicone.of_colimit_cocone hc)).to_cocone).X) _)}
noncomputable
def
category_theory.limits.preserves_coproducts_of_shape_of_preserves_biproducts_of_shape
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u'}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type}
[fintype J]
[category_theory.limits.preserves_biproducts_of_shape J F] :
A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite coproducts.
def
category_theory.limits.preserves_biproduct_of_preserves_coproduct
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u'}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type}
[fintype J]
{f : J → C}
[category_theory.limits.preserves_colimit (category_theory.discrete.functor f) F] :
A functor between preadditive categories that preserves (zero morphisms and) finite coproducts preserves finite biproducts.
Equations
- category_theory.limits.preserves_biproduct_of_preserves_coproduct F = {preserves := λ (b : category_theory.limits.bicone f) (hb : b.is_bilimit), category_theory.limits.is_bilimit_of_is_colimit (F.map_bicone b) ((⇑((category_theory.limits.is_colimit.precompose_inv_equiv (category_theory.discrete.comp_nat_iso_discrete f F) (F.map_cocone b.to_cocone)).symm) (category_theory.limits.is_colimit_of_preserves F hb.is_colimit)).of_iso_colimit (category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.limits.cocones.precompose (category_theory.discrete.comp_nat_iso_discrete f F).inv).obj (F.map_cocone b.to_cocone)).X) _))}
def
category_theory.limits.preserves_biproducts_of_shape_of_preserves_coproducts_of_shape
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u'}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type}
[fintype J]
[category_theory.limits.preserves_colimits_of_shape (category_theory.discrete J) F] :
A functor between preadditive categories that preserves (zero morphisms and) finite coproducts preserves finite biproducts.
def
category_theory.limits.preserves_binary_product_of_preserves_binary_biproduct
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u'}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{X Y : C}
[category_theory.limits.preserves_binary_biproduct X Y F] :
A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary products.
Equations
- category_theory.limits.preserves_binary_product_of_preserves_binary_biproduct F = {preserves := λ (c : category_theory.limits.cone (category_theory.limits.pair X Y)) (hc : category_theory.limits.is_limit c), (⇑((category_theory.limits.is_limit.postcompose_inv_equiv (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)) (F.map_binary_bicone (category_theory.limits.binary_bicone.of_limit_cone hc)).to_cone).symm) (category_theory.limits.is_binary_bilimit_of_preserves F (category_theory.limits.binary_bicone_is_bilimit_of_limit_cone_of_is_limit hc)).is_limit).of_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)).inv).obj (F.map_binary_bicone (category_theory.limits.binary_bicone.of_limit_cone hc)).to_cone).X) _)}
def
category_theory.limits.preserves_binary_products_of_preserves_binary_biproducts
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u'}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
[category_theory.limits.preserves_binary_biproducts F] :
A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary products.
def
category_theory.limits.preserves_binary_biproduct_of_preserves_binary_product
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u'}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{X Y : C}
[category_theory.limits.preserves_limit (category_theory.limits.pair X Y) F] :
A functor between preadditive categories that preserves (zero morphisms and) binary products preserves binary biproducts.
Equations
- category_theory.limits.preserves_binary_biproduct_of_preserves_binary_product F = {preserves := λ (b : category_theory.limits.binary_bicone X Y) (hb : b.is_bilimit), category_theory.limits.is_binary_bilimit_of_is_limit (F.map_binary_bicone b) ((⇑((category_theory.limits.is_limit.postcompose_hom_equiv (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)) (F.map_cone b.to_cone)).symm) (category_theory.limits.is_limit_of_preserves F hb.is_limit)).of_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)).hom).obj (F.map_cone b.to_cone)).X) _))}
noncomputable
def
category_theory.limits.preserves_binary_biproduct_of_mono_biprod_comparison
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u'}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.has_binary_biproduct (F.obj X) (F.obj Y)]
[category_theory.mono (F.biprod_comparison 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.
noncomputable
def
category_theory.limits.preserves_binary_biproduct_of_epi_biprod_comparison'
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u'}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.has_binary_biproduct (F.obj X) (F.obj Y)]
[category_theory.epi (F.biprod_comparison' 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 map_biprod.
def
category_theory.limits.preserves_binary_biproducts_of_preserves_binary_products
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u'}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
[category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F] :
A functor between preadditive categories that preserves (zero morphisms and) binary products preserves binary biproducts.
def
category_theory.limits.preserves_binary_coproduct_of_preserves_binary_biproduct
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u'}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{X Y : C}
[category_theory.limits.preserves_binary_biproduct X Y F] :
A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary coproducts.
Equations
- category_theory.limits.preserves_binary_coproduct_of_preserves_binary_biproduct F = {preserves := λ (c : category_theory.limits.cocone (category_theory.limits.pair X Y)) (hc : category_theory.limits.is_colimit c), (⇑((category_theory.limits.is_colimit.precompose_hom_equiv (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)) (F.map_binary_bicone (category_theory.limits.binary_bicone.of_colimit_cocone hc)).to_cocone).symm) (category_theory.limits.is_binary_bilimit_of_preserves F (category_theory.limits.binary_bicone_is_bilimit_of_colimit_cocone_of_is_colimit hc)).is_colimit).of_iso_colimit (category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.limits.cocones.precompose (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)).hom).obj (F.map_binary_bicone (category_theory.limits.binary_bicone.of_colimit_cocone hc)).to_cocone).X) _)}
def
category_theory.limits.preserves_binary_coproducts_of_preserves_binary_biproducts
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u'}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
[category_theory.limits.preserves_binary_biproducts F] :
A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary coproducts.
def
category_theory.limits.preserves_binary_biproduct_of_preserves_binary_coproduct
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u'}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{X Y : C}
[category_theory.limits.preserves_colimit (category_theory.limits.pair X Y) F] :
A functor between preadditive categories that preserves (zero morphisms and) binary coproducts preserves binary biproducts.
Equations
- category_theory.limits.preserves_binary_biproduct_of_preserves_binary_coproduct F = {preserves := λ (b : category_theory.limits.binary_bicone X Y) (hb : b.is_bilimit), category_theory.limits.is_binary_bilimit_of_is_colimit (F.map_binary_bicone b) ((⇑((category_theory.limits.is_colimit.precompose_inv_equiv (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)) (F.map_cocone b.to_cocone)).symm) (category_theory.limits.is_colimit_of_preserves F hb.is_colimit)).of_iso_colimit (category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.limits.cocones.precompose (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)).inv).obj (F.map_cocone b.to_cocone)).X) _))}
def
category_theory.limits.preserves_binary_biproducts_of_preserves_binary_coproducts
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u'}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
[category_theory.limits.preserves_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F] :
A functor between preadditive categories that preserves (zero morphisms and) binary coproducts preserves binary biproducts.