Binary biproducts of homological complexes
In this file, it is shown that if two homological complex K and L in
a preadditive category are such that for all i : ι, the binary biproduct
K.X i ⊞ L.X i exists, then K ⊞ L exists, and there is an isomorphism
biprodXIso K L i : (K ⊞ L).X i ≅ (K.X i) ⊞ (L.X i).
instance
HomologicalComplex.instHasBinaryBiproductObjEval
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
:
CategoryTheory.Limits.HasBinaryBiproduct ((HomologicalComplex.eval C c i).obj K) ((HomologicalComplex.eval C c i).obj L)
instance
HomologicalComplex.instHasLimitDiscreteWalkingPairCompPairEval
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
:
CategoryTheory.Limits.HasLimit ((CategoryTheory.Limits.pair K L).comp (HomologicalComplex.eval C c i))
instance
HomologicalComplex.instHasColimitDiscreteWalkingPairCompPairEval
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
:
CategoryTheory.Limits.HasColimit ((CategoryTheory.Limits.pair K L).comp (HomologicalComplex.eval C c i))
instance
HomologicalComplex.instHasBinaryBiproduct
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
:
instance
HomologicalComplex.instPreservesBinaryBiproductEval
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
:
noncomputable def
HomologicalComplex.biprodXIso
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
:
The canonical isomorphism (K ⊞ L).X i ≅ (K.X i) ⊞ (L.X i).
Equations
- K.biprodXIso L i = (HomologicalComplex.eval C c i).mapBiprod K L
Instances For
@[simp]
theorem
HomologicalComplex.inl_biprodXIso_inv
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (K.biprodXIso L i).inv = CategoryTheory.Limits.biprod.inl.f i
@[simp]
theorem
HomologicalComplex.inl_biprodXIso_inv_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
{Z : C}
(h : (K ⊞ L).X i ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.inr_biprodXIso_inv
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (K.biprodXIso L i).inv = CategoryTheory.Limits.biprod.inr.f i
@[simp]
theorem
HomologicalComplex.inr_biprodXIso_inv_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
{Z : C}
(h : (K ⊞ L).X i ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.biprodXIso_hom_fst
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
:
CategoryTheory.CategoryStruct.comp (K.biprodXIso L i).hom CategoryTheory.Limits.biprod.fst = CategoryTheory.Limits.biprod.fst.f i
@[simp]
theorem
HomologicalComplex.biprodXIso_hom_fst_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
{Z : C}
(h : K.X i ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.biprodXIso_hom_snd
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
:
CategoryTheory.CategoryStruct.comp (K.biprodXIso L i).hom CategoryTheory.Limits.biprod.snd = CategoryTheory.Limits.biprod.snd.f i
@[simp]
theorem
HomologicalComplex.biprodXIso_hom_snd_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
{Z : C}
(h : L.X i ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.biprod_inl_fst_f
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
:
@[simp]
theorem
HomologicalComplex.biprod_inl_fst_f_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
{Z : C}
(h : K.X i ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.biprod_inl_snd_f
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
:
@[simp]
theorem
HomologicalComplex.biprod_inl_snd_f_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
{Z : C}
(h : L.X i ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.biprod_inr_fst_f
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
:
@[simp]
theorem
HomologicalComplex.biprod_inr_fst_f_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
{Z : C}
(h : K.X i ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.biprod_inr_snd_f
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
:
@[simp]
theorem
HomologicalComplex.biprod_inr_snd_f_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
{Z : C}
(h : L.X i ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.biprod_inl_desc_f
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
{M : HomologicalComplex C c}
(α : K ⟶ M)
(β : L ⟶ M)
(i : ι)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i)
((CategoryTheory.Limits.biprod.desc α β).f i) = α.f i
@[simp]
theorem
HomologicalComplex.biprod_inl_desc_f_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
{M : HomologicalComplex C c}
(α : K ⟶ M)
(β : L ⟶ M)
(i : ι)
{Z : C}
(h : M.X i ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.biprod_inr_desc_f
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
{M : HomologicalComplex C c}
(α : K ⟶ M)
(β : L ⟶ M)
(i : ι)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i)
((CategoryTheory.Limits.biprod.desc α β).f i) = β.f i
@[simp]
theorem
HomologicalComplex.biprod_inr_desc_f_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
{M : HomologicalComplex C c}
(α : K ⟶ M)
(β : L ⟶ M)
(i : ι)
{Z : C}
(h : M.X i ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.biprod_lift_fst_f
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
{M : HomologicalComplex C c}
(α : M ⟶ K)
(β : M ⟶ L)
(i : ι)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.biprod.lift α β).f i)
(CategoryTheory.Limits.biprod.fst.f i) = α.f i
@[simp]
theorem
HomologicalComplex.biprod_lift_fst_f_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
{M : HomologicalComplex C c}
(α : M ⟶ K)
(β : M ⟶ L)
(i : ι)
{Z : C}
(h : K.X i ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.biprod_lift_snd_f
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
{M : HomologicalComplex C c}
(α : M ⟶ K)
(β : M ⟶ L)
(i : ι)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.biprod.lift α β).f i)
(CategoryTheory.Limits.biprod.snd.f i) = β.f i
@[simp]
theorem
HomologicalComplex.biprod_lift_snd_f_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
{M : HomologicalComplex C c}
(α : M ⟶ K)
(β : M ⟶ L)
(i : ι)
{Z : C}
(h : L.X i ⟶ Z)
: