Op

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/Op.lean

Statistics

Metric	Count
Definitions op, opEquivalence, opFunctor, opFunctorCompOpFunctorIso, opObjEquiv	5
Theorems opEquivalence_counitIso, opEquivalence_functor, opEquivalence_inverse, opEquivalence_unitIso, opFunctorCompOpFunctorIso_hom_app_app, opFunctorCompOpFunctorIso_inv_app_app, opFunctor_map, op_map, op_δ, op_σ	10
Total	15

SSet

Definitions

Name	Category	Theorems
op 📖	CompOp	4 math math: op_δ, opFunctor_map, op_σ, op_map
opEquivalence 📖	CompOp	4 math math: opEquivalence_inverse, opEquivalence_unitIso, opEquivalence_counitIso, opEquivalence_functor
opFunctor 📖	CompOp	6 math math: opFunctorCompOpFunctorIso_inv_app_app, opFunctorCompOpFunctorIso_hom_app_app, opEquivalence_inverse, opFunctor_map, opEquivalence_unitIso, opEquivalence_functor
opFunctorCompOpFunctorIso 📖	CompOp	4 math math: opFunctorCompOpFunctorIso_inv_app_app, opFunctorCompOpFunctorIso_hom_app_app, opEquivalence_unitIso, opEquivalence_counitIso
opObjEquiv 📖	CompOp	6 math math: op_δ, opFunctorCompOpFunctorIso_inv_app_app, opFunctorCompOpFunctorIso_hom_app_app, opFunctor_map, op_σ, op_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
opEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso SSet largeCategory opEquivalence opFunctorCompOpFunctorIso	—	—
opEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor SSet largeCategory opEquivalence opFunctor	—	—
opEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse SSet largeCategory opEquivalence opFunctor	—	—
opEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso SSet largeCategory opEquivalence CategoryTheory.Iso.symm CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp opFunctor CategoryTheory.Functor.id opFunctorCompOpFunctorIso	—	—
opFunctorCompOpFunctorIso_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj SSet largeCategory CategoryTheory.Functor.comp opFunctor CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category opFunctorCompOpFunctorIso DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike opObjEquiv	—	—
opFunctorCompOpFunctorIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj SSet largeCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp opFunctor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category opFunctorCompOpFunctorIso DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm opObjEquiv	—	—
opFunctor_map 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj SSet largeCategory opFunctor CategoryTheory.Functor.map DFunLike.coe Equiv op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm opObjEquiv	—	—
op_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types op DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite.op SimplexCategory.rev Opposite.unop EquivLike.toFunLike Equiv.instEquivLike Equiv.symm opObjEquiv Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop	—	—
op_δ 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types op DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm opObjEquiv	—	SimplexCategory.rev_map_δ
op_σ 📖	mathematical	—	CategoryTheory.SimplicialObject.σ CategoryTheory.types op DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm opObjEquiv	—	SimplexCategory.rev_map_σ

---

← Back to Index