Cat

📁 Source: Mathlib/CategoryTheory/Bicategory/Adjunction/Cat.lean

Statistics

Metric	Count
Definitions ofCat, toCat	2
Theorems ofCat_counit, ofCat_toCat, ofCat_unit, toCat_comp_toCat, toCat_counit_toNatTrans, toCat_ofCat, toCat_unit_toNatTrans, ofCat_comp, ofCat_id, toNatTrans_conjugateEquiv, toNatTrans_mateEquiv	11
Total	13

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
ofCat 📖	CompOp	8 math math: ofCat_counit, CategoryTheory.Bicategory.Adjunction.ofCat_id, CategoryTheory.Bicategory.Adjunction.ofCat_comp, toCat_ofCat, CategoryTheory.Bicategory.toNatTrans_mateEquiv, ofCat_toCat, ofCat_unit, CategoryTheory.Bicategory.toNatTrans_conjugateEquiv
toCat 📖	CompOp	6 math math: AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_adj, toCat_comp_toCat, toCat_counit_toNatTrans, toCat_ofCat, ofCat_toCat, toCat_unit_toNatTrans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofCat_counit 📖	mathematical	—	counit CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor ofCat CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.Adjunction.counit	—	—
ofCat_toCat 📖	mathematical	—	ofCat CategoryTheory.Cat.of CategoryTheory.Functor.toCatHom toCat	—	—
ofCat_unit 📖	mathematical	—	unit CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor ofCat CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.CategoryStruct.id CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Adjunction.unit	—	—
toCat_comp_toCat 📖	mathematical	—	CategoryTheory.Bicategory.Adjunction.comp CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.Cat.of CategoryTheory.Functor.toCatHom toCat CategoryTheory.Functor.comp comp	—	CategoryTheory.Bicategory.Adjunction.ext CategoryTheory.Cat.Hom₂.ext CategoryTheory.NatTrans.ext' CategoryTheory.Iso.refl_trans CategoryTheory.Bicategory.whiskerRight_comp CategoryTheory.Bicategory.id_whiskerRight CategoryTheory.Category.id_comp CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id comp_unit_app CategoryTheory.Iso.trans_refl CategoryTheory.Category.assoc comp_counit_app
toCat_counit_toNatTrans 📖	mathematical	—	CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Cat.of CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.Functor.toCatHom CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.Adjunction.counit toCat counit	—	—
toCat_ofCat 📖	mathematical	—	toCat CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor ofCat	—	—
toCat_unit_toNatTrans 📖	mathematical	—	CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Cat.of CategoryTheory.CategoryStruct.id CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.toCatHom CategoryTheory.Bicategory.Adjunction.unit toCat unit	—	—

CategoryTheory.Bicategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toNatTrans_conjugateEquiv 📖	mathematical	—	CategoryTheory.Cat.Hom₂.toNatTrans DFunLike.coe Equiv Quiver.Hom CategoryTheory.Cat CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.Category.toCategoryStruct homCategory EquivLike.toFunLike Equiv.instEquivLike conjugateEquiv CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Functor.category CategoryTheory.Cat.Hom.toFunctor CategoryTheory.conjugateEquiv CategoryTheory.Adjunction.ofCat	—	toNatTrans_mateEquiv CategoryTheory.NatTrans.ext' CategoryTheory.Functor.whiskerRight_comp CategoryTheory.Category.assoc CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
toNatTrans_mateEquiv 📖	mathematical	—	CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.CategoryStruct.comp CategoryTheory.Cat toCategoryStruct CategoryTheory.Cat.bicategory DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct homCategory EquivLike.toFunLike Equiv.instEquivLike mateEquiv CategoryTheory.TwoSquare CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.mateEquiv CategoryTheory.Adjunction.ofCat	—	CategoryTheory.NatTrans.ext' comp_whiskerLeft CategoryTheory.Category.assoc whiskerRight_comp CategoryTheory.Category.id_comp whiskerLeft_comp whiskerLeft_rightUnitor_inv pentagon_hom_inv_inv_inv_inv_assoc CategoryTheory.Functor.whiskerLeft_twice CategoryTheory.Functor.whiskerRight_twice CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id

CategoryTheory.Bicategory.Adjunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofCat_comp 📖	mathematical	—	CategoryTheory.Adjunction.ofCat CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory comp CategoryTheory.Adjunction.comp CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor	—	CategoryTheory.Adjunction.ext CategoryTheory.NatTrans.ext' CategoryTheory.Iso.refl_trans CategoryTheory.Bicategory.whiskerRight_comp CategoryTheory.Bicategory.id_whiskerRight CategoryTheory.Category.id_comp CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.Adjunction.comp_unit_app
ofCat_id 📖	mathematical	—	CategoryTheory.Adjunction.ofCat CategoryTheory.CategoryStruct.id CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory id CategoryTheory.Adjunction.id CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str	—	—

---

← Back to Index