Presheaf

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

Statistics

Metric	Count
Definitions coconeOfRepresentable, colimitOfRepresentable, compULiftYonedaIsoULiftYonedaCompLan, coconeApp, extensionHom, natTrans, presheafHom, functorToRepresentables, instUniqueHomLeftExtensionFunctorOppositeTypeUliftYonedaCompMkLanOpHomCompULiftYonedaIsoULiftYonedaCompLan, instUniqueHomLeftExtensionOppositeOpObjFunctorTypeUliftYonedaMkUliftYonedaMap, instUniqueHomLeftExtensionOppositeOpObjFunctorTypeYonedaMkYonedaMap, isColimitTautologicalCocone, isColimitTautologicalCocone', isExtensionAlongULiftYoneda, isExtensionAlongYoneda, restrictedULiftYoneda, restrictedULiftYonedaHomEquiv, restrictedULiftYonedaHomEquiv', restrictedYoneda, tautologicalCocone, tautologicalCocone', uliftYonedaAdjunction, uniqueExtensionAlongULiftYoneda, uniqueExtensionAlongYoneda, yonedaAdjunction	25
Theorems 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_along_yoneda_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	43
Total	68

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	—
isExtensionAlongYoneda 📖	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
restrictedYoneda 📖	CompOp	—
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	—
uniqueExtensionAlongYoneda 📖	CompOp	—
yonedaAdjunction 📖	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 CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.uliftYoneda CategoryTheory.Functor.lan 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.comp 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.comp	—	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.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 CategoryTheory.Functor.category CategoryTheory.Functor.lan 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.comp	—	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	—	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.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_along_yoneda_iff 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda	CategoryTheory.Functor.IsLeftKanExtension CategoryTheory.IsIso CategoryTheory.Functor.comp CategoryTheory.Limits.PreservesColimitsOfSize	—	isLeftKanExtension_along_uliftYoneda_iff
isLeftKanExtension_of_preservesColimits 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda	CategoryTheory.Functor.IsLeftKanExtension 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.leftKanExtension 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.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 CategoryTheory.Functor.obj 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.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 CategoryTheory.Functor.obj 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.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 CategoryTheory.Functor.category CategoryTheory.Functor.lan 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