homObjFunctor

Mathlib.CategoryTheory.Functor.FunctorHom

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

Lean4

/-- The contravariant functor taking `A : C ⥤ Type w` to `HomObj F G A`, i.e. Hom(F ⊗ -, G). -/
@[simps]
def homObjFunctor : (C ⥤ Type w)ᵒᵖ ⥤ Type max w v' u
    where
  obj A := HomObj F G A.unop
  map {A A'} f
    x :=
    { app := fun X a ↦ x.app X (f.unop.app _ a)
      naturality := fun {X Y} φ a ↦ by
        rw [← HomObj.naturality]
        congr 2
        exact congr_fun (f.unop.naturality φ) a }

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

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

Разделы

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

Аффилиация

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