Documentation Verification Report

Adjunction

📁 Source: Mathlib/CategoryTheory/Functor/Derived/Adjunction.lean

Statistics

Metric	Count
Definitions `derived`, `derived'`, `derivedε`, `derivedη`	4
Theorems `derived'_counit`, `derived'_unit`, `derived_counit`, `derived_unit`, `derivedε_fac_app`, `derivedε_fac_app_assoc`, `derivedη_fac_app`, `derivedη_fac_app_assoc`	8
Total	12

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
`derived` 📖	CompOp	2 math math: `derived_counit`, `derived_unit`
`derived'` 📖	CompOp	2 math math: `derived'_unit`, `derived'_counit`
`derivedε` 📖	CompOp	3 math math: `derivedε_fac_app_assoc`, `derived_counit`, `derivedε_fac_app`
`derivedη` 📖	CompOp	3 math math: `derived_unit`, `derivedη_fac_app`, `derivedη_fac_app_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`derived'_counit` 📖	mathematical	—	`counit` `derived'`	—	—
`derived'_unit` 📖	mathematical	—	`unit` `derived'`	—	—
`derived_counit` 📖	mathematical	—	`counit` `derived` `derivedε`	—	—
`derived_unit` 📖	mathematical	—	`unit` `derived` `derivedη`	—	—
`derivedε_fac_app` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `derivedε` `counit`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Functor.rightDerived_fac_app`
`derivedε_fac_app_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `derivedε` `counit`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `derivedε_fac_app`
`derivedη_fac_app` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app` `derivedη` `CategoryTheory.Functor.map` `unit`	—	`CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id` `CategoryTheory.Functor.leftDerived_fac_app`
`derivedη_fac_app_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `derivedη` `CategoryTheory.Functor.map` `unit`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `derivedη_fac_app`

---

← Back to Index