comapComp

Mathlib.CategoryTheory.Pi.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Pi.comapComp

Lean4

/-- The natural isomorphism comparing between
pulling back along two successive functions, and
pulling back along their composition
-/
@[simps!]
def comapComp (f : K → J) (g : J → I) : comap C g ⋙ comap (C ∘ g) f ≅ comap C (g ∘ f)
    where
  hom :=
    { app := fun X b => 𝟙 (X (g (f b)))
      naturality := fun X Y f' => by simp only [comap, Function.comp]; funext; simp }
  inv :=
    { app := fun X b => 𝟙 (X (g (f b)))
      naturality := fun X Y f' => by simp only [comap, Function.comp]; funext; simp }

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

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

Разделы

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

Аффилиация

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