whisker_assoc — Mathlib

English

For X, morphism f: Y → Y' and Z, the whiskerRight of whiskerLeft by X commutes with associator: (X ◁ f) ▷ Z = (α_{X Y Z}).hom ≫ X ◁ f ▷ Z ≫ (α_{X Y' Z}).inv.

Русский

Пусть X и f: Y → Y', Z. Обёртка справа от обёртки слева через X коммутирует с ассоциатором: (X ◁ f) ▷ Z = (α_{X Y Z}).hom ≫ X ◁ f ▷ Z ≫ (α_{X Y' Z}).inv.

LaTeX

$$$ (X \\triangleleft f) \\triangleright Z = (\\alpha_{X Y Z}).hom \\circ (X \\triangleleft f \\triangleright Z) \\circ (\\alpha_{X Y' Z}).inv $$$

Lean4

@[reassoc, simp]
theorem whisker_assoc (X : C) {Y Y' : C} (f : Y ⟶ Y') (Z : C) :
    (X ◁ f) ▷ Z = (α_ X Y Z).hom ≫ X ◁ f ▷ Z ≫ (α_ X Y' Z).inv :=
  by
  simp only [← id_tensorHom, ← tensorHom_id]
  rw [← assoc, ← associator_naturality]
  simp

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