whiskeringEquivalence

Mathlib.CategoryTheory.Limits.Cones

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.Cones.whiskeringEquivalence

Lean4

/-- Whiskering by an equivalence gives an equivalence between categories of cones.
-/
@[simps]
def whiskeringEquivalence (e : K ≌ J) : Cone F ≌ Cone (e.functor ⋙ F)
    where
  functor := whiskering e.functor
  inverse := whiskering e.inverse ⋙ postcompose (e.invFunIdAssoc F).hom
  unitIso := NatIso.ofComponents fun s => Cones.ext (Iso.refl _)
  counitIso :=
    NatIso.ofComponents fun s =>
      Cones.ext (Iso.refl _)
        (by
          intro k
          simpa [e.counit_app_functor] using s.w (e.unitInv.app k))

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

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

Разделы

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

Аффилиация

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