forget_obj_of

Mathlib.CategoryTheory.Limits.ExactFunctor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.LeftExactFunctor.forget_obj_of

Lean4

theorem forget_obj_of (F : C ⥤ D) [PreservesFiniteLimits F] :
    (LeftExactFunctor.forget C D).obj (LeftExactFunctor.of F) = F :=
  rfl

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

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

Разделы

Аффилиация

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