Rev

📁 Source: Mathlib/AlgebraicTopology/SimplexCategory/Rev.lean

Statistics

Metric	Count
Definitions rev, revCompRevIso, revEquivalence	3
Theorems revCompRevIso_hom_app, revCompRevIso_inv_app, revEquivalence_counitIso, revEquivalence_functor, revEquivalence_inverse, revEquivalence_unitIso, rev_map_apply, rev_map_rev_map, rev_map_δ, rev_map_σ, rev_obj	11
Total	14

SimplexCategory

Definitions

Name	Category	Theorems
rev 📖	CompOp	12 math math: SimplicialObject.opFunctor_obj_map, revEquivalence_unitIso, rev_map_δ, revCompRevIso_inv_app, rev_map_apply, rev_map_σ, rev_obj, revCompRevIso_hom_app, revEquivalence_functor, rev_map_rev_map, SSet.op_map, revEquivalence_inverse
revCompRevIso 📖	CompOp	4 math math: revEquivalence_unitIso, revCompRevIso_inv_app, revCompRevIso_hom_app, revEquivalence_counitIso
revEquivalence 📖	CompOp	4 math math: revEquivalence_unitIso, revEquivalence_functor, revEquivalence_inverse, revEquivalence_counitIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
revCompRevIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app SimplexCategory smallCategory CategoryTheory.Functor.comp rev CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category revCompRevIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
revCompRevIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app SimplexCategory smallCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp rev CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category revCompRevIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
revEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso SimplexCategory smallCategory revEquivalence revCompRevIso	—	—
revEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor SimplexCategory smallCategory revEquivalence rev	—	—
revEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse SimplexCategory smallCategory revEquivalence rev	—	—
revEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso SimplexCategory smallCategory revEquivalence CategoryTheory.Iso.symm CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp rev CategoryTheory.Functor.id revCompRevIso	—	—
rev_map_apply 📖	mathematical	—	DFunLike.coe OrderHom len PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike Hom.toOrderHom CategoryTheory.Functor.map SimplexCategory smallCategory rev	—	—
rev_map_rev_map 📖	mathematical	—	CategoryTheory.Functor.map SimplexCategory smallCategory rev CategoryTheory.Functor.obj	—	Hom.ext OrderHom.ext rev_map_apply
rev_map_δ 📖	mathematical	—	CategoryTheory.Functor.map SimplexCategory smallCategory rev δ	—	Hom.ext OrderHom.ext rev_map_apply Fin.succAbove_rev_right
rev_map_σ 📖	mathematical	—	CategoryTheory.Functor.map SimplexCategory smallCategory rev σ	—	Hom.ext OrderHom.ext rev_map_apply Fin.predAbove_rev_right
rev_obj 📖	mathematical	—	CategoryTheory.Functor.obj SimplexCategory smallCategory rev	—	—

---

← Back to Index