Theorems · Theorem · category theory

HomologicalComplex.evalCompCoyonedaCorepresentableBySingle_homEquiv_symm_apply

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [inst_3 : DecidableEq ι]
  (hi : ∀ (j : ι), ¬c.Rel i j) (X : C) {K : HomologicalComplex C c}
  (f : ((HomologicalComplex.eval C c i).comp (CategoryTheory.coyoneda.obj (Opposite.op X))).obj K),
  (HomologicalComplex.evalCompCoyonedaCorepresentableBySingle c i hi X).homEquiv.symm f =
    HomologicalComplex.mkHomFromSingle f ⋯

Defined in

Mathlib.Algebra.Homology.Double

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.Limits.HasZeroObjectDecidableEq