constCompWhiskeringLeftIso

Mathlib.CategoryTheory.Functor.Const

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.constCompWhiskeringLeftIso

Lean4

/-- The canonical isomorphism
`const D ⋙ (whiskeringLeft J _ _).obj F ≅ const J` -/
@[simps!]
def constCompWhiskeringLeftIso (F : J ⥤ D) : const D ⋙ (whiskeringLeft J D C).obj F ≅ const J :=
  NatIso.ofComponents fun X => NatIso.ofComponents fun Y => Iso.refl _

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

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

Разделы

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

Аффилиация

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