Theorems · Definition · category theory

CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles

{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._auto_1) →
                [inst_2 : (S.sc hS k ⋯).HasRightHomology] →
                  [inst_3 : (S.sc hS (k + 1) ⋯).HasLeftHomology] → (S.sc hS k ⋯).opcycles ⟶ (S.sc hS (k + 1) ⋯).cycles

If S is a complex, this is the morphism from the opcycles of S in degree k + 1 to the cycles of S in degree k + 2.

Defined in

Mathlib.Algebra.Homology.ExactSequenceFour

Cited by

2 results in Mathlib

Foundations

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

Assumes

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