Theorems · Theorem · category theory

HomologicalComplex.opcycles_right_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.Epi S.g] (i : ι) [inst_3 : S.X₁.HasHomology i] [inst_4 : S.X₂.HasHomology i]
      [inst_5 : S.X₃.HasHomology i],
      { X₁ := S.X₁.opcycles i, X₂ := S.X₂.opcycles i, X₃ := S.X₃.opcycles i, f := HomologicalComplex.opcyclesMap S.f i,
          g := HomologicalComplex.opcyclesMap S.g i, zero := ⋯ }.Exact

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.

Defined in

Mathlib.Algebra.Homology.HomologySequence

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.EpiHomologicalComplex.HasHomologyHomologicalComplex.HasHomologyHomologicalComplex.HasHomology