whiskeringRight

Mathlib.CategoryTheory.Whiskering

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.FullyFaithful.whiskeringRight

Lean4

/-- If `F : D ⥤ E` is fully faithful, then so is
`(whiskeringRight C D E).obj F : (C ⥤ D) ⥤ C ⥤ E`. -/
@[simps]
def whiskeringRight {F : D ⥤ E} (hF : F.FullyFaithful) (C : Type*) [Category C] :
    ((whiskeringRight C D E).obj F).FullyFaithful where
  preimage
    f :=
    { app := fun X => hF.preimage (f.app X)
      naturality := fun _ _ g => by
        apply hF.map_injective
        dsimp
        simp only [map_comp, map_preimage]
        apply f.naturality }

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

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

Разделы

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

Аффилиация

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