mapComp_assoc_left_hom — Mathlib

English

The left-hand associativity coherence component for a pseudofunctor is expressed by an inverse equation involving α, map, and map₂.

Русский

Левая когерентная составная ассоциации псевдофункторa задается через обратное равенство, содержащее α, map и map₂.

LaTeX

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

Lean4

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

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