Structures · Category theory
CategoryTheory.Functor.IsLeftDerivedFunctor
A functor LF : D ⥤ H is a left derived functor of F : C ⥤ H
if it is equipped with a natural transformation α : L ⋙ LF ⟶ F
which makes it a right Kan extension of F along L,
where L : C ⥤ D is a localization functor for W : MorphismProperty C.
- Shape
- 3 explicit arguments · adds isRightKanExtension
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 by36
- CategoryTheory.Functor.leftDerivedNatTrans
- CategoryTheory.Functor.leftDerivedLift
- CategoryTheory.Functor.IsLeftDerivedFunctor.isRightKanExtension
- CategoryTheory.Functor.leftDerivedNatTrans_fac
- CategoryTheory.Adjunction.derivedη
- CategoryTheory.Functor.leftDerived_fac_app
- CategoryTheory.Functor.leftDerived_fac
- CategoryTheory.Adjunction.derived'
- CategoryTheory.Functor.leftDerivedNatIso
- CategoryTheory.Adjunction.derived
- CategoryTheory.Functor.leftDerivedUnique
- CategoryTheory.Functor.leftDerived_ext
- CategoryTheory.Adjunction.derivedη_fac_app
- CategoryTheory.Functor.leftDerivedNatTrans_fac_assoc
- CategoryTheory.Functor.isIso_of_isLeftDerivedFunctor_of_inverts
- CategoryTheory.Functor.leftDerivedNatTrans_comp
- CategoryTheory.Functor.leftDerivedNatTrans_app
- CategoryTheory.Functor.leftDerivedNatIso_inv
- CategoryTheory.Functor.leftDerivedNatTrans.congr_simp
- CategoryTheory.Adjunction.derived'_counit
- CategoryTheory.Functor.leftDerivedNatTrans_id
- CategoryTheory.Functor.leftDerivedNatTrans_comp_assoc
- CategoryTheory.Functor.leftDerivedNatTrans_app_assoc
- CategoryTheory.Adjunction.derived'_unit
- CategoryTheory.Adjunction.derived_unit
- CategoryTheory.Functor.leftDerivedNatIso_hom
- CategoryTheory.Functor.isLeftDerivedFunctor_iff_isIso_leftDerivedLift
- CategoryTheory.Functor.HasLeftDerivedFunctor.mk'
- CategoryTheory.Functor.leftDerivedLift.congr_simp
- CategoryTheory.Functor.isPointwiseRightKanExtensionOfHasPointwiseLeftDerivedFunctor
- CategoryTheory.Functor.leftDerivedUnique.congr_simp
- CategoryTheory.Adjunction.derived_counit
- CategoryTheory.Adjunction.derivedη_fac_app_assoc
- CategoryTheory.Functor.leftDerived_fac_app_assoc
- CategoryTheory.Adjunction.derivedη.congr_simp
- CategoryTheory.Functor.leftDerived_fac_assoc
Ancestors0
No ancestors.