lift₂NatIso

Mathlib.CategoryTheory.Localization.Bifunctor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Localization.lift₂NatIso

Lean4

/-- The natural isomorphism `F₁' ≅ F₂'` of bifunctors induced by a
natural isomorphism `e : F₁ ≅ F₂` when `Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'`
and `Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'` hold. -/
noncomputable def lift₂NatIso (e : F₁ ≅ F₂) : F₁' ≅ F₂'
    where
  hom := lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' e.hom
  inv := lift₂NatTrans L₁ L₂ W₁ W₂ F₂ F₁ F₂' F₁' e.inv
  hom_inv_id := natTrans₂_ext L₁ L₂ W₁ W₂ (by simp)
  inv_hom_id := natTrans₂_ext L₁ L₂ W₁ W₂ (by simp)

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

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

Разделы

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

Аффилиация

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