mapComp_assoc_right — Mathlib

English

The right unitor at F.map f has its hom component expressed similarly through mapId and map₂ with the right unitor; i.e., (ρ_(F.map f)).hom equals F.map f ◁ F.mapId b ≫ F.mapComp f (𝟙 b) ≫ F.map₂ (ρ_ f).hom.

Русский

Правая единичная константа на F.map f имеет вид через mapId и map₂ с правым унитором.

LaTeX

$$$(\rho_(F.map f)).hom = F.map f ◁ F.mapId b ≫ F.mapComp f (𝟙 b) ≫ F.map₂ (\rho_ f).hom$$

Lean4

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

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