pushoutComp

Mathlib.CategoryTheory.Comma.Over.Pullback

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Under.pushoutComp

Lean4

/-- pushout commutes with composition (up to natural isomorphism). -/
def pushoutComp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasPushoutsAlong f] [HasPushoutsAlong g] :
    pushout (f ≫ g) ≅ pushout f ⋙ pushout g :=
  (conjugateIsoEquiv ((mapPushoutAdj _).comp (mapPushoutAdj _)) (mapPushoutAdj _)).symm (mapComp f g).symm

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

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

Разделы

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

Аффилиация

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