English
The natural isomorphisms that witness the monoidal structure of the tensor functor agree with the componentwise tensor μ on pairs.
Русский
Единство моноидального тензорного функторы согласуется с компонентной μ на парах объектов.
LaTeX
$$$\; μ( tensor C) X Y = tensorμ X.1 X.2 Y.1 Y.2.$$$
Lean4
instance tensorMonoidal : (tensor C).Monoidal :=
Functor.CoreMonoidal.toMonoidal
{ εIso := (λ_ (𝟙_ C)).symm
μIso := fun X Y ↦
{ hom := tensorμ X.1 X.2 Y.1 Y.2
inv := tensorδ X.1 X.2 Y.1 Y.2 }
μIso_hom_natural_left := fun f Z ↦ tensorμ_natural_left f.1 f.2 Z.1 Z.2
μIso_hom_natural_right := fun Z f ↦ tensorμ_natural_right Z.1 Z.2 f.1 f.2
associativity := fun X Y Z ↦ tensor_associativity X.1 X.2 Y.1 Y.2 Z.1 Z.2
left_unitality := fun ⟨X₁, X₂⟩ ↦ tensor_left_unitality X₁ X₂
right_unitality := fun ⟨X₁, X₂⟩ ↦ tensor_right_unitality X₁ X₂ }
