Structures · Category theory
CategoryTheory.Localization.Lifting
When L : C ⥤ D is a localization functor for W : MorphismProperty C and
F : C ⥤ E is a functor, we shall say that F' : D ⥤ E lifts F if the obvious diagram
is commutative up to an isomorphism.
- Shape
- 4 explicit arguments · adds iso
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- CategoryTheory.Functor
- HomologicalComplex
- HomotopyCategory
- CochainComplex
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by52
- CategoryTheory.Localization.Lifting.iso
- CategoryTheory.Localization.liftNatTrans_app
- CategoryTheory.Localization.liftNatIso
- CategoryTheory.Localization.liftNatTrans
- CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost
- CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp
- CategoryTheory.Functor.commShiftOfLocalization.iso
- CategoryTheory.Localization.Monoidal.functorMonoidalOfComp
- CategoryTheory.Localization.equivalence
- CategoryTheory.Localization.liftNatIso_hom
- CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app
- CategoryTheory.Functor.commShiftOfLocalization
- CategoryTheory.Functor.commShiftOfLocalization.iso_hom_app
- CategoryTheory.Functor.commShiftOfLocalization.iso_inv_app
- CategoryTheory.Localization.functor_linear_iff
- CategoryTheory.Functor.commShiftOfLocalization_iso_hom_app
- CategoryTheory.Functor.commShiftOfLocalization_iso_inv_app
- CategoryTheory.Localization.liftNatTrans.congr_simp
- CategoryTheory.Localization.liftNatIso_inv
- CategoryTheory.Localization.comp_liftNatTrans
- CategoryTheory.Localization.isEquivalence
- CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε
- CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_μ
- CategoryTheory.Localization.Lifting.ofIsos
- CategoryTheory.Localization.liftNatIso.congr_simp
- CategoryTheory.Localization.liftNatTrans_add
- CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPre_iso
- CategoryTheory.Functor.commShiftOfLocalization.iso_hom_app_assoc
- CategoryTheory.Functor.commShiftOfLocalization.iso_inv_app_assoc
- CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPre
- CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_μIso_hom
- CategoryTheory.Localization.Lifting.compRight_iso
- CategoryTheory.Localization.comp_liftNatTrans_assoc
- CategoryTheory.Localization.Monoidal.lifting_isMonoidal
- CategoryTheory.NatTrans.commShift_iso_hom_of_localization
- CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_εIso_hom
- CategoryTheory.Localization.Lifting.compRight
- CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_μ_assoc
- CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPost_iso
- CategoryTheory.Localization.liftNatTrans_zero
- CategoryTheory.Localization.Lifting.ofIsos_iso
- CategoryTheory.Localization.liftNatTrans_id
- CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app'
- CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_εIso_inv
- CategoryTheory.Localization.equivalence_counitIso_app
- CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_μIso_inv
- CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε_assoc
- CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost.congr_simp
- CategoryTheory.Functor.commShiftOfLocalization.iso.congr_simp
- CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPost
Ancestors0
No ancestors.