Presheaf

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

Statistics

Metric	Count
Definitions flipFunctorToInterchange, functorToInterchange, functorToInterchangeIso, iso, isoAux	5
Theorems flipFunctorToInterchange_hom_app_app, flipFunctorToInterchange_inv_app_app, functorToInterchangeIso_hom_app_app, functorToInterchangeIso_inv_app_app, isIso_post, isoAux_hom_app, iso_hom, isFiltered_costructuredArrow_yoneda_iff_nonempty_preservesFiniteLimits, isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits, preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda	10
Total	15

CategoryTheory.Limits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isFiltered_costructuredArrow_yoneda_iff_nonempty_preservesFiniteLimits 📖	mathematical	—	CategoryTheory.IsFiltered CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow PreservesFiniteLimits	—	preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits
isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits 📖	mathematical	—	CategoryTheory.IsFiltered CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow	—	CategoryTheory.CategoryOfElements.instHasLimitsOfShapeElements UnivLE.small univLE_of_max UnivLE.self hasLimitsOfShape_of_hasFiniteLimits hasFiniteLimits_opposite PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.IsCofiltered.of_hasFiniteLimits CategoryTheory.IsFiltered.of_equivalence CategoryTheory.isFiltered_op_of_isCofiltered
preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda 📖	mathematical	—	PreservesFiniteLimits Opposite CategoryTheory.Category.opposite CategoryTheory.types	—	CategoryTheory.preservesLimit_of_isIso_post hasLimitOfHasLimitsOfShape hasLimitsOfShape_of_hasFiniteLimits hasFiniteLimits_opposite Types.hasLimit UnivLE.small univLE_of_max UnivLE.self PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isIso_post

CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux

Definitions

Name	Category	Theorems
flipFunctorToInterchange 📖	CompOp	2 math math: flipFunctorToInterchange_inv_app_app, flipFunctorToInterchange_hom_app_app
functorToInterchange 📖	CompOp	4 math math: functorToInterchangeIso_inv_app_app, functorToInterchangeIso_hom_app_app, flipFunctorToInterchange_inv_app_app, flipFunctorToInterchange_hom_app_app
functorToInterchangeIso 📖	CompOp	2 math math: functorToInterchangeIso_inv_app_app, functorToInterchangeIso_hom_app_app
iso 📖	CompOp	1 math math: iso_hom
isoAux 📖	CompOp	1 math math: isoAux_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
flipFunctorToInterchange_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.flip functorToInterchange CategoryTheory.Iso.hom CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj CategoryTheory.Functor.whiskeringLeft flipFunctorToInterchange	—	—
flipFunctorToInterchange_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.flip functorToInterchange CategoryTheory.Iso.inv CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj CategoryTheory.Functor.whiskeringLeft flipFunctorToInterchange	—	—
functorToInterchangeIso_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.obj functorToInterchange CategoryTheory.Iso.hom CategoryTheory.Functor.comp CategoryTheory.coyoneda CategoryTheory.Functor.whiskeringLeft CategoryTheory.CostructuredArrow.proj functorToInterchangeIso	—	—
functorToInterchangeIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.obj functorToInterchange CategoryTheory.Iso.inv CategoryTheory.Functor.comp CategoryTheory.coyoneda CategoryTheory.Functor.whiskeringLeft CategoryTheory.CostructuredArrow.proj functorToInterchangeIso	—	—
isIso_post 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.limit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_opposite CategoryTheory.Functor.comp CategoryTheory.Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.limit.post	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_opposite CategoryTheory.Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Iso.isIso_hom iso_hom
isoAux_hom_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.evaluation CategoryTheory.Limits.limit CategoryTheory.Iso.hom CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_opposite CategoryTheory.coyoneda CategoryTheory.Functor.whiskeringLeft isoAux CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Opposite.unop CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_opposite
iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.limit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_opposite CategoryTheory.Functor.comp CategoryTheory.Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self iso CategoryTheory.Limits.limit.post	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_opposite CategoryTheory.Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Category.assoc CategoryTheory.Iso.inv_comp_eq CategoryTheory.Limits.limit.hom_ext CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.HasLimit.isoOfNatIso_hom_π CategoryTheory.Limits.HasLimit.isoOfNatIso_hom_π_assoc CategoryTheory.Limits.limit.post_π CategoryTheory.Limits.functorCategoryHasColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.Types.hasColimitsOfShape CategoryTheory.Limits.hasColimitCompEvaluation CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_ι_inv_assoc CategoryTheory.Iso.app_inv CategoryTheory.NatTrans.comp_app_assoc CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv CategoryTheory.Presheaf.tautologicalCocone_ι_app CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom_assoc CategoryTheory.Limits.functorCategoryHasLimit CategoryTheory.Limits.ι_colimitLimitIso_limit_π_assoc isoAux_hom_app CategoryTheory.Limits.instHasLimitCompOfPreservesLimit CategoryTheory.preservesLimitIso_hom_π_assoc CategoryTheory.Iso.symm_hom CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom CategoryTheory.Limits.ι_colimitCompWhiskeringLeftIsoCompColimit_hom CategoryTheory.NatTrans.comp_app CategoryTheory.Functor.isoWhiskerLeft_hom CategoryTheory.Functor.whiskerLeft_comp CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom CategoryTheory.NatTrans.naturality CategoryTheory.types_ext CategoryTheory.Category.id_comp

---

← Back to Index