Symmetry

📁 Source: Mathlib/CategoryTheory/Equivalence/Symmetry.lean

Statistics

Metric	Count
Definitions congrLeftFunctor, inverseFunctor, inverseFunctorObj', inverseFunctorObjIso, symmEquiv, symmEquivFunctor, symmEquivInverse	7
Theorems congrLeftFunctor_map, congrLeftFunctor_obj, inverseFunctorMapIso_symm_eq_isoInverseOfIsoFunctor, inverseFunctorObj'_hom_app, inverseFunctorObj'_inv_app, inverseFunctorObjIso_hom, inverseFunctorObjIso_inv, inverseFunctor_map, inverseFunctor_obj, symmEquivFunctor_map, symmEquivFunctor_obj, symmEquivInverse_map_app, symmEquivInverse_obj_counitIso_hom, symmEquivInverse_obj_counitIso_inv, symmEquivInverse_obj_functor, symmEquivInverse_obj_inverse, symmEquivInverse_obj_unitIso_hom, symmEquivInverse_obj_unitIso_inv, symmEquiv_counitIso, symmEquiv_functor, symmEquiv_inverse, symmEquiv_unitIso	22
Total	29

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
congrLeftFunctor 📖	CompOp	2 math math: congrLeftFunctor_obj, congrLeftFunctor_map
inverseFunctor 📖	CompOp	7 math math: inverseFunctor_obj, inverseFunctor_map, inverseFunctorObjIso_inv, inverseFunctorObj'_hom_app, inverseFunctorMapIso_symm_eq_isoInverseOfIsoFunctor, inverseFunctorObjIso_hom, inverseFunctorObj'_inv_app
inverseFunctorObj' 📖	CompOp	2 math math: inverseFunctorObj'_hom_app, inverseFunctorObj'_inv_app
inverseFunctorObjIso 📖	CompOp	2 math math: inverseFunctorObjIso_inv, inverseFunctorObjIso_hom
symmEquiv 📖	CompOp	4 math math: symmEquiv_functor, symmEquiv_counitIso, symmEquiv_unitIso, symmEquiv_inverse
symmEquivFunctor 📖	CompOp	5 math math: symmEquivFunctor_obj, symmEquivFunctor_map, symmEquiv_functor, symmEquiv_counitIso, symmEquiv_unitIso
symmEquivInverse 📖	CompOp	10 math math: symmEquivInverse_obj_counitIso_hom, symmEquivInverse_obj_functor, symmEquivInverse_obj_counitIso_inv, symmEquiv_counitIso, symmEquiv_unitIso, symmEquiv_inverse, symmEquivInverse_obj_unitIso_inv, symmEquivInverse_obj_inverse, symmEquivInverse_obj_unitIso_hom, symmEquivInverse_map_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congrLeftFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Equivalence instCategory Opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Category.opposite congrLeftFunctor Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct congrLeft mkHom CategoryTheory.Functor.whiskeringLeft inverse DFunLike.coe Equiv Quiver.Hom functor EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.conjugateEquiv toAdjunction asNatTrans	—	—
congrLeftFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Equivalence instCategory Opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Category.opposite congrLeftFunctor Opposite.op congrLeft	—	—
inverseFunctorMapIso_symm_eq_isoInverseOfIsoFunctor 📖	mathematical	—	CategoryTheory.Iso.unop CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Equivalence instCategory Opposite CategoryTheory.Category.opposite inverseFunctor CategoryTheory.Functor.mapIso CategoryTheory.Iso.symm CategoryTheory.Iso.isoInverseOfIsoFunctor functorFunctor	—	CategoryTheory.Iso.ext CategoryTheory.NatTrans.ext' CategoryTheory.conjugateEquiv_apply_app CategoryTheory.Iso.isoInverseOfIsoFunctor_hom_app
inverseFunctorObj'_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite.unop CategoryTheory.Functor CategoryTheory.Functor.obj CategoryTheory.Equivalence instCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category inverseFunctor CategoryTheory.Iso.hom inverse inverseFunctorObj' CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inverseFunctorObj'_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite.unop CategoryTheory.Functor CategoryTheory.Functor.obj CategoryTheory.Equivalence instCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category inverseFunctor CategoryTheory.Iso.inv inverse inverseFunctorObj' CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inverseFunctorObjIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom Opposite CategoryTheory.Functor CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Equivalence instCategory inverseFunctor Opposite.op inverse inverseFunctorObjIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inverseFunctorObjIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv Opposite CategoryTheory.Functor CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Equivalence instCategory inverseFunctor Opposite.op inverse inverseFunctorObjIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inverseFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Equivalence instCategory Opposite CategoryTheory.Functor CategoryTheory.Category.opposite CategoryTheory.Functor.category inverseFunctor Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct inverse DFunLike.coe Equiv Quiver.Hom functor EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.conjugateEquiv toAdjunction asNatTrans	—	—
inverseFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Equivalence instCategory Opposite CategoryTheory.Functor CategoryTheory.Category.opposite CategoryTheory.Functor.category inverseFunctor Opposite.op inverse	—	—
symmEquivFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Equivalence instCategory Opposite CategoryTheory.Category.opposite symmEquivFunctor Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct symm mkHom DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.Functor.category functor inverse EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.conjugateEquiv toAdjunction asNatTrans	—	—
symmEquivFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Equivalence instCategory Opposite CategoryTheory.Category.opposite symmEquivFunctor Opposite.op symm	—	—
symmEquivInverse_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app functor Opposite.unop CategoryTheory.Equivalence CategoryTheory.Functor.obj instCategory Opposite CategoryTheory.Category.opposite Opposite.op symm Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct mkHom Equiv.invFun Quiver.Hom CategoryTheory.Functor CategoryTheory.Functor.category inverse CategoryTheory.conjugateEquiv toAdjunction asNatTrans CategoryTheory.Functor.map symmEquivInverse CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.id CategoryTheory.Functor.comp counitInv Quiver.Hom.unop unitInv	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
symmEquivInverse_obj_counitIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp functor Opposite.unop CategoryTheory.Equivalence inverse CategoryTheory.Functor.id counitIso CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite instCategory symmEquivInverse CategoryTheory.Iso.inv unitIso	—	—
symmEquivInverse_obj_counitIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp functor Opposite.unop CategoryTheory.Equivalence inverse CategoryTheory.Functor.id counitIso CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite instCategory symmEquivInverse CategoryTheory.Iso.hom unitIso	—	—
symmEquivInverse_obj_functor 📖	mathematical	—	functor CategoryTheory.Functor.obj Opposite CategoryTheory.Equivalence CategoryTheory.Category.opposite instCategory symmEquivInverse inverse Opposite.unop	—	—
symmEquivInverse_obj_inverse 📖	mathematical	—	inverse CategoryTheory.Functor.obj Opposite CategoryTheory.Equivalence CategoryTheory.Category.opposite instCategory symmEquivInverse functor Opposite.unop	—	—
symmEquivInverse_obj_unitIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp inverse Opposite.unop CategoryTheory.Equivalence functor unitIso CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite instCategory symmEquivInverse CategoryTheory.Iso.inv counitIso	—	—
symmEquivInverse_obj_unitIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp inverse Opposite.unop CategoryTheory.Equivalence functor unitIso CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite instCategory symmEquivInverse CategoryTheory.Iso.hom counitIso	—	—
symmEquiv_counitIso 📖	mathematical	—	counitIso CategoryTheory.Equivalence Opposite instCategory CategoryTheory.Category.opposite symmEquiv CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.comp symmEquivInverse symmEquivFunctor CategoryTheory.Functor.id CategoryTheory.Iso.op Opposite.unop symm CategoryTheory.Functor.obj CategoryTheory.Iso.refl	—	—
symmEquiv_functor 📖	mathematical	—	functor CategoryTheory.Equivalence Opposite instCategory CategoryTheory.Category.opposite symmEquiv symmEquivFunctor	—	—
symmEquiv_inverse 📖	mathematical	—	inverse CategoryTheory.Equivalence Opposite instCategory CategoryTheory.Category.opposite symmEquiv symmEquivInverse	—	—
symmEquiv_unitIso 📖	mathematical	—	unitIso CategoryTheory.Equivalence Opposite instCategory CategoryTheory.Category.opposite symmEquiv CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.id CategoryTheory.Functor.comp symmEquivFunctor symmEquivInverse CategoryTheory.Iso.refl CategoryTheory.Functor.obj	—	—

---

← Back to Index