associator_naturality — Mathlib

English

For all f1, f2, f3, the naturality of coprod.associator expresses that the reshuffling of coproducts commutes with applying morphisms F.map.

Русский

Для всех f1, f2, f3 естественность копрод-ассоциатора выражает, что перераспределение копродуктов коммутирует с применением отображений F.map.

LaTeX

$$$ \\operatorname{coprod.map} (\\operatorname{coprod.map} f_1 f_2) f_3 \\circ (\\operatorname{coprod.associator} Y_1 Y_2 Y_3).hom = (\\operatorname{coprod.associator} X_1 X_2 X_3).hom \\circ \\operatorname{coprod.map} f_1 (\\operatorname{coprod.map} f_2 f_3) $$$

Lean4

theorem associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
    coprod.map (coprod.map f₁ f₂) f₃ ≫ (coprod.associator Y₁ Y₂ Y₃).hom =
      (coprod.associator X₁ X₂ X₃).hom ≫ coprod.map f₁ (coprod.map f₂ f₃) :=
  by simp

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