mapComp'_comp_mapComp'_whiskerRight

English

A second coherence identity for a lax functor: the whiskered compositions satisfy a pennant-type equation with the associator.

Русский

Вторая связность для лаксового функтора: составления с учетом обвешивания удовлетворяют уравнению типа «флажок» с ассоциатором.

LaTeX

$$$F.mapComp' f_{02} f_{23} f \\\\mapsto F.mapComp' f_{01} f_{13} f \\\\mapsto (\\\\alpha)^{ -1}$$$

Lean4

@[reassoc]
theorem mapComp'_comp_mapComp'_whiskerRight (hf : f₀₂ ≫ f₂₃ = f) :
    F.mapComp' f₀₂ f₂₃ f ≫ F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ =
      F.mapComp' f₀₁ f₁₃ f ≫ F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃ ≫ (α_ _ _ _).inv :=
  by
  rw [F.mapComp'_comp_whiskerLeft_mapComp'_assoc _ _ _ _ _ f h₀₂ h₁₃ (by cat_disch)]
  simp

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