Structures · Category theory
CategoryTheory.Functor.IsLocalization
The predicate expressing that, up to equivalence, a functor L : C ⥤ D
identifies the category D with the localized category of C with respect
to W : MorphismProperty C.
- Shape
- 2 explicit arguments · adds inverts, isEquivalence
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances14
- CategoryTheory.Functor
- HomologicalComplex
- TopCat
- HomotopyCategory
- PresheafOfModules
- CochainComplex
- CochainComplex.Plus
- HomotopyCategory.Plus
- HomotopicalAlgebra.CofibrantObject
- HomotopicalAlgebra.BifibrantObject
- HomotopicalAlgebra.FibrantObject
- HomotopicalAlgebra.CofibrantObject.HoCat
- Prod
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by591
- CategoryTheory.Localization.inverts
- CategoryTheory.LocalizedMonoidal
- CategoryTheory.Localization.isoOfHom
- CategoryTheory.LocalizerMorphism.localizedFunctor
- CategoryTheory.Localization.Monoidal.toMonoidalCategory
- CategoryTheory.Localization.SmallHom.equiv
- CategoryTheory.Localization.SmallShiftedHom.equiv
- CategoryTheory.Localization.liftNatTrans_app
- CategoryTheory.Localization.Monoidal.tensorBifunctor
- CategoryTheory.Localization.homEquiv
- CategoryTheory.Localization.uniq
- CategoryTheory.Localization.compUniqFunctor
- CategoryTheory.Localization.essSurj
- CategoryTheory.Localization.Monoidal.μ
- CategoryTheory.Localization.Preadditive.add'
- CategoryTheory.Localization.exists_leftFraction
- CategoryTheory.Localization.liftNatIso
- CategoryTheory.Localization.SmallHom.equiv_comp
- CategoryTheory.Localization.liftNatTrans
- CategoryTheory.Localization.SmallHom.equiv_mk
- CategoryTheory.LocalizerMorphism.homMap
- CategoryTheory.Functor.rightDerivedNatTrans
- CategoryTheory.Localization.fac
- CategoryTheory.Functor.leftDerivedNatTrans
- CategoryTheory.Localization.lift
- CategoryTheory.Localization.Monoidal.braidingNatIso
- CategoryTheory.Localization.SmallShiftedHom.equiv_comp
- CategoryTheory.Functor.rightDerivedDesc
- CategoryTheory.Functor.IsLocalization.of_equivalence_target
- CategoryTheory.Localization.Preadditive.add'_eq
- CategoryTheory.Localization.Preadditive.add
- CategoryTheory.Functor.leftDerivedLift
- CategoryTheory.Localization.exists_leftFraction₂
- CategoryTheory.Localization.natTrans_ext
- CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost
- CategoryTheory.ObjectProperty.SerreClassLocalization.abelian
- HomotopicalAlgebra.leftHomotopyClassToHom
- CategoryTheory.CatCenter.localization
- CategoryTheory.Localization.SmallShiftedHom.equiv_mk₀
- CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison
- CategoryTheory.areEqualizedByLocalization_iff
- CategoryTheory.Localization.hasSmallLocalizedHom_iff
- CategoryTheory.ObjectProperty.SerreClassLocalization.map_eq_zero_iff
- CategoryTheory.Localization.Monoidal.associator_naturality
- CategoryTheory.Functor.rightDerived_fac
- CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp
- CategoryTheory.Localization.Monoidal.ε'
- CategoryTheory.Localization.Monoidal.whiskerLeft_id
- CategoryTheory.Localization.isoOfHom_inv_hom_id
- CategoryTheory.Functor.hasPointwiseRightDerivedFunctorAt_iff
Ancestors0
No ancestors.