mapComp_assoc_left — Mathlib

English

The left associativity relationship for mapComp in an oplax functor F is expressed by a specific equation involving map₂ and associator.

Русский

Левая ассоциаторность mapComp для OplaxFunctor выражается в конкретном равенстве, содержащее map₂ и ассозиатор.

LaTeX

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

Lean4

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

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