Structures · Category theory
CategoryTheory.Functor.IsRightKanExtension
Given α : L ⋙ F' ⟶ F, the property F'.IsRightKanExtension α asserts that
(F', α) is a terminal object in the category RightExtension L F, i.e. that (F', α)
is a right Kan extension of F along L.
- Shape
- 2 explicit arguments · adds nonempty_isUniversal
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- FintypeCat
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by37
- CategoryTheory.Functor.liftOfIsRightKanExtension
- CategoryTheory.Functor.liftOfIsRightKanExtension_fac
- CategoryTheory.Functor.isUniversalOfIsRightKanExtension
- CategoryTheory.Functor.limitIsoOfIsRightKanExtension
- CategoryTheory.Functor.rightKanExtensionUnique
- CategoryTheory.Functor.rightKanExtensionUnique_hom
- CategoryTheory.Functor.liftOfIsRightKanExtension_fac_app
- CategoryTheory.Functor.isRightKanExtension_iff_isIso
- CategoryTheory.Functor.homEquivOfIsRightKanExtension
- CategoryTheory.Functor.hom_ext_of_isRightKanExtension
- CategoryTheory.Functor.coneOfIsRightKanExtension
- CategoryTheory.Functor.limitIsoOfIsRightKanExtension_inv_π
- CategoryTheory.Functor.liftOfIsRightKanExtension.congr_simp
- CategoryTheory.Functor.isRightKanExtension_of_iso
- CategoryTheory.Functor.isLimitConeOfIsRightKanExtension
- CategoryTheory.Functor.rightKanExtensionUniqueOfIso
- CategoryTheory.Functor.rightKanExtensionUnique_inv
- CategoryTheory.Functor.IsRightKanExtension.nonempty_isUniversal
- CategoryTheory.Functor.limitIsoOfIsRightKanExtension_hom_π
- CategoryTheory.Functor.homEquivOfIsRightKanExtension_apply_app
- CategoryTheory.Functor.rightKanExtensionUniqueOfIso_hom
- CategoryTheory.Functor.homEquivOfIsRightKanExtension.congr_simp
- CategoryTheory.Functor.limitIsoOfIsRightKanExtension.congr_simp
- CategoryTheory.Functor.limitIsoOfIsRightKanExtension_inv_π_assoc
- CategoryTheory.Functor.rightKanExtensionUniqueOfIso_inv
- CategoryTheory.Functor.PreservesRightKanExtension.mk_of_preserves_isRightKanExtension
- CategoryTheory.Functor.isPointwiseRightKanExtensionOfIsRightKanExtension
- CategoryTheory.Functor.coneOfIsRightKanExtension_π
- CategoryTheory.Functor.PreservesRightKanExtension.preserves
- Topology.IsUpperSet.isSheaf_of_isRightKanExtension
- CategoryTheory.Functor.homEquivOfIsRightKanExtension_symm_apply
- CategoryTheory.Functor.liftOfIsRightKanExtension_fac_app_assoc
- CategoryTheory.Functor.coneOfIsRightKanExtension_pt
- CategoryTheory.Functor.isLimitConeOfIsRightKanExtension_lift
- CategoryTheory.Functor.limitIsoOfIsRightKanExtension_hom_π_assoc
- CategoryTheory.Functor.rightKanExtensionUnique.congr_simp
- CategoryTheory.Functor.liftOfIsRightKanExtension_fac_assoc
Ancestors0
No ancestors.