postcompose₂ObjMkIso

Mathlib.CategoryTheory.Functor.KanExtension.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.RightExtension.postcompose₂ObjMkIso

Lean4

/-- An isomorphism to describe the action of `RightExtension.postcompose₂` on terms of the form
`RightExtension.mk _ α`. -/
@[simps!]
def postcompose₂ObjMkIso (α : L ⋙ F' ⟶ F) :
    (RightExtension.postcompose₂ L F G).obj (.mk F' α) ≅ .mk (F' ⋙ G) <| (associator _ _ _).inv ≫ whiskerRight α G :=
  CostructuredArrow.isoMk (.refl _)

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

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

Разделы

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

Аффилиация

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