ranCounit

Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.ranCounit

Lean4

/-- The natural transformation `L ⋙ (L.lan).obj G ⟶ L`. -/
noncomputable def ranCounit : L.ran ⋙ (whiskeringLeft C D H).obj L ⟶ (𝟭 (C ⥤ H))
    where
  app F := rightKanExtensionCounit L F
  naturality {F₁ F₂} φ := by ext; simp [ran]

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

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

Разделы

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

Аффилиация

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