mapComp_assoc_right — Mathlib

English

For an oplax functor F and arrows f,g,h, the right associativity of mapComp aligns with the associator and map₂, giving a coherence equation.

Русский

Для_OPLAX-функторa F и стрел f,g,h, правая ассоциаторность mapComp согласуется с ассозиатором и map₂ и образует когерентное равенство.

LaTeX

$$$ F.mapComp f (g ≫ h) \; ≫ \; F.map f ◁ F.mapComp g h = F.map₂ (α_ f g h).inv ≫ F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h ≫ F.map₂ (α_ f g h).hom $$$

Lean4

@[reassoc, to_app]
theorem mapComp_assoc_right {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
    F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h =
      F.map₂ (α_ f g h).inv ≫ F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h ≫ (α_ (F.map f) (F.map g) (F.map h)).hom :=
  by
  rw [← F.map₂_associator, ← F.map₂_comp_assoc]
  simp

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