associator_naturality — Mathlib

English

The associator is natural with respect to maps f1,f2,f3: prod.map (prod.map f1 f2) f3 ≫ associator Y1 Y2 Y3.hom = associator X1 X2 X3.hom ≫ prod.map f1 (prod.map f2 f3).

Русский

Ассоциатор естествен по отображениям f1,f2,f3: естественность ассоциатора по композициям.

LaTeX

$$$\forall f_1: X_1\to Y_1, f_2: X_2\to Y_2, f_3: X_3\to Y_3,\; prod.map (prod.map f_1 f_2) f_3 ≫ assoc_{Y_1,Y_2,Y_3}.hom = assoc_{X_1,X_2,X_3}.hom ≫ prod.map f_1 (prod.map f_2 f_3).hom$$$

Lean4

@[reassoc]
theorem associator_naturality [HasBinaryProducts C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂)
    (f₃ : X₃ ⟶ Y₃) :
    prod.map (prod.map f₁ f₂) f₃ ≫ (prod.associator Y₁ Y₂ Y₃).hom =
      (prod.associator X₁ X₂ X₃).hom ≫ prod.map f₁ (prod.map f₂ f₃) :=
  by simp

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