lift

Mathlib.CategoryTheory.MorphismProperty.Comma

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.Comma.lift

Lean4

/-- Lift a functor `F : C ⥤ Comma L R` to the subcategory `P.Comma L R Q W` under
suitable assumptions on `F`. -/
@[simps obj_toComma map_hom]
def lift {C : Type*} [Category C] (F : C ⥤ Comma L R) (hP : ∀ X, P (F.obj X).hom)
    (hQ : ∀ {X Y} (f : X ⟶ Y), Q (F.map f).left) (hW : ∀ {X Y} (f : X ⟶ Y), W (F.map f).right) : C ⥤ P.Comma L R Q W
    where
  obj
    X :=
    { __ := F.obj X
      prop := hP X }
  map {X Y}
    f :=
    { __ := F.map f
      prop_hom_left := hQ f
      prop_hom_right := hW f }

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

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

Разделы

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

Аффилиация

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