Documentation Verification Report

CompositionIso

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

Statistics

Metric	Count
Definitions `leftAdjointCompIso`, `leftAdjointCompNatTrans`, `leftAdjointIdIso`	3
Theorems `conjugateEquiv_leftAdjointCompIso_inv`, `conjugateEquiv_leftAdjointIdIso_hom`, `leftAdjointCompIso_assoc`, `leftAdjointCompIso_comp_id`, `leftAdjointCompIso_hom`, `leftAdjointCompIso_hom_app`, `leftAdjointCompIso_id_comp`, `leftAdjointCompIso_inv_app`, `leftAdjointCompNatTrans_app`, `leftAdjointCompNatTrans_assoc`, `leftAdjointCompNatTrans₀₁₃_eq_conjugateEquiv_symm`, `leftAdjointCompNatTrans₀₂₃_eq_conjugateEquiv_symm`, `leftAdjointIdIso_hom_app`, `leftAdjointIdIso_inv_app`	14
Total	17

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
`leftAdjointCompIso` 📖	CompOp	7 math math: `conjugateEquiv_leftAdjointCompIso_inv`, `leftAdjointCompIso_inv_app`, `leftAdjointCompIso_hom`, `leftAdjointCompIso_id_comp`, `leftAdjointCompIso_hom_app`, `leftAdjointCompIso_comp_id`, `leftAdjointCompIso_assoc`
`leftAdjointCompNatTrans` 📖	CompOp	5 math math: `leftAdjointCompNatTrans₀₁₃_eq_conjugateEquiv_symm`, `leftAdjointCompIso_hom`, `leftAdjointCompNatTrans₀₂₃_eq_conjugateEquiv_symm`, `leftAdjointCompNatTrans_assoc`, `leftAdjointCompNatTrans_app`
`leftAdjointIdIso` 📖	CompOp	5 math math: `conjugateEquiv_leftAdjointIdIso_hom`, `leftAdjointCompIso_id_comp`, `leftAdjointCompIso_comp_id`, `leftAdjointIdIso_inv_app`, `leftAdjointIdIso_hom_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conjugateEquiv_leftAdjointCompIso_inv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Functor` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.conjugateEquiv` `comp` `CategoryTheory.Iso.inv` `leftAdjointCompIso` `CategoryTheory.Iso.hom`	—	`Equiv.apply_symm_apply`
`conjugateEquiv_leftAdjointIdIso_hom` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Functor` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.conjugateEquiv` `id` `CategoryTheory.Iso.hom` `leftAdjointIdIso` `CategoryTheory.Iso.inv`	—	`Equiv.apply_symm_apply`
`leftAdjointCompIso_assoc` 📖	mathematical	`CategoryTheory.Iso.trans` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.isoWhiskerLeft` `CategoryTheory.Iso.symm` `CategoryTheory.Functor.associator` `CategoryTheory.Functor.isoWhiskerRight`	`leftAdjointCompIso`	—	`CategoryTheory.Iso.ext` `leftAdjointCompNatTrans_assoc` `CategoryTheory.Category.assoc`
`leftAdjointCompIso_comp_id` 📖	mathematical	`CategoryTheory.Iso.trans` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.Functor.isoWhiskerRight` `CategoryTheory.Functor.leftUnitor`	`leftAdjointCompIso` `CategoryTheory.Functor.isoWhiskerLeft` `leftAdjointIdIso` `CategoryTheory.Functor.rightUnitor`	—	`CategoryTheory.Iso.ext` `CategoryTheory.NatTrans.ext'` `leftAdjointCompIso_hom_app` `CategoryTheory.Category.id_comp` `counit_naturality` `left_triangle_components_assoc` `leftAdjointIdIso_hom_app` `CategoryTheory.Category.comp_id`
`leftAdjointCompIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `leftAdjointCompIso` `leftAdjointCompNatTrans` `CategoryTheory.Iso.inv`	—	—
`leftAdjointCompIso_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `leftAdjointCompIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.id` `unit` `CategoryTheory.Iso.inv` `counit`	—	`CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `comp_counit_app`
`leftAdjointCompIso_id_comp` 📖	mathematical	`CategoryTheory.Iso.trans` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.Functor.isoWhiskerLeft` `CategoryTheory.Functor.rightUnitor`	`leftAdjointCompIso` `CategoryTheory.Functor.isoWhiskerRight` `leftAdjointIdIso` `CategoryTheory.Functor.leftUnitor`	—	`CategoryTheory.Iso.ext` `CategoryTheory.NatTrans.ext'` `CategoryTheory.Functor.congr_map` `CategoryTheory.NatTrans.naturality` `leftAdjointCompIso_hom_app` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.Functor.map_comp` `left_triangle_components` `CategoryTheory.Category.comp_id` `leftAdjointIdIso_hom_app`
`leftAdjointCompIso_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `leftAdjointCompIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.id` `unit` `CategoryTheory.Iso.hom` `counit`	—	`comp_unit_app` `CategoryTheory.Functor.map_comp` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.assoc`
`leftAdjointCompNatTrans_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `leftAdjointCompNatTrans` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.id` `unit` `counit`	—	`CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `comp_counit_app`
`leftAdjointCompNatTrans_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.whiskerLeft` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.Iso.hom` `CategoryTheory.Functor.associator`	`leftAdjointCompNatTrans` `CategoryTheory.Iso.inv`	—	`leftAdjointCompNatTrans₀₁₃_eq_conjugateEquiv_symm` `leftAdjointCompNatTrans₀₂₃_eq_conjugateEquiv_symm` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Category.comp_id`
`leftAdjointCompNatTrans₀₁₃_eq_conjugateEquiv_symm` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.whiskerLeft` `leftAdjointCompNatTrans` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.conjugateEquiv` `comp` `CategoryTheory.Functor.whiskerRight`	—	`Equiv.surjective` `Equiv.injective` `Equiv.symm_apply_apply` `CategoryTheory.conjugateEquiv_whiskerLeft` `CategoryTheory.conjugateEquiv_comp`
`leftAdjointCompNatTrans₀₂₃_eq_conjugateEquiv_symm` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.inv` `CategoryTheory.Functor.associator` `CategoryTheory.Functor.whiskerRight` `leftAdjointCompNatTrans` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.conjugateEquiv` `comp` `CategoryTheory.Functor.whiskerLeft`	—	`Equiv.surjective` `Equiv.injective` `Equiv.symm_apply_apply` `Equiv.apply_symm_apply` `CategoryTheory.cancel_mono` `CategoryTheory.IsSplitMono.mono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id` `CategoryTheory.conjugateEquiv_associator_hom` `CategoryTheory.conjugateEquiv_whiskerRight` `CategoryTheory.conjugateEquiv_comp` `CategoryTheory.Iso.hom_inv_id_assoc`
`leftAdjointIdIso_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `leftAdjointIdIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `CategoryTheory.Functor.comp` `counit`	—	`CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`leftAdjointIdIso_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `leftAdjointIdIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `unit` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`

---

← Back to Index