rightAdj_map

Mathlib.CategoryTheory.Closed.FunctorToTypes

URI: https://scilib.ai/kg/mathlib#CategoryTheory.FunctorToTypes.rightAdj_map

Lean4

/-- Given a morphism `f : G ⟶ H`, an object `c : C`, and an element of `(F.functorHom G).obj c`,
construct an element of `(F.functorHom H).obj c`. -/
@[simps]
def rightAdj_map {F G H : C ⥤ Type max w v u} (f : G ⟶ H) (c : C) (a : (F.functorHom G).obj c) : (F.functorHom H).obj c
    where
  app d b := a.app d b ≫ f.app d
  naturality g
    h := by
    have := a.naturality g h
    change (F.map g ≫ a.app _ (h ≫ g)) ≫ _ = _
    aesop

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

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

Разделы

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

Аффилиация

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