Theorems · Inductive type · category theory
CochainComplex.IsKProjective
{C : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} C] → [inst_1 : CategoryTheory.Abelian C] → CochainComplex C ℤ → PropA cochain complex K is K-projective if any morphism K ⟶ L
with L acyclic is homotopic to zero.
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 38 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
- CategoryTheory.Abelianstatement · cited by 1,753
- CochainComplexstatement · cited by 1,016
Cited by19
Results whose statement or proof uses this declaration.
- CochainComplex.IsKProjective.homotopyZerostatement · cited by 3
- CochainComplex.isKProjective_of_isostatement and proof · cited by 2
- CochainComplex.IsKProjective.Qh_map_bijectivestatement and proof · cited by 2
- CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjectivestatement and proof · cited by 2
- CochainComplex.isKProjective_iff_leftOrthogonalstatement and proof · cited by 1
- CochainComplex.isKProjective_of_opstatement · cited by 1
- CochainComplex.IsKProjective.leftOrthogonalstatement and proof · cited by 1
- CochainComplex.IsKProjective.nonempty_homotopy_zerostatement and proof · cited by 1
- CochainComplex.IsKProjective.quasiIso_iffstatement and proof · cited by 1
- CochainComplex.HomComplex.CohomologyClass.bijective_toSmallShiftedHom_of_isKProjectivestatement and proof · cited by 1
- HomotopyEquiv.isKProjectivestatement and proof · cited by 1
- CochainComplex.isKProjective_iff_of_isostatement and proof · cited by 0