English
A coherence identity for composing tensor morphisms and μ maps in a braided setting, ensuring that two nested compositions yield the same morphism after applying naturality and pentagon relations.
Русский
Когерентность композиции тензорных морфизмов и μ в braided-среде: две вложенные композиции совпадают после применения натуралистики и пентагональных соотношений.
LaTeX
$$$$ (tensorμ (F.W) (F.X) (F.Y) (F.Z)) ≫ (μ F W Y ⊗_m μ F X Z) ≫ μ F (W ⊗ Y) (X ⊗ Z) = (μ F W X ⊗_m μ F Y Z) ≫ μ F (W ⊗ X) (Y ⊗ Z) ≫ F.map (tensorμ W X Y Z). $$$$
Lean4
@[reassoc]
theorem leftUnitor_monoidal (X₁ X₂ : C) :
(λ_ X₁).hom ⊗ₘ (λ_ X₂).hom = tensorμ (𝟙_ C) X₁ (𝟙_ C) X₂ ≫ ((λ_ (𝟙_ C)).hom ▷ (X₁ ⊗ X₂)) ≫ (λ_ (X₁ ⊗ X₂)).hom :=
by
dsimp only [tensorμ]
have :
(λ_ X₁).hom ⊗ₘ (λ_ X₂).hom =
(α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).hom ≫
(𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).inv) ≫ (λ_ ((X₁ ⊗ 𝟙_ C) ⊗ X₂)).hom ≫ ((ρ_ X₁).hom ▷ X₂) :=
by monoidal
rw [this]; clear this
rw [← braiding_leftUnitor]
monoidal
