Documentation

Mathlib.Algebra.Homology.HomologicalComplexBiprod

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

source
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)
Equations
  • ⋯ = ⋯
source
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))
Equations
  • ⋯ = ⋯
source
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))
Equations
  • ⋯ = ⋯
source
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)] :
CategoryTheory.Limits.HasBinaryBiproduct K L
Equations
  • ⋯ = ⋯
source
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 : ι) :
CategoryTheory.Limits.PreservesBinaryBiproduct K L (HomologicalComplex.eval C c i)
Equations
  • ⋯ = ⋯
source
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 : ι) :
(K ⊞ L).X i ≅ K.X i ⊞ L.X i

The canonical isomorphism (K ⊞ L).X i ≅ (K.X i) ⊞ (L.X i).

Equations
Instances For
    source
    @[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
    source
    @[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) :
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp (K.biprodXIso L i).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) h
    source
    @[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
    source
    @[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) :
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (K.biprodXIso L i).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) h
    source
    @[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
    source
    @[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) :
    CategoryTheory.CategoryStruct.comp (K.biprodXIso L i).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.fst.f i) h
    source
    @[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
    source
    @[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) :
    CategoryTheory.CategoryStruct.comp (K.biprodXIso L i).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.snd.f i) h
    source
    @[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 : ι) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) (CategoryTheory.Limits.biprod.fst.f i) = CategoryTheory.CategoryStruct.id (K.X i)
    source
    @[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) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.fst.f i) h) = h
    source
    @[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 : ι) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) (CategoryTheory.Limits.biprod.snd.f i) = 0
    source
    @[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) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.snd.f i) h) = CategoryTheory.CategoryStruct.comp 0 h
    source
    @[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 : ι) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) (CategoryTheory.Limits.biprod.fst.f i) = 0
    source
    @[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) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.fst.f i) h) = CategoryTheory.CategoryStruct.comp 0 h
    source
    @[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 : ι) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) (CategoryTheory.Limits.biprod.snd.f i) = CategoryTheory.CategoryStruct.id (L.X i)
    source
    @[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) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.snd.f i) h) = h
    source
    @[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
    source
    @[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) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.biprod.desc α β).f i) h) = CategoryTheory.CategoryStruct.comp (α.f i) h
    source
    @[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
    source
    @[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) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.biprod.desc α β).f i) h) = CategoryTheory.CategoryStruct.comp (β.f i) h
    source
    @[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
    source
    @[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) :
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.biprod.lift α β).f i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.fst.f i) h) = CategoryTheory.CategoryStruct.comp (α.f i) h
    source
    @[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
    source
    @[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) :
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.biprod.lift α β).f i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.snd.f i) h) = CategoryTheory.CategoryStruct.comp (β.f i) h