mapComp_assoc_right_inv — Mathlib

English

Inverse form of mapComp assoc left-hom equation with α and map₂.

Русский

Обратная форма левой ассоциации для mapComp с α и map₂.

LaTeX

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

Lean4

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

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