Opposites

📁 Source: Mathlib/CategoryTheory/Join/Opposites.lean

Statistics

Metric	Count
Definitions InclLeftCompRightOpOpEquivFunctor, InclRightCompRightOpOpEquivFunctor, inclLeftCompOpEquivInverse, inclRightCompOpEquivInverse, opEquiv	5
Theorems InclLeftCompRightOpOpEquivFunctor_hom_app, InclLeftCompRightOpOpEquivFunctor_inv_app, InclRightCompRightOpOpEquivFunctor_hom_app, InclRightCompRightOpOpEquivFunctor_inv_app, inclLeftCompOpEquivInverse_hom_app_op, inclLeftCompOpEquivInverse_inv_app_op, inclRightCompOpEquivInverse_hom_app_op, inclRightCompOpEquivInverse_inv_app_op, opEquiv_functor_map_op_edge, opEquiv_functor_map_op_inclLeft, opEquiv_functor_map_op_inclRight, opEquiv_functor_obj_op_left, opEquiv_functor_obj_op_right, opEquiv_inverse_map_edge_op, opEquiv_inverse_map_inclLeft_op, opEquiv_inverse_map_inclRight_op, opEquiv_inverse_obj_left_op, opEquiv_inverse_obj_right_op	18
Total	23

CategoryTheory.Join

Definitions

Name	Category	Theorems
InclLeftCompRightOpOpEquivFunctor 📖	CompOp	2 math math: InclLeftCompRightOpOpEquivFunctor_hom_app, InclLeftCompRightOpOpEquivFunctor_inv_app
InclRightCompRightOpOpEquivFunctor 📖	CompOp	2 math math: InclRightCompRightOpOpEquivFunctor_inv_app, InclRightCompRightOpOpEquivFunctor_hom_app
inclLeftCompOpEquivInverse 📖	CompOp	2 math math: inclLeftCompOpEquivInverse_inv_app_op, inclLeftCompOpEquivInverse_hom_app_op
inclRightCompOpEquivInverse 📖	CompOp	2 math math: inclRightCompOpEquivInverse_inv_app_op, inclRightCompOpEquivInverse_hom_app_op
opEquiv 📖	CompOp	18 math math: inclRightCompOpEquivInverse_inv_app_op, opEquiv_functor_obj_op_right, opEquiv_inverse_map_inclRight_op, opEquiv_functor_map_op_edge, opEquiv_functor_map_op_inclRight, opEquiv_inverse_obj_right_op, opEquiv_inverse_map_inclLeft_op, InclLeftCompRightOpOpEquivFunctor_hom_app, inclRightCompOpEquivInverse_hom_app_op, opEquiv_functor_obj_op_left, opEquiv_inverse_obj_left_op, inclLeftCompOpEquivInverse_inv_app_op, inclLeftCompOpEquivInverse_hom_app_op, opEquiv_inverse_map_edge_op, InclLeftCompRightOpOpEquivFunctor_inv_app, InclRightCompRightOpOpEquivFunctor_inv_app, opEquiv_functor_map_op_inclLeft, InclRightCompRightOpOpEquivFunctor_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
InclLeftCompRightOpOpEquivFunctor_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Join CategoryTheory.Category.opposite instCategory CategoryTheory.Functor.comp inclLeft CategoryTheory.Functor.rightOp CategoryTheory.Equivalence.functor opEquiv inclRight CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category InclLeftCompRightOpOpEquivFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Opposite.op right	—	CategoryTheory.Category.comp_id
InclLeftCompRightOpOpEquivFunctor_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Join CategoryTheory.Category.opposite instCategory CategoryTheory.Functor.rightOp inclRight CategoryTheory.Functor.comp inclLeft CategoryTheory.Equivalence.functor opEquiv CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category InclLeftCompRightOpOpEquivFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Opposite.op right	—	CategoryTheory.Category.comp_id
InclRightCompRightOpOpEquivFunctor_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Join CategoryTheory.Category.opposite instCategory CategoryTheory.Functor.comp inclRight CategoryTheory.Functor.rightOp CategoryTheory.Equivalence.functor opEquiv inclLeft CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category InclRightCompRightOpOpEquivFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Opposite.op left	—	CategoryTheory.Category.comp_id
InclRightCompRightOpOpEquivFunctor_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Join CategoryTheory.Category.opposite instCategory CategoryTheory.Functor.rightOp inclLeft CategoryTheory.Functor.comp inclRight CategoryTheory.Equivalence.functor opEquiv CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category InclRightCompRightOpOpEquivFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Opposite.op left	—	CategoryTheory.Category.comp_id
inclLeftCompOpEquivInverse_hom_app_op 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Join instCategory CategoryTheory.Functor.comp inclLeft CategoryTheory.Equivalence.inverse opEquiv CategoryTheory.Functor.op inclRight CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category inclLeftCompOpEquivInverse Opposite.op CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct right	—	—
inclLeftCompOpEquivInverse_inv_app_op 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Join instCategory CategoryTheory.Functor.op inclRight CategoryTheory.Functor.comp inclLeft CategoryTheory.Equivalence.inverse opEquiv CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category inclLeftCompOpEquivInverse Opposite.op CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct right	—	—
inclRightCompOpEquivInverse_hom_app_op 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Join instCategory CategoryTheory.Functor.comp inclRight CategoryTheory.Equivalence.inverse opEquiv CategoryTheory.Functor.op inclLeft CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category inclRightCompOpEquivInverse Opposite.op CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct left	—	—
inclRightCompOpEquivInverse_inv_app_op 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Join instCategory CategoryTheory.Functor.op inclLeft CategoryTheory.Functor.comp inclRight CategoryTheory.Equivalence.inverse opEquiv CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category inclRightCompOpEquivInverse Opposite.op CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct left	—	—
opEquiv_functor_map_op_edge 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Join CategoryTheory.Category.opposite instCategory CategoryTheory.Equivalence.functor opEquiv Opposite.op right left Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop edge	—	—
opEquiv_functor_map_op_inclLeft 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Join CategoryTheory.Category.opposite instCategory CategoryTheory.Equivalence.functor opEquiv Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop inclLeft inclRight	—	—
opEquiv_functor_map_op_inclRight 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Join CategoryTheory.Category.opposite instCategory CategoryTheory.Equivalence.functor opEquiv Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop inclRight inclLeft	—	—
opEquiv_functor_obj_op_left 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Join CategoryTheory.Category.opposite instCategory CategoryTheory.Equivalence.functor opEquiv Opposite.op left right	—	—
opEquiv_functor_obj_op_right 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Join CategoryTheory.Category.opposite instCategory CategoryTheory.Equivalence.functor opEquiv Opposite.op right left	—	—
opEquiv_inverse_map_edge_op 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Join Opposite CategoryTheory.Category.opposite instCategory CategoryTheory.Equivalence.inverse opEquiv left Opposite.op right edge Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
opEquiv_inverse_map_inclLeft_op 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Join Opposite CategoryTheory.Category.opposite instCategory CategoryTheory.Equivalence.inverse opEquiv CategoryTheory.Functor.obj inclLeft Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom inclRight	—	—
opEquiv_inverse_map_inclRight_op 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Join Opposite CategoryTheory.Category.opposite instCategory CategoryTheory.Equivalence.inverse opEquiv CategoryTheory.Functor.obj inclRight Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom inclLeft	—	—
opEquiv_inverse_obj_left_op 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Join Opposite CategoryTheory.Category.opposite instCategory CategoryTheory.Equivalence.inverse opEquiv left Opposite.op right	—	—
opEquiv_inverse_obj_right_op 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Join Opposite CategoryTheory.Category.opposite instCategory CategoryTheory.Equivalence.inverse opEquiv right Opposite.op left	—	—

---

← Back to Index