Theorems · Theorem · category theory

HomologicalComplex.cycles_left_exact

∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} (S : CategoryTheory.ShortComplex (HomologicalComplex C c)),
  S.Exact →
    ∀ [CategoryTheory.Mono S.f] (i : ι) [inst_3 : S.X₁.HasHomology i] [inst_4 : S.X₂.HasHomology i]
      [inst_5 : S.X₃.HasHomology i],
      { X₁ := S.X₁.cycles i, X₂ := S.X₂.cycles i, X₃ := S.X₃.cycles i, f := HomologicalComplex.cyclesMap S.f i,
          g := HomologicalComplex.cyclesMap S.g i, zero := ⋯ }.Exact

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.

Defined in

Mathlib.Algebra.Homology.HomologySequence

Cited by

0 results in Mathlib

Foundations

Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.MonoHomologicalComplex.HasHomologyHomologicalComplex.HasHomologyHomologicalComplex.HasHomology