ofNatIso

Mathlib.CategoryTheory.Monoidal.Braided.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.LaxBraided.ofNatIso

Lean4

/-- Given two lax monoidal, monoidally isomorphic functors, if one is lax braided, so is the other.
-/
def ofNatIso {F G : C ⥤ D} (i : F ≅ G) [F.LaxBraided] [G.LaxMonoidal] [NatTrans.IsMonoidal i.hom] : G.LaxBraided where
  braided X
    Y :=
    by
    have (X Y : C) : μ G X Y = (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app _ := by
      simp [NatTrans.IsMonoidal.tensor X Y, tensorHom_comp_tensorHom_assoc]
    rw [this X Y, this Y X, ← braiding_naturality_assoc, ← Functor.LaxBraided.braided_assoc]
    simp

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

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

Разделы

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

Аффилиация

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