mapComp_assoc_left — Mathlib

English

The left unitor at F.map f has its hom component expressed via mapId, mapComp, and map₂ in a standard shape; i.e., (λ_(F.map f)).hom equals F.mapId a ▷ F.map f ≫ F.mapComp (𝟙 a) f ≫ F.map₂ (λ_ f).hom.

Русский

У левого унитора на F.map f выражение компоненты hom через mapId, mapComp и map₂ имеет стандартную форму.

LaTeX

$$$(\lambda_ (F.map f)).hom = F.mapId a \rhd F.map f \; ∘\; F.mapComp (𝟙 a) f \; ∘\; F.map₂ (\lambda_ f).hom$$$

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 ▷ F.map h ≫ F.mapComp (f ≫ g) h =
      (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ F.mapComp g h ≫ F.mapComp f (g ≫ h) ≫ F.map₂ (α_ f g h).inv :=
  by
  rw [← F.map₂_associator_assoc, ← F.map₂_comp]
  simp only [Iso.hom_inv_id, PrelaxFunctor.map₂_id, comp_id]

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