leftUnitor

Mathlib.CategoryTheory.Enriched.EnrichedCat

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

Lean4

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

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

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

Разделы

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

Аффилиация

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