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.{v_1, 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 ((eval C c i).obj K) ((eval C c i).obj L)
instance
HomologicalComplex.instHasLimitDiscreteWalkingPairCompPairEval
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{v_1, 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 (eval C c i))
instance
HomologicalComplex.instHasColimitDiscreteWalkingPairCompPairEval
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{v_1, 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 (eval C c i))
instance
HomologicalComplex.instHasBinaryBiproduct
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{v_1, 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.{v_1, 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.PreservesBinaryBiproduct K L (eval C c i)
noncomputable def
HomologicalComplex.biprodXIso
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{v_1, 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.{v_1, 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.inl_biprodXIso_inv_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{v_1, 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.{v_1, 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.inr_biprodXIso_inv_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{v_1, 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.{v_1, 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.biprodXIso_hom_fst_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{v_1, 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.{v_1, 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.biprodXIso_hom_snd_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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_total_f
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K L : HomologicalComplex C c)
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
(i : ι)
:
theorem
HomologicalComplex.biprodX_ext_from_iff
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
{A : C}
{i : ι}
{f g : (K ⊞ L).X i ⟶ A}
:
f = g ↔ CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) g ∧ CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) g
theorem
HomologicalComplex.biprodX_ext_from
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
{A : C}
{i : ι}
{f g : (K ⊞ L).X i ⟶ A}
(h₁ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) g)
(h₂ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) g)
:
theorem
HomologicalComplex.biprodX_ext_to_iff
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
{A : C}
{i : ι}
{f g : A ⟶ (K ⊞ L).X i}
:
f = g ↔ CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biprod.fst.f i) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biprod.fst.f i) ∧ CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biprod.snd.f i) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biprod.snd.f i)
theorem
HomologicalComplex.biprodX_ext_to
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)]
{A : C}
{i : ι}
{f g : A ⟶ (K ⊞ L).X i}
(h₁ :
CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biprod.fst.f i) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biprod.fst.f i))
(h₂ :
CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biprod.snd.f i) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biprod.snd.f i))
:
@[simp]
theorem
HomologicalComplex.biprod_inl_desc_f
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{v_1, 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 : ι)
:
@[simp]
theorem
HomologicalComplex.biprod_inl_desc_f_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{v_1, 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.{v_1, 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 : ι)
:
@[simp]
theorem
HomologicalComplex.biprod_inr_desc_f_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{v_1, 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.{v_1, 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 : ι)
:
@[simp]
theorem
HomologicalComplex.biprod_lift_fst_f_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{v_1, 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.{v_1, 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 : ι)
:
@[simp]
theorem
HomologicalComplex.biprod_lift_snd_f_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{v_1, 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)
: