braiding

Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalCategory.DayConvolution.braiding

Lean4

/-- The braiding isomorphism for Day convolution. -/
def braiding : F ⊛ G ≅ G ⊛ F
    where
  hom := corepresentableBy F G |>.homEquiv.symm <| braidingHomCorepresenting F G
  inv := corepresentableBy G F |>.homEquiv.symm <| braidingInvCorepresenting F G
  hom_inv_id := by
    apply Functor.hom_ext_of_isLeftKanExtension (F ⊛ G) (unit F G)
    ext
    simp [-tensor_obj]
  inv_hom_id := by
    apply Functor.hom_ext_of_isLeftKanExtension (G ⊛ F) (unit G F)
    ext
    simp [-tensor_obj]

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

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

Разделы

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

Аффилиация

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