mapIdIso

Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

URI: https://scilib.ai/kg/mathlib#CategoryTheory.StrictlyUnitaryLaxFunctor.mapIdIso

Lean4

/-- Promote the morphism `F.mapId x : 𝟙 (F.obj x) ⟶ F.map (𝟙 x)`
to an isomorphism when `F` is strictly unitary. -/
@[simps]
def mapIdIso (F : StrictlyUnitaryLaxFunctor B C) (x : B) : 𝟙 (F.obj x) ≅ F.map (𝟙 x)
    where
  hom := F.mapId x
  inv := eqToHom (F.map_id x)
  hom_inv_id := by simp [F.mapId_eq_eqToHom]
  inv_hom_id := by simp [F.mapId_eq_eqToHom]

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

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

Разделы

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

Аффилиация

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