freeReflMap

Mathlib.CategoryTheory.Category.ReflQuiv

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Cat.freeReflMap

Lean4

/-- A refl prefunctor `V ⥤rq W` induces a functor `FreeRefl V ⥤ FreeRefl W` defined using
`freeMap` and the quotient functor. -/
@[simps!]
def freeReflMap {V W : Type*} [ReflQuiver.{v₁ + 1} V] [ReflQuiver.{v₂ + 1} W] (F : V ⥤rq W) : FreeRefl V ⥤ FreeRefl W :=
  Quotient.lift _ (freeMap F.toPrefunctor ⋙ FreeRefl.quotientFunctor W)
    (by
      rintro _ _ _ _ ⟨hfg⟩
      apply Quotient.sound
      simp [ReflPrefunctor.map_id]
      constructor)

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

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

Разделы

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

Аффилиация

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