mapComp

Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.Over.mapComp

Lean4

/-- `Over.map` commutes with composition. -/
@[simps! hom_app_left inv_app_left]
def mapComp {X Y Z : T} {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) [Q.RespectsIso] :
    map Q (P.comp_mem f g hf hg) ≅ map Q hf ⋙ map Q hg :=
  NatIso.ofComponents (fun X ↦ Over.isoMk (Iso.refl _))

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

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

Разделы

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

Аффилиация

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