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) :