Theorems · Theorem · category theory
CategoryTheory.Functor.hasPointwiseRightKanExtension_of_hasPointwiseLeftDerivedFunctor
∀ {C : Type u₁} {D : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} H]
(F : CategoryTheory.Functor C H) (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
[F.HasPointwiseLeftDerivedFunctor W] [L.IsLocalization W], L.HasPointwiseRightKanExtension F- Cited by
- 0 results in Mathlib
- Foundations
- Depth 40 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Functorstatement and proof · cited by 16,252
- CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
- CategoryTheory.Functor.IsLocalizationstatement and proof · cited by 432
- CategoryTheory.Functor.EssSurjproof · cited by 88
- CategoryTheory.Functor.objObjPreimageIsoproof · cited by 54
- CategoryTheory.Functor.objPreimageproof · cited by 49
- CategoryTheory.Functor.HasPointwiseRightKanExtensionstatement · cited by 34
- CategoryTheory.Localization.essSurjproof · cited by 16
- CategoryTheory.Functor.hasPointwiseLeftDerivedFunctorAt_iffproof · cited by 4
- CategoryTheory.Functor.hasPointwiseRightKanExtensionAt_iff_of_isoproof · cited by 3
- CategoryTheory.Functor.HasPointwiseLeftDerivedFunctorstatement and proof · cited by 2
Cited by1
Results whose statement or proof uses this declaration.