Theorems · Definition · category theory

CochainComplex.ConnectData.homologyIsoPos

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {K : ChainComplex C ℕ} →
        {L : CochainComplex C ℕ} →
          (h : CochainComplex.ConnectData K L) →
            (n : ℕ) →
              [NeZero n] →
                (m : ℤ) →
                  m = ↑n →
                    [inst_3 : HomologicalComplex.HasHomology h.cochainComplex m] →
                      [inst_4 : HomologicalComplex.HasHomology L n] →
                        HomologicalComplex.homology h.cochainComplex m ≅ HomologicalComplex.homology L n

Given h : ConnectData K L and n : ℕ non-zero, the homology of h.cochainComplex in degree n identifies to the homology of L in degree n.

Defined in

Mathlib.Algebra.Homology.Embedding.Connect

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsNeZeroHomologicalComplex.HasHomologyHomologicalComplex.HasHomology