The homology sequence

If 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 is a short exact sequence in a category of complexes HomologicalComplex C c in an abelian category (i.e. S is a short complex in that category and satisfies hS : S.ShortExact), then whenever i and j are degrees such that hij : c.Rel i j, then there is a long exact sequence : ... ⟶ S.X₁.homology i ⟶ S.X₂.homology i ⟶ S.X₃.homology i ⟶ S.X₁.homology j ⟶ .... The connecting homomorphism S.X₃.homology i ⟶ S.X₁.homology j is hS.δ i j hij, and the exactness is asserted as lemmas hS.homology_exact₁, hS.homology_exact₂ and hS.homology_exact₃.

The proof is based on the snake lemma, similarly as it was originally done in the Liquid Tensor Experiment.

References

• https://stacks.math.columbia.edu/tag/0111

noncomputable def HomologicalComplex.opcyclesToCycles {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology K j] : HomologicalComplex.opcycles K i ⟶ HomologicalComplex.cycles K j

The morphism K.opcycles i ⟶ K.cycles j that is induced by K.d i j.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HomologicalComplex.opcyclesToCycles_iCycles_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology K j] {Z : C} (h : K.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesToCycles K i j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles K j) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.fromOpcycles K i j) h

@[simp]

theorem HomologicalComplex.opcyclesToCycles_iCycles {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology K j] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesToCycles K i j) (HomologicalComplex.iCycles K j) = HomologicalComplex.fromOpcycles K i j

theorem HomologicalComplex.pOpcycles_opcyclesToCycles_iCycles_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology K j] {Z : C} (h : K.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles K i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesToCycles K i j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles K j) h)) = CategoryTheory.CategoryStruct.comp (K.d i j) h

theorem HomologicalComplex.pOpcycles_opcyclesToCycles_iCycles {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology K j] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles K i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesToCycles K i j) (HomologicalComplex.iCycles K j)) = K.d i j

@[simp]

theorem HomologicalComplex.pOpcycles_opcyclesToCycles_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology K j] {Z : C} (h : HomologicalComplex.cycles K j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles K i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesToCycles K i j) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.toCycles K i j) h

@[simp]

theorem HomologicalComplex.pOpcycles_opcyclesToCycles {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology K j] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles K i) (HomologicalComplex.opcyclesToCycles K i j) = HomologicalComplex.toCycles K i j

@[simp]

theorem HomologicalComplex.homologyι_opcyclesToCycles_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology K j] {Z : C} (h : HomologicalComplex.cycles K j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyι K i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesToCycles K i j) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem HomologicalComplex.homologyι_opcyclesToCycles {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology K j] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyι K i) (HomologicalComplex.opcyclesToCycles K i j) = 0

@[simp]

theorem HomologicalComplex.opcyclesToCycles_homologyπ_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology K j] {Z : C} (h : HomologicalComplex.homology K j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesToCycles K i j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ K j) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem HomologicalComplex.opcyclesToCycles_homologyπ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology K j] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesToCycles K i j) (HomologicalComplex.homologyπ K j) = 0

@[simp]

theorem HomologicalComplex.opcyclesToCycles_naturality_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) (j : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology K j] [HomologicalComplex.HasHomology L i] [HomologicalComplex.HasHomology L j] {Z : C} (h : HomologicalComplex.cycles L j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesToCycles L i j) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesToCycles K i j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ j) h)

@[simp]

theorem HomologicalComplex.opcyclesToCycles_naturality {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) (j : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology K j] [HomologicalComplex.HasHomology L i] [HomologicalComplex.HasHomology L j] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i) (HomologicalComplex.opcyclesToCycles L i j) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesToCycles K i j) (HomologicalComplex.cyclesMap φ j)

@[simp]

theorem HomologicalComplex.natTransOpCyclesToCycles_app (C : Type u_1) {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (c : ComplexShape ι) (i : ι) (j : ι) [CategoryTheory.CategoryWithHomology C] (K : HomologicalComplex C c) : (HomologicalComplex.natTransOpCyclesToCycles C c i j).app K = HomologicalComplex.opcyclesToCycles K i j

noncomputable def HomologicalComplex.natTransOpCyclesToCycles (C : Type u_1) {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (c : ComplexShape ι) (i : ι) (j : ι) [CategoryTheory.CategoryWithHomology C] : HomologicalComplex.opcyclesFunctor C c i ⟶ HomologicalComplex.cyclesFunctor C c j

The natural transformation K.opcyclesToCycles i j : K.opcycles i ⟶ K.cycles j for all K : HomologicalComplex C c.

Equations

• HomologicalComplex.natTransOpCyclesToCycles C c i j = CategoryTheory.NatTrans.mk fun (K : HomologicalComplex C c) => HomologicalComplex.opcyclesToCycles K i j

noncomputable def HomologicalComplex.HomologySequence.composableArrows₃ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology K j] : CategoryTheory.ComposableArrows C 3

The diagram K.homology i ⟶ K.opcycles i ⟶ K.cycles j ⟶ K.homology j.

Equations

• One or more equations did not get rendered due to their size.

instance HomologicalComplex.HomologySequence.instMonoObjFinHAddNatInstHAddInstAddNatOfNatInstOfNatNatToQuiverToCategoryStructSmallCategoryToPreorderInstPartialOrderFinToQuiverToCategoryStructToPrefunctorComposableArrows₃MkByContradictionLtInstLTNatDecLtNotNot_sat'_of_isImpossibleMkSomeIntOfNatOf_decide_eq_trueEqBoolIsImpossibleTrueInstDecidableEqBoolIdDecideReflConsNegSuccNilOfListCastInstNatCastIntCombine_sat'NoneTidy_satCombo_sat'AddInequality_satLe_of_le_of_eqInstOfNatHSubInstHSubInstSubIntEvalLinearComboInstSubLinearComboMkInstLEIntSub_nonneg_of_leOfNat_le_of_leTransCoordinateSub_congrSymmCoordinate_eval_0Coordinate_eval_1Sub_evalCoordinate_eval_2Le_of_not_ltInstAddLinearComboInstAddIntOfNat_addAdd_congrNatCast_ofNatAdd_evalMap' {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology K j] : CategoryTheory.Mono (CategoryTheory.ComposableArrows.map' (HomologicalComplex.HomologySequence.composableArrows₃ K i j) 0 1)

Equations

• One or more equations did not get rendered due to their size.

instance HomologicalComplex.HomologySequence.instEpiObjFinHAddNatInstHAddInstAddNatOfNatInstOfNatNatToQuiverToCategoryStructSmallCategoryToPreorderInstPartialOrderFinToQuiverToCategoryStructToPrefunctorComposableArrows₃MkByContradictionLtInstLTNatDecLtNotNot_sat'_of_isImpossibleMkSomeIntOfNatOf_decide_eq_trueEqBoolIsImpossibleTrueInstDecidableEqBoolIdDecideReflConsNegSuccNilOfListCastInstNatCastIntCombine_sat'NoneTidy_satCombo_sat'AddInequality_satLe_of_le_of_eqInstOfNatHSubInstHSubInstSubIntEvalLinearComboInstSubLinearComboMkInstLEIntSub_nonneg_of_leOfNat_le_of_leTransCoordinateSub_congrSymmCoordinate_eval_0Coordinate_eval_1Sub_evalCoordinate_eval_2Le_of_not_ltInstAddLinearComboInstAddIntOfNat_addAdd_congrNatCast_ofNatAdd_evalMap' {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology K j] : CategoryTheory.Epi (CategoryTheory.ComposableArrows.map' (HomologicalComplex.HomologySequence.composableArrows₃ K i j) 2 3)

Equations

• One or more equations did not get rendered due to their size.

theorem HomologicalComplex.HomologySequence.composableArrows₃_exact {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hij : c.Rel i j) [CategoryTheory.CategoryWithHomology C] : CategoryTheory.ComposableArrows.Exact (HomologicalComplex.HomologySequence.composableArrows₃ K i j)

The diagram K.homology i ⟶ K.opcycles i ⟶ K.cycles j ⟶ K.homology j is exact when c.Rel i j.

@[simp]

theorem HomologicalComplex.HomologySequence.composableArrows₃Functor_obj (C : Type u_1) {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (i : ι) (j : ι) [CategoryTheory.CategoryWithHomology C] (K : HomologicalComplex C c) : (HomologicalComplex.HomologySequence.composableArrows₃Functor C i j).toPrefunctor.obj K = HomologicalComplex.HomologySequence.composableArrows₃ K i j

@[simp]

theorem HomologicalComplex.HomologySequence.composableArrows₃Functor_map (C : Type u_1) {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (i : ι) (j : ι) [CategoryTheory.CategoryWithHomology C] {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K ⟶ L) : (HomologicalComplex.HomologySequence.composableArrows₃Functor C i j).toPrefunctor.map φ = CategoryTheory.ComposableArrows.homMk₃ (HomologicalComplex.homologyMap φ i) (HomologicalComplex.opcyclesMap φ i) (HomologicalComplex.cyclesMap φ j) (HomologicalComplex.homologyMap φ j) (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyι K i) (HomologicalComplex.opcyclesMap φ i) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ i) (HomologicalComplex.homologyι L i)) (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesToCycles K i j) (HomologicalComplex.cyclesMap φ j) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i) (HomologicalComplex.opcyclesToCycles L i j)) (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ K j) (HomologicalComplex.homologyMap φ j) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ j) (HomologicalComplex.homologyπ L j))

noncomputable def HomologicalComplex.HomologySequence.composableArrows₃Functor (C : Type u_1) {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (i : ι) (j : ι) [CategoryTheory.CategoryWithHomology C] : CategoryTheory.Functor (HomologicalComplex C c) (CategoryTheory.ComposableArrows C 3)

The functor HomologicalComplex C c ⥤ ComposableArrows C 3 that maps K to the diagram K.homology i ⟶ K.opcycles i ⟶ K.cycles j ⟶ K.homology j.

Equations

• One or more equations did not get rendered due to their size.

theorem HomologicalComplex.opcycles_right_exact {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} (S : CategoryTheory.ShortComplex (HomologicalComplex C c)) (hS : CategoryTheory.ShortComplex.Exact S) [CategoryTheory.Epi S.g] (i : ι) [HomologicalComplex.HasHomology S.X₁ i] [HomologicalComplex.HasHomology S.X₂ i] [HomologicalComplex.HasHomology S.X₃ i] : CategoryTheory.ShortComplex.Exact (CategoryTheory.ShortComplex.mk (HomologicalComplex.opcyclesMap S.f i) (HomologicalComplex.opcyclesMap S.g i) (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap S.f i) (HomologicalComplex.opcyclesMap S.g i) = 0))

If X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 is an exact sequence of homological complexes, then X₁.opcycles i ⟶ X₂.opcycles i ⟶ X₃.opcycles i ⟶ 0 is exact. This lemma states the exactness at X₂.opcycles i, while the fact that X₂.opcycles i ⟶ X₃.opcycles i is an epi is an instance.

theorem HomologicalComplex.cycles_left_exact {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} (S : CategoryTheory.ShortComplex (HomologicalComplex C c)) (hS : CategoryTheory.ShortComplex.Exact S) [CategoryTheory.Mono S.f] (i : ι) [HomologicalComplex.HasHomology S.X₁ i] [HomologicalComplex.HasHomology S.X₂ i] [HomologicalComplex.HasHomology S.X₃ i] : CategoryTheory.ShortComplex.Exact (CategoryTheory.ShortComplex.mk (HomologicalComplex.cyclesMap S.f i) (HomologicalComplex.cyclesMap S.g i) (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap S.f i) (HomologicalComplex.cyclesMap S.g i) = 0))

If 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ is an exact sequence of homological complex, then 0 ⟶ X₁.cycles i ⟶ X₂.cycles i ⟶ X₃.cycles i is exact. This lemma states the exactness at X₂.cycles i, while the fact that X₁.cycles i ⟶ X₂.cycles i is a mono is an instance.

noncomputable def HomologicalComplex.HomologySequence.snakeInput {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : CategoryTheory.ShortComplex.ShortExact S) (i : ι) (j : ι) (hij : c.Rel i j) : CategoryTheory.ShortComplex.SnakeInput C

Given a short exact short complex S : HomologicalComplex C c, and degrees i and j such that c.Rel i j, this is the snake diagram whose four lines are respectively obtained by applying the functors homologyFunctor C c i, opcyclesFunctor C c i, cyclesFunctor C c j, homologyFunctor C c j to S. Applying the snake lemma to this gives the homology sequence of S.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.ShortComplex.ShortExact.δ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : CategoryTheory.ShortComplex.ShortExact S) (i : ι) (j : ι) (hij : c.Rel i j) : HomologicalComplex.homology S.X₃ i ⟶ HomologicalComplex.homology S.X₁ j

The connecting homoomorphism S.X₃.homology i ⟶ S.X₁.homology j for a short exact short complex S.

Equations

• CategoryTheory.ShortComplex.ShortExact.δ hS i j hij = CategoryTheory.ShortComplex.SnakeInput.δ (HomologicalComplex.HomologySequence.snakeInput hS i j hij)

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.δ_comp_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : CategoryTheory.ShortComplex.ShortExact S) (i : ι) (j : ι) (hij : c.Rel i j) {Z : C} (h : HomologicalComplex.homology S.X₂ j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.ShortExact.δ hS i j hij) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap S.f j) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.δ_comp {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : CategoryTheory.ShortComplex.ShortExact S) (i : ι) (j : ι) (hij : c.Rel i j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.ShortExact.δ hS i j hij) (HomologicalComplex.homologyMap S.f j) = 0

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.comp_δ_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : CategoryTheory.ShortComplex.ShortExact S) (i : ι) (j : ι) (hij : c.Rel i j) {Z : C} (h : HomologicalComplex.homology S.X₁ j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap S.g i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.ShortExact.δ hS i j hij) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.comp_δ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : CategoryTheory.ShortComplex.ShortExact S) (i : ι) (j : ι) (hij : c.Rel i j) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap S.g i) (CategoryTheory.ShortComplex.ShortExact.δ hS i j hij) = 0

theorem CategoryTheory.ShortComplex.ShortExact.homology_exact₁ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : CategoryTheory.ShortComplex.ShortExact S) (i : ι) (j : ι) (hij : c.Rel i j) : CategoryTheory.ShortComplex.Exact (CategoryTheory.ShortComplex.mk (CategoryTheory.ShortComplex.ShortExact.δ hS i j hij) (HomologicalComplex.homologyMap S.f j) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.ShortExact.δ hS i j hij) (HomologicalComplex.homologyMap S.f j) = 0))

Exactness of S.X₃.homology i ⟶ S.X₁.homology j ⟶ S.X₂.homology j.

theorem CategoryTheory.ShortComplex.ShortExact.homology_exact₂ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : CategoryTheory.ShortComplex.ShortExact S) (i : ι) : CategoryTheory.ShortComplex.Exact (CategoryTheory.ShortComplex.mk (HomologicalComplex.homologyMap S.f i) (HomologicalComplex.homologyMap S.g i) (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap S.f i) (HomologicalComplex.homologyMap S.g i) = 0))

Exactness of S.X₁.homology i ⟶ S.X₂.homology i ⟶ S.X₃.homology i.

theorem CategoryTheory.ShortComplex.ShortExact.homology_exact₃ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : CategoryTheory.ShortComplex.ShortExact S) (i : ι) (j : ι) (hij : c.Rel i j) : CategoryTheory.ShortComplex.Exact (CategoryTheory.ShortComplex.mk (HomologicalComplex.homologyMap S.g i) (CategoryTheory.ShortComplex.ShortExact.δ hS i j hij) (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap S.g i) (CategoryTheory.ShortComplex.ShortExact.δ hS i j hij) = 0))

Exactness of S.X₂.homology i ⟶ S.X₃.homology i ⟶ S.X₁.homology j.

theorem CategoryTheory.ShortComplex.ShortExact.δ_eq' {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : CategoryTheory.ShortComplex.ShortExact S) (i : ι) (j : ι) (hij : c.Rel i j) {A : C} (x₃ : A ⟶ HomologicalComplex.homology S.X₃ i) (x₂ : A ⟶ HomologicalComplex.opcycles S.X₂ i) (x₁ : A ⟶ HomologicalComplex.cycles S.X₁ j) (h₂ : CategoryTheory.CategoryStruct.comp x₂ (HomologicalComplex.opcyclesMap S.g i) = CategoryTheory.CategoryStruct.comp x₃ (HomologicalComplex.homologyι S.X₃ i)) (h₁ : CategoryTheory.CategoryStruct.comp x₁ (HomologicalComplex.cyclesMap S.f j) = CategoryTheory.CategoryStruct.comp x₂ (HomologicalComplex.opcyclesToCycles S.X₂ i j)) : CategoryTheory.CategoryStruct.comp x₃ (CategoryTheory.ShortComplex.ShortExact.δ hS i j hij) = CategoryTheory.CategoryStruct.comp x₁ (HomologicalComplex.homologyπ S.X₁ j)

theorem CategoryTheory.ShortComplex.ShortExact.δ_eq {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : CategoryTheory.ShortComplex.ShortExact S) (i : ι) (j : ι) (hij : c.Rel i j) {A : C} (x₃ : A ⟶ S.X₃.X i) (hx₃ : CategoryTheory.CategoryStruct.comp x₃ (S.X₃.d i j) = 0) (x₂ : A ⟶ S.X₂.X i) (hx₂ : CategoryTheory.CategoryStruct.comp x₂ (S.g.f i) = x₃) (x₁ : A ⟶ S.X₁.X j) (hx₁ : CategoryTheory.CategoryStruct.comp x₁ (S.f.f j) = CategoryTheory.CategoryStruct.comp x₂ (S.X₂.d i j)) (k : ι) (hk : ComplexShape.next c j = k) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles S.X₃ x₃ j (_ : ComplexShape.next c i = j) hx₃) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ S.X₃ i) (CategoryTheory.ShortComplex.ShortExact.δ hS i j hij)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles S.X₁ x₁ k hk (_ : CategoryTheory.CategoryStruct.comp x₁ (S.X₁.d j k) = 0)) (HomologicalComplex.homologyπ S.X₁ j)