η

Mathlib.CategoryTheory.Localization.Adjunction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Adjunction.Localization.η

Lean4

/-- Auxiliary definition of the counit morphism for the adjunction `Adjunction.localization` -/
noncomputable def η : F' ⋙ G' ⟶ 𝟭 D₂ :=
  by
  letI : Lifting L₂ W₂ ((F ⋙ G) ⋙ L₂) (F' ⋙ G') := Lifting.mk (CatCommSq.hComp F G L₂ L₁ L₂ F' G').iso.symm
  exact liftNatTrans L₂ W₂ ((F ⋙ G) ⋙ L₂) L₂ (F' ⋙ G') (𝟭 D₂) (whiskerRight adj.counit L₂)

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

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

Разделы

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

Аффилиация

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