ofRightAdjoint

Mathlib.CategoryTheory.Limits.IsLimit

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.IsLimit.ofRightAdjoint

Lean4

/-- Given a right adjoint functor between categories of cones,
the image of a limit cone is a limit cone.
-/
def ofRightAdjoint {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} {left : Cone F ⥤ Cone G} {right : Cone G ⥤ Cone F}
    (adj : left ⊣ right) {c : Cone G} (t : IsLimit c) : IsLimit (right.obj c) :=
  mkConeMorphism (fun s => adj.homEquiv s c (t.liftConeMorphism _)) fun _ _ =>
    (Adjunction.eq_homEquiv_apply _ _ _).2 t.uniq_cone_morphism

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

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

Разделы

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

Аффилиация

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