Structures · Category theory
CategoryTheory.Functor.IsLeftKanExtension
Given α : F ⟶ L ⋙ F', the property F'.IsLeftKanExtension α asserts that
(F', α) is an initial object in the category LeftExtension L F, i.e. that (F', α)
is a left 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 instances4
- CategoryTheory.Discrete
- SimplexCategory
- Prod
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by48
- CategoryTheory.Functor.descOfIsLeftKanExtension
- CategoryTheory.Functor.hom_ext_of_isLeftKanExtension
- CategoryTheory.Functor.descOfIsLeftKanExtension_fac
- CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app
- CategoryTheory.Functor.homEquivOfIsLeftKanExtension
- CategoryTheory.Functor.colimitIsoOfIsLeftKanExtension
- CategoryTheory.Functor.leftKanExtensionUnique_hom
- CategoryTheory.Functor.isUniversalOfIsLeftKanExtension
- CategoryTheory.Functor.leftKanExtensionUnique
- CategoryTheory.Functor.descOfIsLeftKanExtension.congr_simp
- CategoryTheory.Presheaf.uliftYonedaAdjunction
- CategoryTheory.Functor.leftKanExtensionUnique_inv
- CategoryTheory.Functor.coconeOfIsLeftKanExtension
- CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_hom
- CategoryTheory.Functor.isLeftKanExtension_iff_isIso
- CategoryTheory.Functor.leftKanExtensionUniqueOfIso
- CategoryTheory.Functor.isLeftKanExtension_of_iso
- CategoryTheory.Functor.leftKanExtensionUniqueOfIso_inv
- CategoryTheory.Functor.isColimitCoconeOfIsLeftKanExtension
- CategoryTheory.Functor.leftKanExtensionUniqueOfIso_hom
- CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension
- CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv
- CategoryTheory.Presheaf.uliftYonedaAdjunction_homEquiv_app
- CategoryTheory.Functor.IsLeftKanExtension.nonempty_isUniversal
- CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_inv
- CategoryTheory.Functor.homEquivOfIsLeftKanExtension.congr_simp
- CategoryTheory.Functor.homEquivOfIsLeftKanExtension_symm_apply
- CategoryTheory.Functor.descOfIsLeftKanExtension_fac_assoc
- CategoryTheory.Functor.leftKanExtensionUniqueOfIso.congr_simp
- CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_hom_assoc
- CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv.congr_simp
- CategoryTheory.Functor.coconeOfIsLeftKanExtension_ι
- CategoryTheory.Functor.leftKanExtensionUnique.congr_simp
- CategoryTheory.Presheaf.uliftYonedaAdjunction_unit_app_app
- CategoryTheory.Functor.PreservesLeftKanExtension.preserves
- CategoryTheory.Functor.isLeftKanExtension_iff_postcompose
- CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension.congr_simp
- CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app_assoc
- CategoryTheory.Functor.PreservesLeftKanExtension.mk_of_preserves_isLeftKanExtension
- CategoryTheory.Presheaf.preservesColimitsOfSize_of_isLeftKanExtension
- CategoryTheory.Presheaf.isIso_of_isLeftKanExtension
- CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_inv_assoc
- CategoryTheory.Functor.isColimitCoconeOfIsLeftKanExtension_desc
- CategoryTheory.Presheaf.uliftYonedaAdjunction.congr_simp
- CategoryTheory.Functor.homEquivOfIsLeftKanExtension_apply_app
- CategoryTheory.Functor.coconeOfIsLeftKanExtension_pt
- CategoryTheory.Functor.colimitIsoOfIsLeftKanExtension.congr_simp
- CategoryTheory.Presheaf.instIsIsoFunctorOfIsLeftKanExtensionOppositeType
Ancestors0
No ancestors.