Documentation Verification Report

Adjunction

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

Statistics

Metric	Count
Definitions `leftAdjointLiftStructEquiv`, `rightAdjointLiftStructEquiv`	2
Theorems `hasLiftingProperty_iff`, `instHasLift`, `instHasLift_1`, `left_adjoint`, `left_adjoint_hasLift_iff`, `right_adjoint`, `right_adjoint_hasLift_iff`	7
Total	9

CategoryTheory.Adjunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasLiftingProperty_iff` 📖	mathematical	—	`CategoryTheory.HasLiftingProperty` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	`CategoryTheory.CommSq.left_adjoint` `CategoryTheory.CommSq.left_adjoint_hasLift_iff` `CategoryTheory.sq_hasLift_of_hasLiftingProperty` `CategoryTheory.CommSq.right_adjoint` `CategoryTheory.CommSq.right_adjoint_hasLift_iff`

CategoryTheory.CommSq

Definitions

Name	Category	Theorems
`leftAdjointLiftStructEquiv` 📖	CompOp	—
`rightAdjointLiftStructEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasLift` 📖	mathematical	`CategoryTheory.CommSq` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	`HasLift` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.Adjunction.homEquiv` `right_adjoint`	—	`right_adjoint` `right_adjoint_hasLift_iff`
`instHasLift_1` 📖	mathematical	`CategoryTheory.CommSq` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	`HasLift` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.Adjunction.homEquiv` `left_adjoint`	—	`left_adjoint` `left_adjoint_hasLift_iff`
`left_adjoint` 📖	mathematical	`CategoryTheory.CommSq` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.Adjunction.homEquiv`	—	`CategoryTheory.Adjunction.homEquiv_counit` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp_assoc` `w` `CategoryTheory.Functor.map_comp` `CategoryTheory.Adjunction.counit_naturality`
`left_adjoint_hasLift_iff` 📖	mathematical	`CategoryTheory.CommSq` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	`HasLift` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.Adjunction.homEquiv` `left_adjoint`	—	`left_adjoint` `Equiv.nonempty_congr`
`right_adjoint` 📖	mathematical	`CategoryTheory.CommSq` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.Adjunction.homEquiv`	—	`CategoryTheory.Adjunction.homEquiv_unit` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `w` `CategoryTheory.Adjunction.unit_naturality_assoc`
`right_adjoint_hasLift_iff` 📖	mathematical	`CategoryTheory.CommSq` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	`HasLift` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.Adjunction.homEquiv` `right_adjoint`	—	`right_adjoint` `Equiv.nonempty_congr`

---

← Back to Index