English
The tensor morphisms μ and δ satisfy standard coherence laws ensuring the compatibility of tensor product with associativity and braiding in a monoidal braided category.
Русский
Морфизмы μ и δ удовлетворяют стандартным законам когерентности, обеспечивая совместимость тензорного произведения с ассоциативностью и braiding в моноидальной браидированной категории.
LaTeX
$$$$ tensorδ X_1 X_2 Y_1 Y_2 \;\circ\; tensorμ X_1 X_2 Y_1 Y_2 = id, $$$$
Lean4
@[reassoc]
theorem tensorμ_natural {X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : U₁ ⟶ V₁) (g₂ : U₂ ⟶ V₂) :
((f₁ ⊗ₘ f₂) ⊗ₘ g₁ ⊗ₘ g₂) ≫ tensorμ Y₁ Y₂ V₁ V₂ = tensorμ X₁ X₂ U₁ U₂ ≫ ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂) :=
by
dsimp only [tensorμ]
simp_rw [← id_tensorHom, ← tensorHom_id]
slice_lhs 1 2 => rw [associator_naturality]
slice_lhs 2 3 =>
rw [tensorHom_comp_tensorHom, comp_id f₁, ← id_comp f₁, associator_inv_naturality, ← tensorHom_comp_tensorHom]
slice_lhs 3 4 =>
rw [tensorHom_comp_tensorHom, tensorHom_comp_tensorHom, comp_id f₁, ← id_comp f₁, comp_id g₂, ← id_comp g₂,
braiding_naturality, ← tensorHom_comp_tensorHom, ← tensorHom_comp_tensorHom]
slice_lhs 4 5 =>
rw [tensorHom_comp_tensorHom, comp_id f₁, ← id_comp f₁, associator_naturality, ← tensorHom_comp_tensorHom]
slice_lhs 5 6 => rw [associator_inv_naturality]
simp only [assoc]
