Theorems · Theorem · category theory

ComplexShape.QFactorsThroughHomotopy.areEqualizedByLocalization

∀ {ι : Type u_3} {c : ComplexShape ι} {C : Type u_4} {inst : CategoryTheory.Category.{v_2, u_4} C}
  {inst_1 : CategoryTheory.Preadditive C} {inst_2 : CategoryTheory.CategoryWithHomology C}
  [self : c.QFactorsThroughHomotopy C] {K L : HomologicalComplex C c} {f g : K ⟶ L} (h : Homotopy f g),
  CategoryTheory.AreEqualizedByLocalization (HomologicalComplex.quasiIso C c) f g

Defined in: Mathlib.Algebra.Homology.Localization
Cited by: 1 results in Mathlib
Foundations: Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: ComplexShape.QFactorsThroughHomotopy

Mathlib docs Source Loogle LeanSearch

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
Quiver.Homstatement · cited by 32,603
CategoryTheory.Preadditivestatement and proof · cited by 3,309
HomologicalComplexstatement · cited by 1,691
ComplexShapestatement and proof · cited by 1,684
CategoryTheory.CategoryWithHomologystatement and proof · cited by 116
Homotopystatement · cited by 106
HomologicalComplex.quasiIsostatement · cited by 42
ComplexShape.QFactorsThroughHomotopystatement and proof · cited by 11
CategoryTheory.AreEqualizedByLocalizationstatement · cited by 5

Cited by1

Results whose statement or proof uses this declaration.

HomologicalComplexUpToQuasiIso.Q_map_eq_of_homotopyproof · cited by 1