Theorems · Theorem · category theory
HomotopyCategory.quasiIso_eq_quasiIso_map_quotient
∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} (c : ComplexShape ι)
[inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.CategoryWithHomology C],
HomotopyCategory.quasiIso C c = (HomologicalComplex.quasiIso C c).map (HomotopyCategory.quotient C c)- Defined in
- Mathlib.Algebra.Homology.Localization
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 48 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites21
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
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functor.mapproof · cited by 8,698
- CategoryTheory.Isoproof · cited by 3,963
- CategoryTheory.Preadditivestatement and proof · cited by 3,309
- CategoryTheory.MorphismPropertystatement · cited by 2,179
- HomologicalComplexstatement and proof · cited by 1,691
- ComplexShapestatement and proof · cited by 1,684
- CategoryTheory.Arrow.mkproof · cited by 421
- HomotopyCategorystatement and proof · cited by 132
- CategoryTheory.CategoryWithHomologystatement and proof · cited by 116
- HomotopyCategory.quotientstatement and proof · cited by 109
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.