compRightIso

Mathlib.CategoryTheory.Limits.Shapes.Reflexive

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.reflexivePair.compRightIso

Lean4

/-- A `reflexivePair` composed with a functor is isomorphic to the `reflexivePair` obtained by
applying the functor at each map. -/
@[simps!]
def compRightIso {D : Type u₂} [Category.{v₂} D] {A B : C} (f g : A ⟶ B) (s : B ⟶ A) (sl : s ≫ f = 𝟙 B)
    (sr : s ≫ g = 𝟙 B) (F : C ⥤ D) :
    (reflexivePair f g s sl sr) ⋙ F ≅
      reflexivePair (F.map f) (F.map g) (F.map s) (by simp only [← Functor.map_comp, sl, Functor.map_id])
        (by simp only [← Functor.map_comp, sr, Functor.map_id]) :=
  mkNatIso (Iso.refl _) (Iso.refl _)

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

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

Разделы

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

Аффилиация

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