opFunctorCompOpFunctorIso

Mathlib.AlgebraicTopology.SimplicialObject.Op

URI: https://scilib.ai/kg/mathlib#SimplicialObject.opFunctorCompOpFunctorIso

Lean4

/-- The functor `opFunctor : SimplicialObject C ⥤ SimplicialObject C`
is a covariant involution. -/
def opFunctorCompOpFunctorIso : opFunctor (C := C) ⋙ opFunctor ≅ 𝟭 _ :=
  (Functor.whiskeringLeftObjCompIso _ _).symm ≪≫
    (Functor.whiskeringLeft _ _ _).mapIso ((Functor.opHom _ _).mapIso (SimplexCategory.revCompRevIso).symm.op) ≪≫
      Functor.whiskeringLeftObjIdIso

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru