mapComp_id_left — Mathlib

English

Right side coherence: the image of the right unitor under mapComp is described by the right unitor and associativity data.

Русский

Правая когеренция: образ правого унитора через mapComp описывается правым унитором и данными ассоциатора.

LaTeX

$$$\forall f:\; (F.mapComp f (id b)).hom = F.map₂(ρ_ f).hom ≫ (ρ_{F.map f}).inv ≫ F.map f ◁ (F.mapId b).inv$$$

Lean4

theorem mapComp_id_left (f : a ⟶ b) :
    (F.mapComp (𝟙 a) f) = F.map₂Iso (λ_ f) ≪≫ (λ_ (F.map f)).symm ≪≫ (whiskerRightIso (F.mapId a) (F.map f)).symm :=
  Iso.ext <| F.mapComp_id_left_hom f

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