whiskerLeft_μ_comp_μ — Mathlib

English

Relation expressing the interaction of μ with the associator when whiskering on the left by μ.

Русский

Отношение, выражающее взаимодействие μ с ассоциатором при отводке слева μ.

LaTeX

$$$F.obj X \\triangleright μ_Y Z \\circ μ_{F X, Y}^F Z = α^{-1}_{F X, F Y, F Z} \\circ μ_X Y \\triangleright F.obj Z \\circ μ_{X ⊗ Y} Z \\circ F.map α_{X,Y,Z}^{-1}$$$

Lean4

@[reassoc]
theorem whiskerLeft_μ_comp_μ (X Y Z : C) :
    F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z) =
      (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv ≫ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom :=
  by rw [associativity, Iso.inv_hom_id_assoc]

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