English
There is an isomorphism expressing the coherence between external product and diagonal functor, given by natural transformations and identities.
Русский
Существует изоморфизм, выражающий когерентность между внешним произведением и диагональным функтором, задаваемый натуральными преобразованиями и тождествами.
LaTeX
$$NatIso.ofComponents (fun _ => NatIso.ofComponents (fun _ => Iso.refl _) _) (by ext; simp)$$
Lean4
/-- When `C` is braided, there is an isomorphism `Prod.swap _ _ ⋙ F₁ ⊠ F₂ ≅ F₂ ⊠ F₁`, natural
in both `F₁` and `F₂`.
Note that `(externalProductSwap _ _ _).app (F₁, F₂) : Prod.swap _ _ ⋙ F₁ ⊠ F₂ ≅ F₂ ⊠ F₁`
type checks. -/
@[simps!]
def externalProductSwap [BraidedCategory C] :
externalProductBifunctor J₁ J₂ C ⋙ (whiskeringLeft _ _ _ |>.obj <| Prod.swap _ _) ≅
Prod.swap _ _ ⋙ externalProductBifunctor J₂ J₁ C :=
NatIso.ofComponents (fun _ ↦ NatIso.ofComponents (fun _ ↦ β_ _ _) (by simp [whisker_exchange]))
(fun _ ↦ by ext; simp [whisker_exchange])
