Theorems · Inductive type · category theory

ComplexShape.QFactorsThroughHomotopy

{ι : Type u_3} →
  ComplexShape ι →
    (C : Type u_4) →
      [inst : CategoryTheory.Category.{v_2, u_4} C] →
        [inst_1 : CategoryTheory.Preadditive C] → [CategoryTheory.CategoryWithHomology C] → Prop

The condition on a complex shape c saying that homotopic maps become equal in the localized category with respect to quasi-isomorphisms.

Defined in

Mathlib.Algebra.Homology.Localization

Cited by

11 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.CategoryWithHomology