map_associator — Mathlib

English

The inverse of the left unitor image under F equals a composite of the left unitor in the target, whiskering with η, and μ.

Русский

Обратный образ левого унитора под F равен композиции левого унитора в целевом, усечениям η и μ.

LaTeX

$$$$ F(\\lambda_X)^{-1} = \\lambda_{F X}^{-1} \\circ (\\varepsilon F \\triangleright F X) \\circ μ F(I,X) $$$$

Lean4

@[reassoc]
theorem map_associator (X Y Z : C) :
    F.map (α_ X Y Z).hom =
      δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z) :=
  by rw [← LaxMonoidal.associativity F, whiskerRight_δ_μ_assoc, δ_μ_assoc]

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