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, counit_naturality, counit_naturality_assoc, left_triangle_components, left_triangle_components_assoc, right_triangle_components, right_triangle_components_assoc, unit_naturality, unit_naturality_assoc, ofCat_comp, ofCat_id, toNatTrans_conjugateEquiv, toNatTrans_mateEquiv	19
Total	21

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
ofCat 📖	CompOp	21 math math: CategoryTheory.Pseudofunctor.isEquivalence_toDescentDataAsCoalgebra_iff_isEquivalence_comonadComparison, CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_obj_hom, ofCat_counit, CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_inv_app_f, CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_unitIso_inv_app_hom, CategoryTheory.Bicategory.Adjunction.ofCat_id, CategoryTheory.Bicategory.Adjunction.ofCat_comp, CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_functor_obj_a, CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_map_hom, CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_counitIso_hom_app_f, toCat_ofCat, CategoryTheory.Bicategory.toNatTrans_mateEquiv, CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_hom_app_f, CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_unitIso_hom_app_hom, CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_obj_obj, ofCat_toCat, CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_functor_map_f, ofCat_unit, CategoryTheory.Bicategory.toNatTrans_conjugateEquiv, CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_functor_obj_A, CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_counitIso_inv_app_f
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.Adj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
counit_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category obj CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Hom.l Hom.r CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Bicategory.Adjunction.counit Hom.adj	—	CategoryTheory.Adjunction.counit_naturality
counit_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category obj CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Hom.l Hom.r CategoryTheory.Functor.map CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Bicategory.Adjunction.counit Hom.adj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' counit_naturality
left_triangle_components 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category obj CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Hom.l CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.toCategoryStruct Hom.r CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Bicategory.Adjunction.unit Hom.adj CategoryTheory.Bicategory.Adjunction.counit	—	CategoryTheory.Adjunction.left_triangle_components
left_triangle_components_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category obj CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Hom.l CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.toCategoryStruct Hom.r CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Bicategory.Adjunction.unit Hom.adj CategoryTheory.Bicategory.Adjunction.counit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' left_triangle_components
right_triangle_components 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category obj CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.toCategoryStruct Hom.r Hom.l CategoryTheory.NatTrans.app CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Bicategory.Adjunction.unit Hom.adj CategoryTheory.Functor.map CategoryTheory.Bicategory.Adjunction.counit	—	CategoryTheory.Adjunction.right_triangle_components
right_triangle_components_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category obj CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.toCategoryStruct Hom.r Hom.l CategoryTheory.NatTrans.app CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Bicategory.Adjunction.unit Hom.adj CategoryTheory.Functor.map CategoryTheory.Bicategory.Adjunction.counit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' right_triangle_components
unit_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category obj CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.toCategoryStruct Hom.l Hom.r CategoryTheory.NatTrans.app CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Bicategory.Adjunction.unit Hom.adj CategoryTheory.Functor.map	—	CategoryTheory.Adjunction.unit_naturality
unit_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category obj CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.toCategoryStruct Hom.l Hom.r CategoryTheory.NatTrans.app CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Bicategory.Adjunction.unit Hom.adj CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_naturality

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