Op

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

Statistics

Metric	Count
Definitions opEquivalence, opFunctor, opFunctorCompOpFunctorIso, opObjIso	4
Theorems opEquivalence_counitIso, opEquivalence_functor, opEquivalence_inverse, opEquivalence_unitIso, opFunctorCompOpFunctorIso_hom_app_app, opFunctorCompOpFunctorIso_inv_app_app, opFunctor_map_app, opFunctor_obj_map, opFunctor_obj_δ, opFunctor_obj_σ	10
Total	14

SimplicialObject

Definitions

Name	Category	Theorems
opEquivalence 📖	CompOp	4 math math: opEquivalence_counitIso, opEquivalence_unitIso, opEquivalence_inverse, opEquivalence_functor
opFunctor 📖	CompOp	9 math math: opFunctor_obj_σ, opFunctor_obj_map, opFunctor_map_app, opFunctor_obj_δ, opFunctorCompOpFunctorIso_hom_app_app, opEquivalence_unitIso, opFunctorCompOpFunctorIso_inv_app_app, opEquivalence_inverse, opEquivalence_functor
opFunctorCompOpFunctorIso 📖	CompOp	4 math math: opEquivalence_counitIso, opFunctorCompOpFunctorIso_hom_app_app, opEquivalence_unitIso, opFunctorCompOpFunctorIso_inv_app_app
opObjIso 📖	CompOp	6 math math: opFunctor_obj_σ, opFunctor_obj_map, opFunctor_map_app, opFunctor_obj_δ, opFunctorCompOpFunctorIso_hom_app_app, opFunctorCompOpFunctorIso_inv_app_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
opEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject opEquivalence opFunctorCompOpFunctorIso	—	—
opEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject opEquivalence opFunctor	—	—
opEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject opEquivalence opFunctor	—	—
opEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject 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.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.comp opFunctor CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category opFunctorCompOpFunctorIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opObjIso	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
opFunctorCompOpFunctorIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.Functor.comp opFunctor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category opFunctorCompOpFunctorIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opObjIso	—	CategoryTheory.Category.assoc CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
opFunctor_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject opFunctor CategoryTheory.Functor.map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom opObjIso CategoryTheory.Iso.inv	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
opFunctor_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject opFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.op SimplexCategory.rev Opposite.unop CategoryTheory.Iso.hom opObjIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver Quiver.Hom.unop CategoryTheory.Iso.inv	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
opFunctor_obj_δ 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject opFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op CategoryTheory.Iso.hom opObjIso CategoryTheory.Iso.inv	—	opFunctor_obj_map SimplexCategory.rev_map_δ
opFunctor_obj_σ 📖	mathematical	—	CategoryTheory.SimplicialObject.σ CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject opFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op CategoryTheory.Iso.hom opObjIso CategoryTheory.Iso.inv	—	opFunctor_obj_map SimplexCategory.rev_map_σ

---

← Back to Index