mapCompLeft

Mathlib.CategoryTheory.Join.Pseudofunctor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Join.mapCompLeft

Lean4

/-- The structural isomorphism for composition of `pseudoFunctorLeft`. -/
def mapCompLeft (F : A ⥤ B) (G : B ⥤ C) : mapPair (F ⋙ G) (𝟭 D) ≅ mapPair F (𝟭 D) ⋙ mapPair G (𝟭 D) :=
  mapIsoWhiskerLeft _ (Functor.leftUnitor _).symm ≪≫ mapPairComp F (𝟭 D) G (𝟭 D)

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

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

Разделы

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

Аффилиация

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