Documentation Verification Report

AdjointFunctorTheorems

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

Statistics

Metric	Count
Definitions `SolutionSetCondition`	1
Theorems `hasColimits_of_hasLimits_of_hasCoseparator`, `hasColimits_of_hasLimits_of_isCoseparating`, `hasLimits_of_hasColimits_of_hasSeparator`, `hasLimits_of_hasColimits_of_isSeparating`, `isLeftAdjoint_of_preservesColimits_of_isSeparating`, `isRightAdjoint_of_preservesLimits_of_isCoseparating`, `isRightAdjoint_of_preservesLimits_of_solutionSetCondition`, `solutionSetCondition_of_isRightAdjoint`	8
Total	9

CategoryTheory

Definitions

Name	Category	Theorems
`SolutionSetCondition` 📖	MathDef	1 math math: `solutionSetCondition_of_isRightAdjoint`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLeftAdjoint_of_preservesColimits_of_isSeparating` 📖	mathematical	`ObjectProperty.IsSeparating`	`Functor.IsLeftAdjoint`	—	`instLocallySmallOpposite` `locallySmall_of_univLE` `UnivLE.self` `hasTerminal_of_isSeparating` `CostructuredArrow.locallySmall` `CostructuredArrow.well_copowered_costructuredArrow` `Limits.hasFiniteColimits_of_hasColimits` `Limits.PreservesColimits.preservesFiniteColimits` `CostructuredArrow.hasColimitsOfSize` `CostructuredArrow.small_inverseImage_proj_of_locallySmall` `CostructuredArrow.isSeparating_inverseImage_proj` `isLeftAdjoint_of_costructuredArrowTerminals`
`isRightAdjoint_of_preservesLimits_of_isCoseparating` 📖	mathematical	`ObjectProperty.IsCoseparating`	`Functor.IsRightAdjoint`	—	`locallySmall_of_univLE` `UnivLE.self` `hasInitial_of_isCoseparating` `StructuredArrow.locallySmall` `StructuredArrow.wellPowered_structuredArrow` `Limits.hasFiniteLimits_of_hasLimits` `Limits.PreservesLimits.preservesFiniteLimits` `StructuredArrow.hasLimitsOfSize` `StructuredArrow.small_inverseImage_proj_of_locallySmall` `StructuredArrow.isCoseparating_inverseImage_proj` `isRightAdjointOfStructuredArrowInitials`
`isRightAdjoint_of_preservesLimits_of_solutionSetCondition` 📖	mathematical	`SolutionSetCondition`	`Functor.IsRightAdjoint`	—	`isRightAdjointOfStructuredArrowInitials` `has_weakly_initial_of_weakly_initial_set_and_hasProducts` `StructuredArrow.hasLimitsOfShape` `Limits.hasProductsOfShape_of_hasProducts` `Limits.hasLimitsOfShapeOfHasLimits` `Limits.PreservesLimitsOfSize.preservesLimitsOfShape` `hasInitial_of_weakly_initial_and_hasWideEqualizers`
`solutionSetCondition_of_isRightAdjoint` 📖	mathematical	—	`SolutionSetCondition`	—	`Adjunction.homEquiv_unit` `Equiv.apply_symm_apply`

CategoryTheory.Limits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasColimits_of_hasLimits_of_hasCoseparator` 📖	mathematical	—	`HasColimits`	—	`CategoryTheory.locallySmall_of_univLE` `UnivLE.self` `hasColimits_of_hasLimits_of_isCoseparating` `CategoryTheory.ObjectProperty.instSmallOfObjOfSmall` `UnivLE.small` `univLE_of_max` `CategoryTheory.isCoseparator_coseparator`
`hasColimits_of_hasLimits_of_isCoseparating` 📖	mathematical	`CategoryTheory.ObjectProperty.IsCoseparating`	`HasColimits`	—	`CategoryTheory.locallySmall_of_univLE` `UnivLE.self` `hasColimitsOfShape_iff_isRightAdjoint_const` `CategoryTheory.isRightAdjoint_of_preservesLimits_of_isCoseparating` `preservesLimits_const`
`hasLimits_of_hasColimits_of_hasSeparator` 📖	mathematical	—	`HasLimits`	—	`CategoryTheory.instLocallySmallOpposite` `CategoryTheory.locallySmall_of_univLE` `UnivLE.self` `hasLimits_of_hasColimits_of_isSeparating` `CategoryTheory.ObjectProperty.instSmallOfObjOfSmall` `UnivLE.small` `univLE_of_max` `CategoryTheory.isSeparator_separator`
`hasLimits_of_hasColimits_of_isSeparating` 📖	mathematical	`CategoryTheory.ObjectProperty.IsSeparating`	`HasLimits`	—	`CategoryTheory.instLocallySmallOpposite` `CategoryTheory.locallySmall_of_univLE` `UnivLE.self` `hasLimitsOfShape_iff_isLeftAdjoint_const` `CategoryTheory.isLeftAdjoint_of_preservesColimits_of_isSeparating` `preservesColimits_const`

---

← Back to Index