Op

📁 Source: Mathlib/CategoryTheory/Category/Cat/Op.lean

Statistics

Metric	Count
Definitions opEquivalence, opFunctor, opFunctorInvolutive	3
Theorems opEquivalence_counitIso, opEquivalence_functor, opEquivalence_inverse, opEquivalence_unitIso, opFunctorInvolutive_hom_app_toFunctor_map, opFunctorInvolutive_hom_app_toFunctor_obj, opFunctorInvolutive_inv_app_toFunctor_map, opFunctorInvolutive_inv_app_toFunctor_obj, opFunctor_map, opFunctor_obj	10
Total	13

CategoryTheory.Cat

Definitions

Name	Category	Theorems
opEquivalence 📖	CompOp	4 math math: opEquivalence_counitIso, opEquivalence_unitIso, opEquivalence_inverse, opEquivalence_functor
opFunctor 📖	CompOp	10 math math: opEquivalence_counitIso, opFunctor_obj, opEquivalence_unitIso, opFunctor_map, opFunctorInvolutive_hom_app_toFunctor_map, opFunctorInvolutive_hom_app_toFunctor_obj, opEquivalence_inverse, opEquivalence_functor, opFunctorInvolutive_inv_app_toFunctor_map, opFunctorInvolutive_inv_app_toFunctor_obj
opFunctorInvolutive 📖	CompOp	4 math math: opFunctorInvolutive_hom_app_toFunctor_map, opFunctorInvolutive_hom_app_toFunctor_obj, opFunctorInvolutive_inv_app_toFunctor_map, opFunctorInvolutive_inv_app_toFunctor_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
opEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.Cat category opEquivalence CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.comp opFunctor CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Functor.toCatHom Opposite CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Category.opposite str CategoryTheory.unopUnop CategoryTheory.Bundled.str CategoryTheory.opOp	—	—
opEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.Cat category opEquivalence opFunctor	—	—
opEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.Cat category opEquivalence opFunctor	—	—
opEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.Cat category opEquivalence CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.id CategoryTheory.Functor.comp opFunctor CategoryTheory.Functor.obj CategoryTheory.Functor.toCatHom CategoryTheory.Bundled.α CategoryTheory.Category Opposite CategoryTheory.Bundled.str CategoryTheory.Category.opposite CategoryTheory.opOp str CategoryTheory.unopUnop	—	—
opFunctorInvolutive_hom_app_toFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Category.opposite str Hom.toFunctor CategoryTheory.Functor.obj CategoryTheory.Cat category CategoryTheory.Functor.comp opFunctor CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category opFunctorInvolutive Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop	—	—
opFunctorInvolutive_hom_app_toFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Category.opposite str Hom.toFunctor CategoryTheory.Cat category CategoryTheory.Functor.comp opFunctor CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category opFunctorInvolutive Opposite.unop	—	—
opFunctorInvolutive_inv_app_toFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Bundled.α CategoryTheory.Category str Opposite CategoryTheory.Category.opposite Hom.toFunctor CategoryTheory.Functor.obj CategoryTheory.Cat category CategoryTheory.Functor.id CategoryTheory.Functor.comp opFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category opFunctorInvolutive Quiver.Hom.op Quiver.opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op	—	—
opFunctorInvolutive_inv_app_toFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category str Opposite CategoryTheory.Category.opposite Hom.toFunctor CategoryTheory.Cat category CategoryTheory.Functor.id CategoryTheory.Functor.comp opFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category opFunctorInvolutive Opposite.op	—	—
opFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Cat category opFunctor CategoryTheory.Functor.toCatHom Opposite CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Category.opposite str CategoryTheory.Functor.op Hom.toFunctor	—	—
opFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Cat category opFunctor of Opposite CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Category.opposite str	—	—

---

← Back to Index