Documentation Verification Report

Adjunction

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

Statistics

Metric	Count
Definitions	0
Theorems `hasCardinalFilteredGenerator`, `isCardinalAccessibleCategory`, `isCardinalFilteredGenerator`, `isCardinalLocallyPresentable`, `isCardinalPresentable_leftAdjoint_obj`, `hasCardinalFilteredGenerator`, `isAccessibleCategory`, `isCardinalAccessibleCategory`, `isCardinalLocallyPresentable`, `isLocallyPresentable`	10
Total	10

CategoryTheory.Adjunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasCardinalFilteredGenerator` 📖	mathematical	—	`CategoryTheory.HasCardinalFilteredGenerator`	—	`CategoryTheory.locallySmall_of_faithful` `CategoryTheory.HasCardinalFilteredGenerator.toLocallySmall` `CategoryTheory.HasCardinalFilteredGenerator.exists_generator` `CategoryTheory.ObjectProperty.instEssentiallySmallMap` `isCardinalFilteredGenerator`
`isCardinalAccessibleCategory` 📖	mathematical	—	`CategoryTheory.IsCardinalAccessibleCategory`	—	`hasCardinalFilteredGenerator` `CategoryTheory.IsCardinalAccessibleCategory.toHasCardinalFilteredGenerator` `CategoryTheory.hasColimitsOfShape_of_reflective` `CategoryTheory.HasCardinalFilteredColimits.hasColimitsOfShape` `CategoryTheory.IsCardinalAccessibleCategory.toHasCardinalFilteredColimits`
`isCardinalFilteredGenerator` 📖	mathematical	`CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator`	`CategoryTheory.ObjectProperty.map`	—	`CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.le_isCardinalPresentable` `CategoryTheory.isCardinalPresentable_iff` `isCardinalPresentable_leftAdjoint_obj` `CategoryTheory.isCardinalPresentable_of_iso` `isLeftAdjoint` `CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.exists_colimitsOfShape` `CategoryTheory.ObjectProperty.prop_of_isIso` `CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsColimitsOfShape` `instIsIsoAppCounitOfFullOfFaithful` `CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `CategoryTheory.ObjectProperty.prop_map_obj` `CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj`
`isCardinalLocallyPresentable` 📖	mathematical	—	`CategoryTheory.IsCardinalLocallyPresentable`	—	`hasCardinalFilteredGenerator` `CategoryTheory.IsCardinalAccessibleCategory.toHasCardinalFilteredGenerator` `CategoryTheory.instIsCardinalAccessibleCategoryOfIsCardinalLocallyPresentable` `CategoryTheory.hasColimits_of_reflective` `CategoryTheory.IsCardinalLocallyPresentable.toHasColimitsOfSize`
`isCardinalPresentable_leftAdjoint_obj` 📖	mathematical	—	`CategoryTheory.IsCardinalPresentable` `CategoryTheory.Functor.obj`	—	`CategoryTheory.isCardinalPresentable_iff_isCardinalAccessible_uliftCoyoneda_obj` `CategoryTheory.Functor.isCardinalAccessible_of_natIso` `CategoryTheory.Functor.instIsCardinalAccessibleComp` `CategoryTheory.instIsCardinalAccessibleObjOppositeFunctorTypeUliftCoyonedaOpOfIsCardinalPresentable`

CategoryTheory.Equivalence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasCardinalFilteredGenerator` 📖	mathematical	—	`CategoryTheory.HasCardinalFilteredGenerator`	—	`CategoryTheory.Adjunction.hasCardinalFilteredGenerator` `CategoryTheory.Functor.instIsCardinalAccessibleOfPreservesColimitsOfSize` `CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `isEquivalence_inverse` `full_inverse` `faithful_inverse`
`isAccessibleCategory` 📖	mathematical	—	`CategoryTheory.IsAccessibleCategory`	—	`CategoryTheory.IsAccessibleCategory.exists_cardinal` `isCardinalAccessibleCategory`
`isCardinalAccessibleCategory` 📖	mathematical	—	`CategoryTheory.IsCardinalAccessibleCategory`	—	`CategoryTheory.Adjunction.isCardinalAccessibleCategory` `CategoryTheory.Functor.instIsCardinalAccessibleOfPreservesColimitsOfSize` `CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `isEquivalence_inverse` `full_inverse` `faithful_inverse`
`isCardinalLocallyPresentable` 📖	mathematical	—	`CategoryTheory.IsCardinalLocallyPresentable`	—	`CategoryTheory.Adjunction.isCardinalLocallyPresentable` `CategoryTheory.Functor.instIsCardinalAccessibleOfPreservesColimitsOfSize` `CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `isEquivalence_inverse` `full_inverse` `faithful_inverse`
`isLocallyPresentable` 📖	mathematical	—	`CategoryTheory.IsLocallyPresentable`	—	`CategoryTheory.IsLocallyPresentable.exists_cardinal` `isCardinalLocallyPresentable`

---

← Back to Index