counitIso

Mathlib.CategoryTheory.Localization.Construction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso

Lean4

/-- The counit isomorphism of the equivalence of categories `WhiskeringLeftEquivalence W D`. -/
@[simps!]
def counitIso : inverse W D ⋙ functor W D ≅ 𝟭 (W.FunctorsInverting D) :=
  eqToIso
    (by
      refine Functor.ext ?_ ?_
      · rintro ⟨G, hG⟩
        ext
        exact fac G hG
      · rintro ⟨G₁, hG₁⟩ ⟨G₂, hG₂⟩ f
        ext
        apply NatTransExtension.app_eq)

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

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

Разделы

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

Аффилиация

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