English
There is a natural isomorphism between externalProductBifunctor swapped and the swapped tensor product construction, natural in both F₁ and F₂.
Русский
Существует естественный изоморфизм между swapped и переставленным конструктом тензорного произведения, естественный по обеим F₁ и F₂.
LaTeX
$$$externalProductSwap \\;:\\; externalProductBifunctor J_1 J_2 C \\Rightarrow Prod.swap _ _ \\circ externalProductBifunctor J_2 J_1 C$$$
Lean4
/-- When both diagrams have the same source category, composing the external product with
the diagonal gives the pointwise functor tensor product.
Note that `(externalProductCompDiagIso _ _).app (F₁, F₂) : Functor.diag J₁ ⋙ F₁ ⊠ F₂ ≅ F₁ ⊗ F₂`
type checks. -/
@[simps!]
def externalProductCompDiagIso :
externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft _ _ _ |>.obj <| Functor.diag J₁) ≅ tensor (J₁ ⥤ C) :=
NatIso.ofComponents (fun _ ↦ NatIso.ofComponents (fun _ ↦ Iso.refl _) (by simp [tensorHom_def]))
(fun _ ↦ by ext; simp [tensorHom_def])
