Structures · Algebra
ComplexShape.QFactorsThroughHomotopy
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
- Shape
- 2 explicit arguments · adds areEqualizedByLocalization
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Int
How is a type an instance?
Loading the hierarchy index…
Assumed by17
- HomologicalComplexUpToQuasiIso.Qh
- HomologicalComplexUpToQuasiIso.quotientCompQhIso
- HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh
- CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh
- HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj
- CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app
- HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_inv_app_quotient_obj
- HomologicalComplexUpToQuasiIso.Q_map_eq_of_homotopy
- ComplexShape.QFactorsThroughHomotopy.areEqualizedByLocalization
- HomologicalComplexUpToQuasiIso.instIsLocalizationHomologicalComplexCompHomotopyCategoryQuotientQhQuasiIso
- CategoryTheory.Functor.instLiftingHomotopyCategoryHomologicalComplexUpToQuasiIsoQhQuasiIsoCompMapHomotopyCategoryMapHomologicalComplexUpToQuasiIso
- HomologicalComplexUpToQuasiIso.instIsLocalizationHomotopyCategoryQhQuasiIso
- HomologicalComplexUpToQuasiIso.Qh_inverts_quasiIso
- HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj_assoc
- CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh.congr_simp
- CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc
- HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_inv_app_quotient_obj_assoc
Ancestors0
No ancestors.