Structures · Category theory
CategoryTheory.Functor.IsRightDerivedFunctor
A functor RF : D ⥤ H is a right derived functor of F : C ⥤ H
if it is equipped with a natural transformation α : F ⟶ L ⋙ RF
which makes it a left Kan extension of F along L,
where L : C ⥤ D is a localization functor for W : MorphismProperty C.
- Shape
- 3 explicit arguments · adds isLeftKanExtension
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- HomotopyCategory.Plus
How is a type an instance?
Loading the hierarchy index…
Assumed by47
- CategoryTheory.Functor.rightDerivedNatTrans
- CategoryTheory.Functor.rightDerivedDesc
- CategoryTheory.Functor.IsRightDerivedFunctor.isLeftKanExtension
- CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison
- CategoryTheory.Functor.rightDerived_fac
- CategoryTheory.Functor.rightDerivedNatTrans_fac
- CategoryTheory.Adjunction.derivedε
- CategoryTheory.LocalizerMorphism.Derives.isIso_of_isRightDerivedFunctor
- CategoryTheory.Functor.rightDerived_fac_app
- CategoryTheory.Adjunction.derived'
- CategoryTheory.Functor.rightDerivedNatIso
- CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison_fac
- CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison_fac_app
- CategoryTheory.Functor.rightDerivedUnique
- CategoryTheory.Adjunction.derived
- CategoryTheory.Functor.rightDerived_ext
- CategoryTheory.LocalizerMorphism.isIso_iff_of_isRightDerivabilityStructure
- CategoryTheory.Functor.rightDerivedNatTrans_comp
- CategoryTheory.Functor.rightDerivedNatTrans_app
- CategoryTheory.Functor.isIso_of_isRightDerivedFunctor_of_inverts
- CategoryTheory.Adjunction.derivedε_fac_app
- CategoryTheory.Functor.rightDerivedNatIso_hom
- CategoryTheory.Functor.rightDerivedNatTrans_fac_assoc
- CategoryTheory.Functor.HasRightDerivedFunctor.mk'
- CategoryTheory.Functor.rightDerivedNatTrans_comp_assoc
- CategoryTheory.Functor.rightDerivedNatIso_inv
- CategoryTheory.Adjunction.derived'_counit
- CategoryTheory.LocalizerMorphism.Derives.isIso
- CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison.congr_simp
- CategoryTheory.Functor.isPointwiseLeftKanExtensionOfHasPointwiseRightDerivedFunctor
- CategoryTheory.Functor.rightDerived_fac_app_assoc
- HomotopyCategory.Plus.instIsIsoAppOfInjectiveXIntAsHomologicalComplexUpHomotopicObjPlus
- CategoryTheory.Functor.rightDerived_fac_assoc
- CategoryTheory.Functor.rightDerivedNatTrans_app_assoc
- CategoryTheory.Adjunction.derived'_unit
- CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison_fac_assoc
- CategoryTheory.Functor.isRightDerivedFunctor_iff_isIso_rightDerivedDesc
- CategoryTheory.Adjunction.derived_unit
- CategoryTheory.Functor.rightDerivedNatTrans.congr_simp
- CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison_fac_app_assoc
- CategoryTheory.Adjunction.derived_counit
- CategoryTheory.Functor.rightDerivedUnique.congr_simp
- CategoryTheory.Functor.rightDerivedNatTrans_id
- CategoryTheory.Adjunction.derivedε_fac_app_assoc
- CategoryTheory.Adjunction.derivedε.congr_simp
- CategoryTheory.Functor.rightDerivedDesc.congr_simp
- CategoryTheory.LocalizerMorphism.instIsIsoFunctorRightDerivedFunctorComparison
Ancestors0
No ancestors.