Theorems · Theorem · category theory

HomologicalComplex.i_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] [inst_6 : (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 : ι) (hj : c.next i = j)
  (hx : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (K.d i j))) x = 0),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (K.iCycles i))) (K.cyclesMk x j hj hx) = x

Defined in

Mathlib.Algebra.Homology.ConcreteCategory

Cited by

5 results in Mathlib

Foundations

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

Assumes

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