externalProductFlip

Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic

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

Lean4

/-- A version of `externalProductSwap` phrased in terms of the curried functors. -/
@[simps!]
def externalProductFlip [BraidedCategory C] :
    (Functor.postcompose₂.obj <| flipFunctor _ _ _).obj (externalProductBifunctorCurried J₁ J₂ C) ≅
      (externalProductBifunctorCurried J₂ J₁ C).flip :=
  NatIso.ofComponents <| fun _ ↦
    NatIso.ofComponents <| fun _ ↦ NatIso.ofComponents <| fun _ ↦ NatIso.ofComponents (fun _ ↦ β_ _ _)

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

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

Разделы

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

Аффилиация

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