mapComp_assoc_right_hom — Mathlib

English

For a pseudofunctor F and arrows f,g,h, the right-associated mapComp 2-cells satisfy a coherence identity that relates α and the associator as shown.

Русский

Для псевдофункторa F и стрелок f,g,h выполняется когерентивная тождественность справа, связывающая mapComp, α и ассоциатор.

LaTeX

$$$\forall f,g,h,\; (F.mapComp f (g \gg h)).hom \; ≫ \; F.map f \; ◁ \; (F.mapComp g h).hom = F.map₂(\alpha_{f,g,h}.\text{inv}) \; ≫ \; (F.mapComp (f \gg g) h).hom \; ≫ \; (F.mapComp f g).hom \; ◁ \; F.map h \; ≫ \; (\alpha_{F.map f,F.map g,F.map h}.\text{hom})$$$

Lean4

@[to_app (attr := reassoc)]
theorem mapComp_assoc_right_hom {c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
    (F.mapComp f (g ≫ h)).hom ≫ F.map f ◁ (F.mapComp g h).hom =
      F.map₂ (α_ f g h).inv ≫
        (F.mapComp (f ≫ g) h).hom ≫ (F.mapComp f g).hom ▷ F.map h ≫ (α_ (F.map f) (F.map g) (F.map h)).hom :=
  F.toOplax.mapComp_assoc_right _ _ _

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