μ_whiskerRight_comp_μ — Mathlib

English

Coherence of μ under whiskering on the right, expressing associativity of μ with the tensor product after applying F.

Русский

Согласованность μ при отводке вправо, выражающая ассоциативность μ с тензором после применения F.

LaTeX

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

Lean4

@[reassoc]
theorem μ_whiskerRight_comp_μ (X Y Z : C) :
    μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z =
      (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z) ≫ F.map (α_ X Y Z).inv :=
  by rw [← associativity_assoc, ← F.map_comp, Iso.hom_inv_id, map_id, Category.comp_id]

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