Theorems · Theorem · category theory

CochainComplex.ConnectData.homologyMap_map_of_eq_succ

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K K' : ChainComplex C ℕ} {L L' : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L)
  (h' : CochainComplex.ConnectData K' L') (fK : K ⟶ K') (fL : L ⟶ L')
  (f_comm : CategoryTheory.CategoryStruct.comp (fK.f 0) h'.d₀ = CategoryTheory.CategoryStruct.comp h.d₀ (fL.f 0))
  (n : ℕ) [inst_2 : NeZero n] (m : ℤ) (hmn : m = ↑n) [inst_3 : HomologicalComplex.HasHomology h.cochainComplex m]
  [inst_4 : HomologicalComplex.HasHomology L n] [inst_5 : HomologicalComplex.HasHomology h'.cochainComplex m]
  [inst_6 : HomologicalComplex.HasHomology L' n],
  HomologicalComplex.homologyMap (h.map h' fK fL f_comm) m =
    CategoryTheory.CategoryStruct.comp (h.homologyIsoPos n m hmn).hom
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap fL n) (h'.homologyIsoPos n m hmn).inv)

Defined in

Mathlib.Algebra.Homology.Embedding.Connect

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsNeZeroHomologicalComplex.HasHomologyHomologicalComplex.HasHomologyHomologicalComplex.HasHomologyHomologicalComplex.HasHomology