associator_naturality₂ — Mathlib

English

Natural compatibility of associator under mixed whiskering.

Русский

Естественная совместимость ассоциатора при смешанном whisker.

LaTeX

$$$(\\alpha_{X_1 X_2 X_3})^{hom} \\circ (X_1 \\wr (X_2 \\wr f_3)) = (\\alpha_{X_1 X_2 X_3})^{hom} \\circ ((X_1 \\wr X_2) \\wr f_3)$$$

Lean4

@[reassoc]
theorem associator_naturality₂ {X₁ X₂ X₃ Y₂ : LocalizedMonoidal L W ε} (f₂ : X₂ ⟶ Y₂) :
    ((X₁ ◁ f₂) ▷ X₃) ≫ (α_ X₁ Y₂ X₃).hom = (α_ X₁ X₂ X₃).hom ≫ (X₁ ◁ (f₂ ▷ X₃)) := by
  simp only [← tensorHom_id, ← id_tensorHom, associator_naturality]

Похожие утверждения