Unique

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

Statistics

Metric	Count
Definitions leftAdjointUniq, rightAdjointUniq	2
Theorems homEquiv_leftAdjointUniq_hom_app, homEquiv_symm_rightAdjointUniq_hom_app, leftAdjointUniq_hom_app_counit, leftAdjointUniq_hom_app_counit_assoc, leftAdjointUniq_hom_counit, leftAdjointUniq_hom_counit_assoc, leftAdjointUniq_inv_app, leftAdjointUniq_refl, leftAdjointUniq_trans, leftAdjointUniq_trans_app, leftAdjointUniq_trans_app_assoc, leftAdjointUniq_trans_assoc, rightAdjointUniq_hom_app_counit, rightAdjointUniq_hom_app_counit_assoc, rightAdjointUniq_hom_counit, rightAdjointUniq_hom_counit_assoc, rightAdjointUniq_inv_app, rightAdjointUniq_refl, rightAdjointUniq_trans, rightAdjointUniq_trans_app, rightAdjointUniq_trans_app_assoc, rightAdjointUniq_trans_assoc, unit_leftAdjointUniq_hom, unit_leftAdjointUniq_hom_app, unit_leftAdjointUniq_hom_app_assoc, unit_leftAdjointUniq_hom_assoc, unit_rightAdjointUniq_hom, unit_rightAdjointUniq_hom_app, unit_rightAdjointUniq_hom_app_assoc, unit_rightAdjointUniq_hom_assoc	30
Total	32

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
leftAdjointUniq 📖	CompOp	15 math math: leftAdjointUniq_refl, leftAdjointUniq_hom_app_counit_assoc, leftAdjointUniq_trans_app_assoc, leftAdjointUniq_hom_counit, leftAdjointUniq_hom_app_counit, leftAdjointUniq_trans_assoc, leftAdjointUniq_trans_app, unit_leftAdjointUniq_hom_assoc, leftAdjointUniq_hom_counit_assoc, unit_leftAdjointUniq_hom_app_assoc, leftAdjointUniq_inv_app, unit_leftAdjointUniq_hom, leftAdjointUniq_trans, homEquiv_leftAdjointUniq_hom_app, unit_leftAdjointUniq_hom_app
rightAdjointUniq 📖	CompOp	15 math math: rightAdjointUniq_trans, unit_rightAdjointUniq_hom, unit_rightAdjointUniq_hom_app, rightAdjointUniq_trans_app_assoc, rightAdjointUniq_hom_counit_assoc, rightAdjointUniq_hom_counit, rightAdjointUniq_trans_app, rightAdjointUniq_hom_app_counit, rightAdjointUniq_trans_assoc, rightAdjointUniq_hom_app_counit_assoc, unit_rightAdjointUniq_hom_assoc, rightAdjointUniq_refl, homEquiv_symm_rightAdjointUniq_hom_app, unit_rightAdjointUniq_hom_app_assoc, rightAdjointUniq_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homEquiv_leftAdjointUniq_hom_app 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category leftAdjointUniq CategoryTheory.Functor.id CategoryTheory.Functor.comp unit	—	CategoryTheory.conjugateEquiv_symm_apply_app CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp homEquiv_unit CategoryTheory.Functor.map_comp unit_naturality_assoc right_triangle_components CategoryTheory.Category.comp_id
homEquiv_symm_rightAdjointUniq_hom_app 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category rightAdjointUniq CategoryTheory.Functor.comp CategoryTheory.Functor.id counit	—	CategoryTheory.conjugateEquiv_apply_app CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp homEquiv_counit CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc counit_naturality left_triangle_components_assoc
leftAdjointUniq_hom_app_counit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category leftAdjointUniq CategoryTheory.Functor.comp counit	—	leftAdjointUniq_hom_counit
leftAdjointUniq_hom_app_counit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category leftAdjointUniq CategoryTheory.Functor.comp CategoryTheory.Functor.id counit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftAdjointUniq_hom_app_counit
leftAdjointUniq_hom_counit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom leftAdjointUniq counit	—	CategoryTheory.NatTrans.ext' CategoryTheory.conjugateEquiv_symm_apply_app CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.Category.assoc counit_naturality CategoryTheory.Functor.map_comp right_triangle_components
leftAdjointUniq_hom_counit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom leftAdjointUniq CategoryTheory.Functor.id counit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftAdjointUniq_hom_counit
leftAdjointUniq_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category leftAdjointUniq CategoryTheory.Iso.hom	—	—
leftAdjointUniq_refl 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category leftAdjointUniq CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.conjugateEquiv_symm_id
leftAdjointUniq_trans 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Iso.hom leftAdjointUniq	—	CategoryTheory.conjugateEquiv_symm_comp CategoryTheory.Category.comp_id
leftAdjointUniq_trans_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category leftAdjointUniq	—	leftAdjointUniq_trans
leftAdjointUniq_trans_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category leftAdjointUniq	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftAdjointUniq_trans_app
leftAdjointUniq_trans_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Iso.hom leftAdjointUniq	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftAdjointUniq_trans
rightAdjointUniq_hom_app_counit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category rightAdjointUniq CategoryTheory.Functor.comp counit	—	CategoryTheory.conjugateEquiv_apply_app CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc counit_naturality left_triangle_components_assoc
rightAdjointUniq_hom_app_counit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category rightAdjointUniq CategoryTheory.Functor.comp CategoryTheory.Functor.id counit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightAdjointUniq_hom_app_counit
rightAdjointUniq_hom_counit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom rightAdjointUniq counit	—	CategoryTheory.NatTrans.ext' rightAdjointUniq_hom_app_counit
rightAdjointUniq_hom_counit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom rightAdjointUniq CategoryTheory.Functor.id counit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightAdjointUniq_hom_counit
rightAdjointUniq_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category rightAdjointUniq CategoryTheory.Iso.hom	—	—
rightAdjointUniq_refl 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category rightAdjointUniq CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.conjugateEquiv_id
rightAdjointUniq_trans 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Iso.hom rightAdjointUniq	—	CategoryTheory.conjugateEquiv_comp CategoryTheory.Category.comp_id
rightAdjointUniq_trans_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category rightAdjointUniq	—	rightAdjointUniq_trans
rightAdjointUniq_trans_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category rightAdjointUniq	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightAdjointUniq_trans_app
rightAdjointUniq_trans_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Iso.hom rightAdjointUniq	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightAdjointUniq_trans
unit_leftAdjointUniq_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp unit CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom leftAdjointUniq	—	CategoryTheory.NatTrans.ext' CategoryTheory.NatTrans.comp_app homEquiv_leftAdjointUniq_hom_app homEquiv_unit
unit_leftAdjointUniq_hom_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.app unit CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category leftAdjointUniq	—	unit_leftAdjointUniq_hom
unit_leftAdjointUniq_hom_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category leftAdjointUniq	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_leftAdjointUniq_hom_app
unit_leftAdjointUniq_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp unit CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom leftAdjointUniq	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_leftAdjointUniq_hom
unit_rightAdjointUniq_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp unit CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom rightAdjointUniq	—	CategoryTheory.NatTrans.ext' unit_rightAdjointUniq_hom_app
unit_rightAdjointUniq_hom_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.app unit CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category rightAdjointUniq	—	CategoryTheory.conjugateEquiv_apply_app CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp unit_naturality_assoc CategoryTheory.Functor.map_comp left_triangle_components CategoryTheory.Category.comp_id
unit_rightAdjointUniq_hom_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category rightAdjointUniq	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_rightAdjointUniq_hom_app
unit_rightAdjointUniq_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp unit CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom rightAdjointUniq	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_rightAdjointUniq_hom

---

← Back to Index