isoMk

Mathlib.CategoryTheory.Monoidal.Center

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Center.isoMk

Lean4

/-- Construct an isomorphism in the Drinfeld center from
a morphism whose underlying morphism is an isomorphism.
-/
@[simps]
def isoMk {X Y : Center C} (f : X ⟶ Y) [IsIso f.f] : X ≅ Y
    where
  hom := f
  inv :=
    ⟨inv f.f, fun U => by simp [← cancel_epi (f.f ▷ U), ← comp_whiskerRight_assoc, ← MonoidalCategory.whiskerLeft_comp]⟩

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

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

Разделы

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

Аффилиация

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