Theorems · Definition · category theory

CategoryTheory.ShortComplex.cyclesMk

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type w} →
        [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.Preadditive C] →
                [inst_5 : (CategoryTheory.forget₂ C Ab).Additive] →
                  [(CategoryTheory.forget₂ C Ab).PreservesHomology] →
                    (S : CategoryTheory.ShortComplex C) →
                      [inst_7 : S.HasHomology] →
                        (x₂ : ↑((CategoryTheory.forget₂ C Ab).obj S.X₂)) →
                          (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map S.g)) x₂ = 0 →
                            ↑((CategoryTheory.forget₂ C Ab).obj S.cycles)

Constructor for cycles of short complexes in a concrete category.

Defined in

Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.HasForget₂CategoryTheory.PreadditiveCategoryTheory.Functor.AdditiveCategoryTheory.Functor.PreservesHomologyCategoryTheory.ShortComplex.HasHomology