Presheaf

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

Statistics

Metric	Count
Definitions	0
Theorems instIsCardinalLocallyPresentableFunctorOppositeOfHasPullbacks, instIsCardinalPresentableFunctorOppositeFreeYonedaOfHasColimitsOfSize, instIsCardinalPresentableFunctorOppositeTypeObjUliftYonedaOfHasColimitsOfSize, instIsLocallyPresentableFunctorOppositeOfHasPullbacks, isStrongGenerator	5
Total	5

CategoryTheory.Presheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsCardinalLocallyPresentableFunctorOppositeOfHasPullbacks 📖	mathematical	—	CategoryTheory.IsCardinalLocallyPresentable CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category	—	CategoryTheory.IsCardinalLocallyPresentable.iff_exists_isStrongGenerator CategoryTheory.IsCardinalLocallyPresentable.toHasColimitsOfSize CategoryTheory.HasCardinalFilteredGenerator.toLocallySmall CategoryTheory.IsCardinalAccessibleCategory.toHasCardinalFilteredGenerator CategoryTheory.instIsCardinalAccessibleCategoryOfIsCardinalLocallyPresentable CategoryTheory.Limits.functorCategoryHasColimitsOfSize CategoryTheory.instLocallySmallFunctor CategoryTheory.Limits.hasCoproductsOfShape_of_hasCoproducts CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.ObjectProperty.instSmallOfObjOfSmall small_prod UnivLE.small UnivLE.self isStrongGenerator CategoryTheory.isCardinalPresentable_iff instIsCardinalPresentableFunctorOppositeFreeYonedaOfHasColimitsOfSize
instIsCardinalPresentableFunctorOppositeFreeYonedaOfHasColimitsOfSize 📖	mathematical	CategoryTheory.Limits.HasCoproducts	CategoryTheory.IsCardinalPresentable CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category freeYoneda	—	CategoryTheory.types_ext ULift.ext freeYonedaHomEquiv_comp CategoryTheory.preservesColimitsOfShape_of_isCardinalPresentable CategoryTheory.Limits.preservesColimitsOfShape_of_natIso CategoryTheory.Limits.comp_preservesColimitsOfShape CategoryTheory.Limits.evaluation_preservesColimitsOfShape CategoryTheory.HasCardinalFilteredColimits.hasColimitsOfShape CategoryTheory.instHasCardinalFilteredColimitsOfHasColimitsOfSize CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Limits.Types.instPreservesColimitsOfSizeUliftFunctor
instIsCardinalPresentableFunctorOppositeTypeObjUliftYonedaOfHasColimitsOfSize 📖	mathematical	—	CategoryTheory.IsCardinalPresentable CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.uliftYoneda	—	CategoryTheory.Limits.preservesColimitsOfShape_of_natIso CategoryTheory.Limits.comp_preservesColimitsOfShape CategoryTheory.Limits.evaluation_preservesColimitsOfShape CategoryTheory.HasCardinalFilteredColimits.hasColimitsOfShape CategoryTheory.instHasCardinalFilteredColimitsOfHasColimitsOfSize CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Limits.Types.instPreservesColimitsOfSizeUliftFunctor
instIsLocallyPresentableFunctorOppositeOfHasPullbacks 📖	mathematical	—	CategoryTheory.IsLocallyPresentable CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category	—	CategoryTheory.IsLocallyPresentable.exists_cardinal instIsCardinalLocallyPresentableFunctorOppositeOfHasPullbacks
isStrongGenerator 📖	mathematical	CategoryTheory.ObjectProperty.IsStrongGenerator CategoryTheory.Limits.HasCoproducts	CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.ObjectProperty.ofObj CategoryTheory.Category.toCategoryStruct freeYoneda	—	CategoryTheory.ObjectProperty.isStrongGenerator_iff isSeparating CategoryTheory.ObjectProperty.ofObj_subtypeVal CategoryTheory.NatTrans.isIso_iff_isIso_app CategoryTheory.instMonoAppOfFunctor Equiv.surjective CategoryTheory.ObjectProperty.ofObj_apply freeYonedaHomEquiv_comp

---

← Back to Index