Presheaf

📁 Source: Mathlib/CategoryTheory/Limits/Presheaf.lean

Statistics

Metric	Count
Definitions coconeπOpCompShrinkYonedaFlip, coconeπOpCompShrinkYonedaObj, isColimitCoconeπOpCompShrinkYonedaFlip, isColimitCoconeπOpCompShrinkYonedaObj, isInitialElementsMkShrinkYonedaObjObjEquivId, shrinkYonedaCompWhiskeringLeftObjπCompColimIso, coconeOfRepresentable, colimitOfRepresentable, compULiftYonedaIsoULiftYonedaCompLan, coconeApp, extensionHom, natTrans, presheafHom, functorToRepresentables, instUniqueHomLeftExtensionFunctorOppositeTypeUliftYonedaCompMkLanOpHomCompULiftYonedaIsoULiftYonedaCompLan, instUniqueHomLeftExtensionOppositeOpObjFunctorTypeUliftYonedaMkUliftYonedaMap, instUniqueHomLeftExtensionOppositeOpObjFunctorTypeYonedaMkYonedaMap, isColimitTautologicalCocone, isColimitTautologicalCocone', isExtensionAlongULiftYoneda, restrictedULiftYoneda, restrictedULiftYonedaHomEquiv, restrictedULiftYonedaHomEquiv', tautologicalCocone, tautologicalCocone', uliftYonedaAdjunction, uniqueExtensionAlongULiftYoneda	27
Theorems coconeπOpCompShrinkYonedaObj_pt, coconeπOpCompShrinkYonedaObj_ι_app, instHasInitialObjOppositeTypeFlipShrinkYonedaOp, shrinkYonedaCompWhiskeringLeftObjπCompColimIso_inv_app_apply, shrinkYoneda_map_app_coconeπOpCompShrinkYonedaObj_ι_app, shrinkYoneda_map_app_coconeπOpCompShrinkYonedaObj_ι_app_assoc, coconeOfRepresentable_naturality, coconeOfRepresentable_pt, coconeOfRepresentable_ι_app, coconeApp_naturality, coconeApp_naturality_assoc, hom_ext, hom_ext_iff, natTrans_app_uliftYoneda_obj, presheafHom_naturality, presheafHom_naturality_assoc, uliftYonedaEquiv_presheafHom_uliftYoneda_obj, uliftYonedaEquiv_ι_presheafHom, compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id, final_toCostructuredArrow_comp_pre, functorToRepresentables_map, functorToRepresentables_obj, instIsIsoFunctorLeftKanExtensionUnitOppositeTypeUliftYoneda, instIsIsoFunctorOfIsLeftKanExtensionOppositeType, instIsLeftKanExtensionFunctorOppositeTypeIdCompUliftYonedaOfPreservesColimitsOfSizeOfHasPointwiseLeftKanExtension, instIsLeftKanExtensionFunctorOppositeTypeLanOpHomCompULiftYonedaIsoULiftYonedaCompLan, instIsLeftKanExtensionOppositeObjFunctorTypeUliftYonedaUliftYonedaMap, instIsLeftKanExtensionOppositeObjFunctorTypeYonedaYonedaMap, isIso_of_isLeftKanExtension, isLeftAdjoint_of_preservesColimits, isLeftKanExtension_along_uliftYoneda_iff, isLeftKanExtension_of_preservesColimits, map_comp_uliftYonedaEquiv_down, map_comp_uliftYonedaEquiv_down_assoc, preservesColimitsOfSize_leftKanExtension, preservesColimitsOfSize_of_isLeftKanExtension, restrictedULiftYonedaHomEquiv'_symm_app_naturality_left, restrictedULiftYonedaHomEquiv'_symm_app_naturality_left_assoc, restrictedULiftYonedaHomEquiv'_symm_naturality_right, restrictedULiftYonedaHomEquiv'_symm_naturality_right_assoc, restrictedULiftYoneda_map_app, restrictedULiftYoneda_obj_map, tautologicalCocone'_pt, tautologicalCocone'_ι_app, tautologicalCocone_pt, tautologicalCocone_ι_app, uliftYonedaAdjunction_homEquiv_app, uliftYonedaAdjunction_unit_app_app	48
Total	75

CategoryTheory.Functor.Elements

Definitions

Name	Category	Theorems
coconeπOpCompShrinkYonedaFlip 📖	CompOp	—
coconeπOpCompShrinkYonedaObj 📖	CompOp	4 math math: shrinkYoneda_map_app_coconeπOpCompShrinkYonedaObj_ι_app_assoc, coconeπOpCompShrinkYonedaObj_pt, shrinkYoneda_map_app_coconeπOpCompShrinkYonedaObj_ι_app, coconeπOpCompShrinkYonedaObj_ι_app
isColimitCoconeπOpCompShrinkYonedaFlip 📖	CompOp	—
isColimitCoconeπOpCompShrinkYonedaObj 📖	CompOp	—
isInitialElementsMkShrinkYonedaObjObjEquivId 📖	CompOp	—
shrinkYonedaCompWhiskeringLeftObjπCompColimIso 📖	CompOp	1 math math: shrinkYonedaCompWhiskeringLeftObjπCompColimIso_inv_app_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coconeπOpCompShrinkYonedaObj_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt Opposite CategoryTheory.Functor.Elements CategoryTheory.Category.opposite CategoryTheory.categoryOfElements CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.CategoryOfElements.π CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shrinkYoneda coconeπOpCompShrinkYonedaObj	—	—
coconeπOpCompShrinkYonedaObj_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Functor.Elements CategoryTheory.Category.opposite CategoryTheory.categoryOfElements CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.CategoryOfElements.π CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shrinkYoneda CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.ι coconeπOpCompShrinkYonedaObj CategoryTheory.Functor.map Opposite.unop DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.shrinkYonedaObjObjEquiv	—	—
instHasInitialObjOppositeTypeFlipShrinkYonedaOp 📖	mathematical	—	CategoryTheory.Limits.HasInitial CategoryTheory.Functor.Elements CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.flip CategoryTheory.shrinkYoneda Opposite.op CategoryTheory.categoryOfElements	—	CategoryTheory.Limits.IsInitial.hasInitial
shrinkYonedaCompWhiskeringLeftObjπCompColimIso_inv_app_apply 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.shrinkYoneda CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op CategoryTheory.CategoryOfElements.π CategoryTheory.Limits.colim CategoryTheory.Iso.inv shrinkYonedaCompWhiskeringLeftObjπCompColimIso CategoryTheory.Limits.colimit.ι CategoryTheory.Limits.hasColimitOfHasColimitsOfShape Opposite.op DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.shrinkYonedaObjObjEquiv CategoryTheory.CategoryStruct.id	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv Equiv.apply_symm_apply CategoryTheory.FunctorToTypes.map_id_apply
shrinkYoneda_map_app_coconeπOpCompShrinkYonedaObj_ι_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shrinkYoneda Opposite.op CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.CategoryOfElements.π coconeπOpCompShrinkYonedaObj CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Limits.Cocone.ι	—	CategoryTheory.types_ext Equiv.surjective CategoryTheory.shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm Equiv.apply_symm_apply CategoryTheory.FunctorToTypes.map_comp_apply
shrinkYoneda_map_app_coconeπOpCompShrinkYonedaObj_ι_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shrinkYoneda Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.CategoryOfElements.π coconeπOpCompShrinkYonedaObj CategoryTheory.Limits.Cocone.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shrinkYoneda_map_app_coconeπOpCompShrinkYonedaObj_ι_app

CategoryTheory.Presheaf

Definitions

Name	Category	Theorems
coconeOfRepresentable 📖	CompOp	3 math math: coconeOfRepresentable_pt, coconeOfRepresentable_naturality, coconeOfRepresentable_ι_app
colimitOfRepresentable 📖	CompOp	—
compULiftYonedaIsoULiftYonedaCompLan 📖	CompOp	3 math math: instIsLeftKanExtensionFunctorOppositeTypeLanOpHomCompULiftYonedaIsoULiftYonedaCompLan, compULiftYonedaIsoULiftYonedaCompLan.natTrans_app_uliftYoneda_obj, compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id
functorToRepresentables 📖	CompOp	5 math math: coconeOfRepresentable_pt, functorToRepresentables_map, functorToRepresentables_obj, coconeOfRepresentable_naturality, coconeOfRepresentable_ι_app
instUniqueHomLeftExtensionFunctorOppositeTypeUliftYonedaCompMkLanOpHomCompULiftYonedaIsoULiftYonedaCompLan 📖	CompOp	—
instUniqueHomLeftExtensionOppositeOpObjFunctorTypeUliftYonedaMkUliftYonedaMap 📖	CompOp	—
instUniqueHomLeftExtensionOppositeOpObjFunctorTypeYonedaMkYonedaMap 📖	CompOp	—
isColimitTautologicalCocone 📖	CompOp	—
isColimitTautologicalCocone' 📖	CompOp	—
isExtensionAlongULiftYoneda 📖	CompOp	—
restrictedULiftYoneda 📖	CompOp	13 math math: CategoryTheory.Functor.instFullOppositeTypeRestrictedULiftYonedaOfIsDense, restrictedULiftYoneda_obj_map, CategoryTheory.Functor.isDense_iff_fullyFaithful_restrictedULiftYoneda, restrictedULiftYoneda_map_app, uliftYonedaAdjunction_homEquiv_app, CategoryTheory.Functor.instFaithfulOppositeTypeRestrictedULiftYonedaOfIsDense, uliftYonedaAdjunction_unit_app_app, map_comp_uliftYonedaEquiv_down_assoc, map_comp_uliftYonedaEquiv_down, restrictedULiftYonedaHomEquiv'_symm_app_naturality_left, restrictedULiftYonedaHomEquiv'_symm_naturality_right_assoc, restrictedULiftYonedaHomEquiv'_symm_app_naturality_left_assoc, restrictedULiftYonedaHomEquiv'_symm_naturality_right
restrictedULiftYonedaHomEquiv 📖	CompOp	—
restrictedULiftYonedaHomEquiv' 📖	CompOp	4 math math: restrictedULiftYonedaHomEquiv'_symm_app_naturality_left, restrictedULiftYonedaHomEquiv'_symm_naturality_right_assoc, restrictedULiftYonedaHomEquiv'_symm_app_naturality_left_assoc, restrictedULiftYonedaHomEquiv'_symm_naturality_right
tautologicalCocone 📖	CompOp	2 math math: tautologicalCocone_ι_app, tautologicalCocone_pt
tautologicalCocone' 📖	CompOp	2 math math: tautologicalCocone'_pt, tautologicalCocone'_ι_app
uliftYonedaAdjunction 📖	CompOp	2 math math: uliftYonedaAdjunction_homEquiv_app, uliftYonedaAdjunction_unit_app_app
uniqueExtensionAlongULiftYoneda 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coconeOfRepresentable_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements functorToRepresentables CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt coconeOfRepresentable CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Functor.op CategoryTheory.CategoryOfElements.map	—	CategoryTheory.NatTrans.ext' CategoryTheory.types_ext CategoryTheory.FunctorToTypes.naturality
coconeOfRepresentable_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt Opposite CategoryTheory.Functor.Elements CategoryTheory.Category.opposite CategoryTheory.categoryOfElements CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category functorToRepresentables coconeOfRepresentable	—	—
coconeOfRepresentable_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Functor.Elements CategoryTheory.Category.opposite CategoryTheory.categoryOfElements CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category functorToRepresentables CategoryTheory.Functor.obj CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.ι coconeOfRepresentable DFunLike.coe Equiv Opposite.op CategoryTheory.Functor.leftOp CategoryTheory.CategoryOfElements.π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.uliftYoneda EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.uliftYonedaEquiv Opposite.unop	—	—
compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id 📖	mathematical	CategoryTheory.Functor.HasLeftKanExtension Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.op	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.uliftYoneda CategoryTheory.Functor.lan CategoryTheory.Functor.op CategoryTheory.Iso.inv compULiftYonedaIsoULiftYonedaCompLan Opposite.op CategoryTheory.Functor.id CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.lanUnit CategoryTheory.yoneda CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver	—	CategoryTheory.Functor.instIsLeftKanExtensionObjLanAppLanUnit CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app CategoryTheory.Functor.map_id
final_toCostructuredArrow_comp_pre 📖	mathematical	—	CategoryTheory.Functor.Final CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.comp CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Limits.Cocone.toCostructuredArrow CategoryTheory.CostructuredArrow.pre	—	CategoryTheory.Functor.final_of_isTerminal_colimit_comp_yoneda CategoryTheory.Over.hasColimit_of_hasColimit_comp_forget CategoryTheory.Limits.functorCategoryHasColimit CategoryTheory.Limits.Types.hasColimit UnivLE.small UnivLE.self CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom_assoc CategoryTheory.Over.w CategoryTheory.Category.comp_id CategoryTheory.CreatesLimit.toReflectsLimit CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Limits.instHasColimitCompOfPreservesColimit
functorToRepresentables_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Functor.Elements CategoryTheory.Category.opposite CategoryTheory.categoryOfElements CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category functorToRepresentables CategoryTheory.uliftYoneda Opposite.unop CategoryTheory.Functor.obj Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom	—	—
functorToRepresentables_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Functor.Elements CategoryTheory.Category.opposite CategoryTheory.categoryOfElements CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category functorToRepresentables CategoryTheory.uliftYoneda Opposite.unop	—	—
instIsIsoFunctorLeftKanExtensionUnitOppositeTypeUliftYoneda 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.uliftYoneda CategoryTheory.Functor.leftKanExtension CategoryTheory.Functor.instHasLeftKanExtension CategoryTheory.Functor.leftKanExtensionUnit	—	isIso_of_isLeftKanExtension CategoryTheory.Functor.instHasLeftKanExtension CategoryTheory.Functor.instIsLeftKanExtensionLeftKanExtensionLeftKanExtensionUnit
instIsIsoFunctorOfIsLeftKanExtensionOppositeType 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.uliftYoneda	—	CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isIso_hom CategoryTheory.ULiftYoneda.instFullFunctorOppositeTypeUliftYoneda CategoryTheory.ULiftYoneda.instFaithfulFunctorOppositeTypeUliftYoneda
instIsLeftKanExtensionFunctorOppositeTypeIdCompUliftYonedaOfPreservesColimitsOfSizeOfHasPointwiseLeftKanExtension 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda CategoryTheory.Functor.comp	CategoryTheory.Functor.IsLeftKanExtension CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda CategoryTheory.Functor.comp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	isLeftKanExtension_of_preservesColimits
instIsLeftKanExtensionFunctorOppositeTypeLanOpHomCompULiftYonedaIsoULiftYonedaCompLan 📖	mathematical	CategoryTheory.Functor.HasLeftKanExtension Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.op	CategoryTheory.Functor.IsLeftKanExtension CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.lan CategoryTheory.Functor.op CategoryTheory.uliftYoneda CategoryTheory.Functor.comp CategoryTheory.Iso.hom compULiftYonedaIsoULiftYonedaCompLan	—	—
instIsLeftKanExtensionOppositeObjFunctorTypeUliftYonedaUliftYonedaMap 📖	mathematical	—	CategoryTheory.Functor.IsLeftKanExtension Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.uliftYoneda CategoryTheory.Functor.op CategoryTheory.uliftYonedaMap	—	—
instIsLeftKanExtensionOppositeObjFunctorTypeYonedaYonedaMap 📖	mathematical	—	CategoryTheory.Functor.IsLeftKanExtension Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Functor.op CategoryTheory.yonedaMap	—	—
isIso_of_isLeftKanExtension 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.uliftYoneda	—	CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isIso_hom CategoryTheory.ULiftYoneda.instFullFunctorOppositeTypeUliftYoneda CategoryTheory.ULiftYoneda.instFaithfulFunctorOppositeTypeUliftYoneda
isLeftAdjoint_of_preservesColimits 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension Opposite CategoryTheory.Functor CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.congrLeft CategoryTheory.opOpEquivalence	CategoryTheory.Functor.IsLeftAdjoint CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category	—	instIsLeftKanExtensionFunctorOppositeTypeIdCompUliftYonedaOfPreservesColimitsOfSizeOfHasPointwiseLeftKanExtension CategoryTheory.Limits.comp_preservesColimits CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_functor
isLeftKanExtension_along_uliftYoneda_iff 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda	CategoryTheory.Functor.IsLeftKanExtension CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda CategoryTheory.IsIso CategoryTheory.Functor.comp CategoryTheory.Limits.PreservesColimitsOfSize	—	instIsIsoFunctorOfIsLeftKanExtensionOppositeType CategoryTheory.Limits.preservesColimits_of_natIso CategoryTheory.Functor.instHasLeftKanExtension CategoryTheory.Functor.instIsLeftKanExtensionLeftKanExtensionLeftKanExtensionUnit preservesColimitsOfSize_leftKanExtension CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Category.comp_id CategoryTheory.Functor.whiskerRight_id' CategoryTheory.Category.assoc CategoryTheory.Functor.whiskerLeft_twice CategoryTheory.NatIso.isIso_app_of_isIso CategoryTheory.NatIso.isIso_inv_app CategoryTheory.Category.id_comp CategoryTheory.IsIso.inv_hom_id_assoc
isLeftKanExtension_of_preservesColimits 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda	CategoryTheory.Functor.IsLeftKanExtension CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda CategoryTheory.Iso.hom CategoryTheory.Functor.comp	—	isLeftKanExtension_along_uliftYoneda_iff CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape
map_comp_uliftYonedaEquiv_down 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Functor.op Opposite.op DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.uliftYoneda restrictedULiftYoneda EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.uliftYonedaEquiv	—	CategoryTheory.NatTrans.naturality CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
map_comp_uliftYonedaEquiv_down_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Functor.op Opposite.op DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.uliftYoneda restrictedULiftYoneda EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.uliftYonedaEquiv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_comp_uliftYonedaEquiv_down
preservesColimitsOfSize_leftKanExtension 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.leftKanExtension CategoryTheory.uliftYoneda CategoryTheory.Functor.instHasLeftKanExtension	—	CategoryTheory.Adjunction.leftAdjoint_preservesColimits CategoryTheory.Functor.instHasLeftKanExtension CategoryTheory.Functor.instIsLeftKanExtensionLeftKanExtensionLeftKanExtensionUnit
preservesColimitsOfSize_of_isLeftKanExtension 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category	—	CategoryTheory.Adjunction.leftAdjoint_preservesColimits
restrictedULiftYonedaHomEquiv'_symm_app_naturality_left 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj CategoryTheory.Functor.obj CategoryTheory.Functor.const DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct restrictedULiftYoneda EquivLike.toFunLike Equiv.instEquivLike Equiv.symm restrictedULiftYonedaHomEquiv' CategoryTheory.CategoryStruct.comp CategoryTheory.CostructuredArrow.map	—	—
restrictedULiftYonedaHomEquiv'_symm_app_naturality_left_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.proj CategoryTheory.Functor.const CategoryTheory.NatTrans.app CategoryTheory.Functor.comp DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver restrictedULiftYoneda EquivLike.toFunLike Equiv.instEquivLike Equiv.symm restrictedULiftYonedaHomEquiv' CategoryTheory.CostructuredArrow.map	—	Mathlib.Tactic.Reassoc.eq_whisker' restrictedULiftYonedaHomEquiv'_symm_app_naturality_left
restrictedULiftYonedaHomEquiv'_symm_naturality_right 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj restrictedULiftYoneda CategoryTheory.CostructuredArrow CategoryTheory.uliftYoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj CategoryTheory.Functor.const EquivLike.toFunLike Equiv.instEquivLike Equiv.symm restrictedULiftYonedaHomEquiv' CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	—	—
restrictedULiftYonedaHomEquiv'_symm_naturality_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.CostructuredArrow Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj CategoryTheory.Functor.obj CategoryTheory.Functor.const DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver restrictedULiftYoneda EquivLike.toFunLike Equiv.instEquivLike Equiv.symm restrictedULiftYonedaHomEquiv' CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' restrictedULiftYonedaHomEquiv'_symm_naturality_right
restrictedULiftYoneda_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op CategoryTheory.uliftYoneda CategoryTheory.Functor.map restrictedULiftYoneda Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.CategoryStruct.comp	—	—
restrictedULiftYoneda_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category restrictedULiftYoneda Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.CategoryStruct.comp Quiver.Hom.unop	—	—
tautologicalCocone'_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj tautologicalCocone'	—	—
tautologicalCocone'_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj CategoryTheory.Functor.obj CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.ι tautologicalCocone' CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
tautologicalCocone_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj tautologicalCocone	—	—
tautologicalCocone_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj CategoryTheory.Functor.obj CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.ι tautologicalCocone CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
uliftYonedaAdjunction_homEquiv_app 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category restrictedULiftYoneda DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv uliftYonedaAdjunction Opposite.unop CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.comp CategoryTheory.uliftYoneda CategoryTheory.Functor.map Opposite.op Equiv.symm CategoryTheory.uliftYonedaEquiv	—	CategoryTheory.Category.assoc CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv
uliftYonedaAdjunction_unit_app_app 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp restrictedULiftYoneda CategoryTheory.Adjunction.unit uliftYonedaAdjunction Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.CategoryStruct.comp CategoryTheory.uliftYoneda CategoryTheory.Functor.map DFunLike.coe Equiv Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.uliftYonedaEquiv	—	CategoryTheory.Adjunction.homEquiv_unit CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id uliftYonedaAdjunction_homEquiv_app

CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan

Definitions

Name	Category	Theorems
coconeApp 📖	CompOp	2 math math: coconeApp_naturality, coconeApp_naturality_assoc
extensionHom 📖	CompOp	—
natTrans 📖	CompOp	1 math math: natTrans_app_uliftYoneda_obj
presheafHom 📖	CompOp	4 math math: uliftYonedaEquiv_ι_presheafHom, presheafHom_naturality, uliftYonedaEquiv_presheafHom_uliftYoneda_obj, presheafHom_naturality_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coconeApp_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.uliftYoneda Opposite.unop CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Functor.map Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver Quiver.Hom coconeApp	—	Equiv.injective Equiv.apply_symm_apply CategoryTheory.NatTrans.naturality CategoryTheory.congr_app CategoryTheory.uliftYonedaEquiv_naturality CategoryTheory.Functor.map_comp CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
coconeApp_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.uliftYoneda Opposite.unop CategoryTheory.Functor.map Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver Quiver.Hom CategoryTheory.Functor.comp CategoryTheory.Functor.op coconeApp	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coconeApp_naturality
hom_ext 📖	—	CategoryTheory.Functor.HasLeftKanExtension Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.op	—	—	CategoryTheory.StructuredArrow.hom_ext CategoryTheory.NatTrans.ext' CategoryTheory.Functor.hom_ext_of_isLeftKanExtension CategoryTheory.Functor.instIsLeftKanExtensionObjLanAppLanUnit CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.NatTrans.naturality CategoryTheory.congr_app CategoryTheory.StructuredArrow.w CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.NatIso.hom_app_isIso Equiv.injective
hom_ext_iff 📖	—	CategoryTheory.Functor.HasLeftKanExtension Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.op	—	—	hom_ext
natTrans_app_uliftYoneda_obj 📖	mathematical	CategoryTheory.Functor.HasLeftKanExtension Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.op	CategoryTheory.NatTrans.app CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.lan CategoryTheory.Functor.op natTrans CategoryTheory.Functor.obj CategoryTheory.uliftYoneda CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan	—	CategoryTheory.Functor.hom_ext_of_isLeftKanExtension CategoryTheory.Functor.instIsLeftKanExtensionObjLanAppLanUnit CategoryTheory.Functor.descOfIsLeftKanExtension_fac Equiv.injective uliftYonedaEquiv_presheafHom_uliftYoneda_obj CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id
presheafHom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Functor.obj presheafHom CategoryTheory.Functor.whiskerLeft CategoryTheory.Functor.map	—	CategoryTheory.hom_ext_uliftYoneda Equiv.injective CategoryTheory.Category.assoc uliftYonedaEquiv_ι_presheafHom CategoryTheory.uliftYonedaEquiv_comp CategoryTheory.Functor.map_comp CategoryTheory.FunctorToTypes.comp
presheafHom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Functor.obj presheafHom CategoryTheory.Functor.whiskerLeft CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' presheafHom_naturality
uliftYonedaEquiv_presheafHom_uliftYoneda_obj 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.uliftYoneda CategoryTheory.Functor.comp CategoryTheory.Functor.op Opposite.op EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.uliftYonedaEquiv presheafHom CategoryTheory.NatTrans.app CategoryTheory.yoneda CategoryTheory.CategoryStruct.id Opposite.unop	—	CategoryTheory.Category.id_comp CategoryTheory.Functor.map_id uliftYonedaEquiv_ι_presheafHom
uliftYonedaEquiv_ι_presheafHom 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.uliftYoneda CategoryTheory.Functor.comp CategoryTheory.Functor.op Opposite.op EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.uliftYonedaEquiv CategoryTheory.CategoryStruct.comp presheafHom CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.yoneda CategoryTheory.CategoryStruct.id Opposite.unop	—	Equiv.surjective CategoryTheory.Limits.IsColimit.fac Equiv.apply_symm_apply

---

← Back to Index