mapPairEquiv

Mathlib.CategoryTheory.Join.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Join.mapPairEquiv

Lean4

/-- Equivalent categories have equivalent joins. -/
@[simps]
def mapPairEquiv (e : C ≌ C') (e' : D ≌ D') : C ⋆ D ≌ C' ⋆ D'
    where
  functor := mapPair e.functor e'.functor
  inverse := mapPair e.inverse e'.inverse
  unitIso := mapPairId.symm ≪≫ mapIsoWhiskerRight e.unitIso _ ≪≫ mapIsoWhiskerLeft _ e'.unitIso ≪≫ mapPairComp _ _ _ _
  counitIso :=
    (mapPairComp _ _ _ _).symm ≪≫ mapIsoWhiskerRight e.counitIso _ ≪≫ mapIsoWhiskerLeft _ e'.counitIso ≪≫ mapPairId
  functor_unitIso_comp x := by cases x <;> simp [← (inclLeft C' D').map_comp, ← (inclRight C' D').map_comp]

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

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

Разделы

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

Аффилиация

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