Documentation Verification Report

Parametrized

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

Statistics

Metric	Count
Definitions `adj`, `homEquiv`, `mk'`, `«term_⊣₂_»`	4
Theorems `homEquiv_eq`, `homEquiv_naturality_one`, `homEquiv_naturality_one_assoc`, `homEquiv_naturality_three`, `homEquiv_naturality_three_assoc`, `homEquiv_naturality_two`, `homEquiv_naturality_two_assoc`, `homEquiv_symm_naturality_one`, `homEquiv_symm_naturality_one_assoc`, `homEquiv_symm_naturality_three`, `homEquiv_symm_naturality_three_assoc`, `homEquiv_symm_naturality_two`, `homEquiv_symm_naturality_two_assoc`, `mk'_adj`, `unit_whiskerRight_map`, `unit_whiskerRight_map_assoc`, `whiskerLeft_map_counit`, `whiskerLeft_map_counit_assoc`	18
Total	22

CategoryTheory

Definitions

Name	Category	Theorems
`«term_⊣₂_»` 📖	CompOp	—

CategoryTheory.ParametrizedAdjunction

Definitions

Name	Category	Theorems
`adj` 📖	CompOp	8 math math: `mk'_adj`, `CategoryTheory.MonoidalClosed.internalHomAdjunction₂_adj`, `whiskerLeft_map_counit`, `CategoryTheory.Functor.leibnizAdjunction_adj`, `unit_whiskerRight_map_assoc`, `unit_whiskerRight_map`, `homEquiv_eq`, `whiskerLeft_map_counit_assoc`
`homEquiv` 📖	CompOp	27 math math: `homEquiv_symm_naturality_three_assoc`, `homEquiv_naturality_two`, `inr_arrowHomEquiv_symm_apply_left`, `inl_arrowHomEquiv_symm_apply_left`, `homEquiv_symm_naturality_one`, `CategoryTheory.Functor.LeibnizAdjunction.adj_unit_app_left`, `arrowHomEquiv_apply_left`, `CategoryTheory.Functor.LeibnizAdjunction.adj_counit_app_left`, `arrowHomEquiv_apply_right_snd`, `arrowHomEquiv_symm_apply_right`, `homEquiv_symm_naturality_one_assoc`, `homEquiv_symm_naturality_three`, `inr_arrowHomEquiv_symm_apply_left_assoc`, `CategoryTheory.Functor.LeibnizAdjunction.adj_counit_app_right`, `homEquiv_symm_naturality_two`, `arrowHomEquiv_apply_right_fst_assoc`, `homEquiv_naturality_three`, `homEquiv_symm_naturality_two_assoc`, `inl_arrowHomEquiv_symm_apply_left_assoc`, `arrowHomEquiv_apply_right_fst`, `CategoryTheory.Functor.LeibnizAdjunction.adj_unit_app_right`, `homEquiv_naturality_one`, `homEquiv_eq`, `homEquiv_naturality_one_assoc`, `homEquiv_naturality_two_assoc`, `homEquiv_naturality_three_assoc`, `arrowHomEquiv_apply_right_snd_assoc`
`mk'` 📖	CompOp	1 math math: `mk'_adj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homEquiv_eq` 📖	mathematical	—	`homEquiv` `CategoryTheory.Adjunction.homEquiv` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `adj`	—	—
`homEquiv_naturality_one` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.map` `Quiver.Hom.op`	—	`CategoryTheory.NatTrans.congr_app` `unit_whiskerRight_map` `CategoryTheory.Adjunction.homEquiv_unit` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.NatTrans.naturality`
`homEquiv_naturality_one_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Opposite.op` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquiv` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.map` `Quiver.Hom.op`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homEquiv_naturality_one`
`homEquiv_naturality_three` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.map`	—	`CategoryTheory.Adjunction.homEquiv_naturality_right`
`homEquiv_naturality_three_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Opposite.op` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquiv` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homEquiv_naturality_three`
`homEquiv_naturality_two` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.map`	—	`CategoryTheory.Adjunction.homEquiv_naturality_left`
`homEquiv_naturality_two_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Opposite.op` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquiv` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homEquiv_naturality_two`
`homEquiv_symm_naturality_one` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `homEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.map` `Quiver.Hom.op`	—	`Equiv.injective` `Equiv.apply_symm_apply` `homEquiv_naturality_one`
`homEquiv_symm_naturality_one_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `homEquiv` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.map` `Quiver.Hom.op`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homEquiv_symm_naturality_one`
`homEquiv_symm_naturality_three` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `homEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.map`	—	`Equiv.injective` `Equiv.apply_symm_apply` `homEquiv_naturality_three`
`homEquiv_symm_naturality_three_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `homEquiv` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homEquiv_symm_naturality_three`
`homEquiv_symm_naturality_two` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `homEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.map`	—	`Equiv.injective` `Equiv.apply_symm_apply` `homEquiv_naturality_two`
`homEquiv_symm_naturality_two_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `homEquiv` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homEquiv_symm_naturality_two`
`mk'_adj` 📖	mathematical	—	`adj` `mk'`	—	—
`unit_whiskerRight_map` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Adjunction.unit` `adj` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.Functor.map` `CategoryTheory.Functor.whiskerLeft` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver`	—	—
`unit_whiskerRight_map_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Adjunction.unit` `adj` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.Functor.map` `CategoryTheory.Functor.whiskerLeft` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `unit_whiskerRight_map`
`whiskerLeft_map_counit` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Functor.id` `CategoryTheory.Functor.whiskerLeft` `CategoryTheory.Functor.map` `CategoryTheory.Adjunction.counit` `adj` `CategoryTheory.Functor.whiskerRight` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver`	—	`CategoryTheory.NatTrans.ext'` `Equiv.injective` `homEquiv_naturality_one` `homEquiv_naturality_two` `CategoryTheory.Adjunction.homEquiv_unit` `CategoryTheory.Adjunction.right_triangle_components` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id`
`whiskerLeft_map_counit_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Functor.whiskerLeft` `CategoryTheory.Functor.map` `CategoryTheory.Functor.id` `CategoryTheory.Adjunction.counit` `adj` `CategoryTheory.Functor.whiskerRight` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `whiskerLeft_map_counit`

---

← Back to Index