Theorems · Theorem · category theory

CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles_fac

∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.IsComplex) (k : ℕ)
  (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles_fac._auto_1)
  [inst_2 : (S.sc hS k ⋯).HasRightHomology] [inst_3 : (S.sc hS (k + 1) ⋯).HasLeftHomology],
  CategoryTheory.CategoryStruct.comp (S.sc hS k ⋯).pOpcycles
      (CategoryTheory.CategoryStruct.comp (hS.opcyclesToCycles k ⋯) (S.sc hS (k + 1) ⋯).iCycles) =
    S.map' (k + 1) (k + 2) ⋯ ⋯

Defined in

Mathlib.Algebra.Homology.ExactSequenceFour

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.ShortComplex.HasRightHomologyCategoryTheory.ShortComplex.HasLeftHomology