opFunctorCompOpFunctorIso

Mathlib.AlgebraicTopology.SimplicialSet.Op

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

Lean4

/-- The functor `opFunctor : SSet ⥤ SSet` is an involution. -/
@[simps!]
def opFunctorCompOpFunctorIso : opFunctor.{u} ⋙ opFunctor ≅ 𝟭 _ :=
  NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun n ↦ Equiv.toIso (opObjEquiv.trans opObjEquiv)))

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

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

Разделы

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

Аффилиация

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