Homology of a biproduct of homological complexes

Homology commutes with binary biproducts: Hᵢ(A ⊞ B) ≅ Hᵢ(A) ⊞ Hᵢ(B) (HomologicalComplex.homologyBiprodIso). Hence a biproduct A ⊞ B of homological complexes is exact in a degree, or acyclic, exactly when both of its summands are, and the maps induced on homology by morphisms into and out of A ⊞ B can be read off from their components.

Main results

• HomologicalComplex.exactAt_biprod_iff, HomologicalComplex.acyclic_biprod_iff: A ⊞ B is exact in a degree, or acyclic, if and only if A and B both are.
• HomologicalComplex.mono_biprod_lift_homologyMap_iff, HomologicalComplex.epi_biprod_desc_homologyMap_iff: the map Hᵢ(X) ⟶ Hᵢ(A) ⊞ Hᵢ(B) induced by (f₁, f₂) is mono, and the map Hᵢ(A) ⊞ Hᵢ(B) ⟶ Hᵢ(Z) induced by g₁ + g₂ is epi, exactly when the map induced on Hᵢ(A ⊞ B) is.

@[simp]

theorem HomologicalComplex.exactAt_biprod_iff {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.CategoryWithHomology C] {c : ComplexShape ι} (A B : HomologicalComplex C c) (i : ι) : (A ⊞ B).ExactAt i ↔ A.ExactAt i ∧ B.ExactAt i

The binary biproduct A ⊞ B is exact in degree i if and only if A and B both are.

@[simp]

theorem HomologicalComplex.acyclic_biprod_iff {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.CategoryWithHomology C] {c : ComplexShape ι} (A B : HomologicalComplex C c) : (A ⊞ B).Acyclic ↔ A.Acyclic ∧ B.Acyclic

The binary biproduct A ⊞ B is acyclic if and only if A and B both are.

@[reducible, inline]

noncomputable abbrev HomologicalComplex.homologyBiprodIso {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.CategoryWithHomology C] {c : ComplexShape ι} (A B : HomologicalComplex C c) (i : ι) : (A ⊞ B).homology i ≅ A.homology i ⊞ B.homology i

Homology commutes with the binary biproduct A ⊞ B.

theorem HomologicalComplex.biprod_lift_homologyMap_comp_desc_homologyMap {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.CategoryWithHomology C] {c : ComplexShape ι} {A B X Z : HomologicalComplex C c} {f₁ : X ⟶ A} {f₂ : X ⟶ B} {g₁ : A ⟶ Z} {g₂ : B ⟶ Z} (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift f₁ f₂) (CategoryTheory.Limits.biprod.desc g₁ g₂) = 0) (i : ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift (homologyMap f₁ i) (homologyMap f₂ i)) (CategoryTheory.Limits.biprod.desc (homologyMap g₁ i) (homologyMap g₂ i)) = 0

The maps induced on homology by the components of X ⟶ A ⊞ B ⟶ Z compose to zero.

theorem HomologicalComplex.biprod_lift_homologyMap_comp_desc_homologyMap_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.CategoryWithHomology C] {c : ComplexShape ι} {A B X Z : HomologicalComplex C c} {f₁ : X ⟶ A} {f₂ : X ⟶ B} {g₁ : A ⟶ Z} {g₂ : B ⟶ Z} (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift f₁ f₂) (CategoryTheory.Limits.biprod.desc g₁ g₂) = 0) (i : ι) {Z✝ : C} (h : Z.homology i ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift (homologyMap f₁ i) (homologyMap f₂ i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.desc (homologyMap g₁ i) (homologyMap g₂ i)) h) = CategoryTheory.CategoryStruct.comp 0 h

The maps induced on homology by the components of X ⟶ A ⊞ B ⟶ Z compose to zero.

theorem HomologicalComplex.homologyMap_biprod_lift_comp_homologyBiprodIso_hom {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.CategoryWithHomology C] {c : ComplexShape ι} {A B X : HomologicalComplex C c} {f₁ : X ⟶ A} {f₂ : X ⟶ B} (i : ι) : CategoryTheory.CategoryStruct.comp (homologyMap (CategoryTheory.Limits.biprod.lift f₁ f₂) i) (A.homologyBiprodIso B i).hom = CategoryTheory.Limits.biprod.lift (homologyMap f₁ i) (homologyMap f₂ i)

Under Hᵢ(A ⊞ B) ≅ Hᵢ(A) ⊞ Hᵢ(B), the map induced by biprod.lift f₁ f₂ becomes the lift of the maps induced by f₁ and f₂.

theorem HomologicalComplex.homologyBiprodIso_hom_comp_biprod_desc_homologyMap {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.CategoryWithHomology C] {c : ComplexShape ι} {A B Z : HomologicalComplex C c} {g₁ : A ⟶ Z} {g₂ : B ⟶ Z} (i : ι) : CategoryTheory.CategoryStruct.comp (A.homologyBiprodIso B i).hom (CategoryTheory.Limits.biprod.desc (homologyMap g₁ i) (homologyMap g₂ i)) = homologyMap (CategoryTheory.Limits.biprod.desc g₁ g₂) i

Under Hᵢ(A ⊞ B) ≅ Hᵢ(A) ⊞ Hᵢ(B), the map induced by biprod.desc g₁ g₂ becomes the descent of the maps induced by g₁ and g₂.

theorem HomologicalComplex.homologyBiprodIso_hom_comp_biprod_desc_homologyMap_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.CategoryWithHomology C] {c : ComplexShape ι} {A B Z : HomologicalComplex C c} {g₁ : A ⟶ Z} {g₂ : B ⟶ Z} (i : ι) {Z✝ : C} (h : Z.homology i ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (A.homologyBiprodIso B i).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.desc (homologyMap g₁ i) (homologyMap g₂ i)) h) = CategoryTheory.CategoryStruct.comp (homologyMap (CategoryTheory.Limits.biprod.desc g₁ g₂) i) h

Under Hᵢ(A ⊞ B) ≅ Hᵢ(A) ⊞ Hᵢ(B), the map induced by biprod.desc g₁ g₂ becomes the descent of the maps induced by g₁ and g₂.

theorem HomologicalComplex.mono_biprod_lift_homologyMap_iff {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.CategoryWithHomology C] {c : ComplexShape ι} {A B X : HomologicalComplex C c} {f₁ : X ⟶ A} {f₂ : X ⟶ B} (i : ι) : CategoryTheory.Mono (CategoryTheory.Limits.biprod.lift (homologyMap f₁ i) (homologyMap f₂ i)) ↔ CategoryTheory.Mono (homologyMap (CategoryTheory.Limits.biprod.lift f₁ f₂) i)

The map Hᵢ(X) ⟶ Hᵢ(A) ⊞ Hᵢ(B) induced by (f₁, f₂) is a monomorphism if and only if the map induced by biprod.lift f₁ f₂ is.

theorem HomologicalComplex.epi_biprod_desc_homologyMap_iff {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.CategoryWithHomology C] {c : ComplexShape ι} {A B Z : HomologicalComplex C c} {g₁ : A ⟶ Z} {g₂ : B ⟶ Z} (i : ι) : CategoryTheory.Epi (CategoryTheory.Limits.biprod.desc (homologyMap g₁ i) (homologyMap g₂ i)) ↔ CategoryTheory.Epi (homologyMap (CategoryTheory.Limits.biprod.desc g₁ g₂) i)

The map Hᵢ(A) ⊞ Hᵢ(B) ⟶ Hᵢ(Z) induced by g₁ + g₂ is an epimorphism if and only if the map induced by biprod.desc g₁ g₂ is.