associator_naturality — Mathlib

English

The associator is natural with respect to morphisms, expressing coherence of associativity under morphisms.

Русский

Ассоциатор естествен по отношению к морфизмам, выражая согласованность ассоциативности под морфизмами.

LaTeX

$$$\text{naturality of }(\alpha) : \, (\text{tensorHom}(\text{tensorHom}(f_1,f_2),f_3)) \circ (\text{associator}^Y) = (\text{associator}^X) \circ \text{tensorHom}(f_1,\text{tensorHom}(f_2,f_3))$$$

Lean4

theorem associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : Dial C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
    tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom =
      (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃) :=
  by cat_disch

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