rightUnitor

Mathlib.CategoryTheory.Enriched.EnrichedCat

URI: https://scilib.ai/kg/mathlib#CategoryTheory.EnrichedCat.rightUnitor

Lean4

/-- Composing any `V`-enriched functor with the identity functor is isomorphic to the former
functor. -/
@[simps!]
def rightUnitor (F : EnrichedFunctor V C D) : EnrichedFunctor.comp V F (EnrichedFunctor.id V _) ≅ F :=
  EnrichedFunctor.isoMk <|
    F.forgetComp _ ≪≫ Functor.isoWhiskerLeft _ (EnrichedFunctor.forgetId V D) ≪≫ Functor.rightUnitor F.forget

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

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

Разделы

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

Аффилиация

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