Theorems · Definition · category theory
HomotopyCategory.Plus.quasiIso
(A : Type u_3) →
[inst : CategoryTheory.Category.{v_3, u_3} A] →
[inst_1 : CategoryTheory.Abelian A] → CategoryTheory.MorphismProperty (HomotopyCategory.Plus A)The class of quasi-isomorphisms in the homotopy category of bounded below cochain complexes.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.MorphismPropertystatement · cited by 2,179
- CategoryTheory.Abelianstatement and proof · cited by 1,753
- ComplexShape.upstatement and proof · cited by 1,123
- HomotopyCategorystatement · cited by 132
- CategoryTheory.MorphismProperty.inverseImageproof · cited by 83
- HomotopyCategory.quasiIsoproof · cited by 12
- HomotopyCategory.plusstatement · cited by 9
- HomotopyCategory.Plusstatement · cited by 8
- HomotopyCategory.Plus.ιproof · cited by 2
Cited by6
Results whose statement or proof uses this declaration.
- HomotopyCategory.Plus.localizerMorphismstatement · cited by 1
- HomotopyCategory.Plus.localizerMorphism_derivesstatement · cited by 0
- HomotopyCategory.Plus.quasiIso_eq_subcategoryAcyclic_trWstatement and proof · cited by 0
- HomotopyCategory.Plus.quasiIso_iffstatement · cited by 0
- CategoryTheory.Functor.rightDerivedFunctorPlusUnitproof · cited by 0
- CategoryTheory.Functor.rightDerivedFunctorPlusproof · cited by 0