Documentation Verification Report

Right

📁 Source: Mathlib/CategoryTheory/Adjunction/Lifting/Right.lean

Statistics

Metric	Count
Definitions `constructRightAdjoint`, `constructRightAdjointEquiv`, `constructRightAdjointObj`, `otherMap`, `unitEqualises`	5
Theorems `constructRightAdjointEquiv_apply`, `constructRightAdjointEquiv_symm_apply`, `instIsCoreflexivePairMapAppUnitOtherMap`, `isLeftAdjoint_square_lift`, `isLeftAdjoint_square_lift_comonadic`, `isLeftAdjoint_triangle_lift`, `isLeftAdjoint_triangle_lift_comonadic`	7
Total	12

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLeftAdjoint_square_lift` 📖	mathematical	—	`Functor.IsLeftAdjoint`	—	`Adjunction.isLeftAdjoint` `Functor.isLeftAdjoint_comp` `isLeftAdjoint_triangle_lift`
`isLeftAdjoint_square_lift_comonadic` 📖	mathematical	—	`Functor.IsLeftAdjoint`	—	`Adjunction.isLeftAdjoint` `Functor.isLeftAdjoint_comp` `isLeftAdjoint_triangle_lift_comonadic`
`isLeftAdjoint_triangle_lift` 📖	mathematical	—	`Functor.IsLeftAdjoint`	—	—
`isLeftAdjoint_triangle_lift_comonadic` 📖	mathematical	—	`Functor.IsLeftAdjoint`	—	`instIsEquivalenceCoalgebraToComonadComonadicAdjunctionComparison` `Functor.isLeftAdjoint_comp` `Adjunction.isLeftAdjoint` `Functor.map_id` `Category.comp_id` `Comonad.adj_unit` `Comonad.CofreeEqualizer.condition` `isLeftAdjoint_triangle_lift` `Functor.isLeftAdjoint_of_isEquivalence` `Functor.isEquivalence_inv`

CategoryTheory.LiftRightAdjoint

Definitions

Name	Category	Theorems
`constructRightAdjoint` 📖	CompOp	—
`constructRightAdjointEquiv` 📖	CompOp	2 math math: `constructRightAdjointEquiv_apply`, `constructRightAdjointEquiv_symm_apply`
`constructRightAdjointObj` 📖	CompOp	2 math math: `constructRightAdjointEquiv_apply`, `constructRightAdjointEquiv_symm_apply`
`otherMap` 📖	CompOp	3 math math: `constructRightAdjointEquiv_apply`, `constructRightAdjointEquiv_symm_apply`, `instIsCoreflexivePairMapAppUnitOtherMap`
`unitEqualises` 📖	CompOp	2 math math: `constructRightAdjointEquiv_apply`, `constructRightAdjointEquiv_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`constructRightAdjointEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `constructRightAdjointObj` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `constructRightAdjointEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Adjunction.unit` `Equiv.symm` `CategoryTheory.Limits.Fork.IsLimit.homIso` `CategoryTheory.Limits.Fork.ofι` `unitEqualises` `CategoryTheory.Adjunction.homEquiv` `otherMap` `CategoryTheory.Limits.limit.cone` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Limits.limit.isLimit`	—	—
`constructRightAdjointEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `constructRightAdjointObj` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `constructRightAdjointEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Adjunction.unit` `otherMap` `CategoryTheory.Limits.Fork.IsLimit.homIso` `CategoryTheory.Limits.limit.cone` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Limits.limit.isLimit` `CategoryTheory.Adjunction.homEquiv` `CategoryTheory.Limits.Fork.ofι` `unitEqualises`	—	—
`instIsCoreflexivePairMapAppUnitOtherMap` 📖	mathematical	—	`CategoryTheory.IsCoreflexivePair` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.unit` `otherMap`	—	`CategoryTheory.IsCoreflexivePair.mk'` `CategoryTheory.Adjunction.left_triangle_components` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `CategoryTheory.Adjunction.counit_naturality` `CategoryTheory.Adjunction.left_triangle_components_assoc` `CategoryTheory.Adjunction.right_triangle_components`

---

← Back to Index