Structures · Category theory
CategoryTheory.MorphismProperty.HasLocalization
The data of a localized category with a given universe for the morphisms.
- Shape
- One type argument · adds D, hD, L, hL
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by48
- HomologicalComplexUpToQuasiIso
- HomologicalComplexUpToQuasiIso.Q
- HomologicalComplexUpToQuasiIso.Qh
- HomologicalComplexUpToQuasiIso.quotientCompQhIso
- HomologicalComplexUpToQuasiIso.homologyFunctorFactors
- HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh
- HomologicalComplexUpToQuasiIso.homologyFunctor
- CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIso
- CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh
- HomologicalComplexUpToQuasiIso.isIso_Q_map_iff_mem_quasiIso
- HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj
- CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactors
- CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app
- HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_inv_app_quotient_obj
- CategoryTheory.MorphismProperty.HasLocalization.D
- CategoryTheory.MorphismProperty.HasLocalization.hD
- HomologicalComplexUpToQuasiIso.Q_map_eq_of_homotopy
- CategoryTheory.MorphismProperty.HasLocalization.L
- CategoryTheory.MorphismProperty.Q'
- CategoryTheory.Triangulated.Localization.instIsTriangulatedLocalization'
- CategoryTheory.MorphismProperty.Localization'
- HomologicalComplexUpToQuasiIso.instIsLocalizationHomologicalComplexCompHomotopyCategoryQuotientQhQuasiIso
- CategoryTheory.Functor.instLiftingHomotopyCategoryHomologicalComplexUpToQuasiIsoQhQuasiIsoCompMapHomotopyCategoryMapHomologicalComplexUpToQuasiIso
- HomologicalComplexUpToQuasiIso.instIsLocalizationHomotopyCategoryQhQuasiIso
- CategoryTheory.Triangulated.Localization.instPretriangulatedLocalization'
- CategoryTheory.Functor.mapHomologicalComplex_upToQuasiIso_Q_inverts_quasiIso
- CategoryTheory.MorphismProperty.HasLocalization.hL
- HomologicalComplexUpToQuasiIso.Q_inverts_homotopyEquivalences
- CategoryTheory.MorphismProperty.locallySmall_of_hasLocalization
- HomologicalComplexUpToQuasiIso.Qh_inverts_quasiIso
- HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj_assoc
- CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh.congr_simp
- CategoryTheory.Localization.instPreadditiveLocalization'
- CategoryTheory.Localization.instLinearLocalization'
- CategoryTheory.HasShift.localization'
- CategoryTheory.Localization.instAdditiveLocalization'Q'
- CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc
- CategoryTheory.Triangulated.Localization.instAdditiveLocalization'ShiftFunctorInt
- CategoryTheory.MorphismProperty.instIsLocalizationLocalization'Q'
- CategoryTheory.Shift.instLinearLocalization'ShiftFunctorOfCommShiftOfQ'
- CategoryTheory.Localization.instLinearLocalization'Q'
- HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_inv_app_quotient_obj_assoc
- CategoryTheory.Localization.instHasZeroObjectLocalization'
- CategoryTheory.MorphismProperty.instCategoryLocalization'
- CategoryTheory.Functor.instLiftingHomologicalComplexHomologicalComplexUpToQuasiIsoQQuasiIsoCompMapHomologicalComplexMapHomologicalComplexUpToQuasiIso
- CategoryTheory.Localization.instPreservesFiniteProductsLocalization'Q'
- CategoryTheory.Localization.instHasFiniteProductsLocalization'
- CategoryTheory.MorphismProperty.commShift_Q'
Ancestors0
No ancestors.