Theorems · Definition · category theory

HomologicalComplex.cyclesMk

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type v} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            [inst_3 : CategoryTheory.HasForget₂ C Ab] →
              [inst_4 : CategoryTheory.Abelian C] →
                [inst_5 : (CategoryTheory.forget₂ C Ab).Additive] →
                  [(CategoryTheory.forget₂ C Ab).PreservesHomology] →
                    {ι : Type u_2} →
                      {c : ComplexShape ι} →
                        (K : HomologicalComplex C c) →
                          {i : ι} →
                            (x : ↑((CategoryTheory.forget₂ C Ab).obj (K.X i))) →
                              (j : ι) →
                                c.next i = j →
                                  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (K.d i j)))
                                        x =
                                      0 →
                                    ↑((CategoryTheory.forget₂ C Ab).obj (K.cycles i))

Constructor for cycles of a homological complex in a concrete category.

Defined in

Mathlib.Algebra.Homology.ConcreteCategory

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.HasForget₂CategoryTheory.AbelianCategoryTheory.Functor.AdditiveCategoryTheory.Functor.PreservesHomology