mkOfHomFunctors

Mathlib.CategoryTheory.Bicategory.Functor.Prelax

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PrelaxFunctor.mkOfHomFunctors

Lean4

/-- Construct a prelax functor from a map on objects, and functors between the corresponding
hom types. -/
@[simps]
def mkOfHomFunctors (F : B → C) (F' : (a : B) → (b : B) → (a ⟶ b) ⥤ (F a ⟶ F b)) : PrelaxFunctor B C
    where
  toPrelaxFunctorStruct := PrelaxFunctorStruct.mkOfHomPrefunctors F fun a b => (F' a b).toPrefunctor
  map₂_id {a b} := (F' a b).map_id
  map₂_comp {a b} := (F' a b).map_comp

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

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

Разделы

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

Аффилиация

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