whiskerRightIso_mapId — Mathlib

English

The whiskering of mapId with map f is controlled by the left and right unitors and map₂ with left unitor corrections.

Русский

Сворачивание mapId справа с map f описывается левым и правым униторами и map₂ через левые униторы.

LaTeX

$$$\forall f:\; whiskerRightIso (F.mapId a) (F.map f) = (F.mapComp (id a) f).symm \; ≪≫\; F.map₂Iso (λ_ f) \; ≪≫\; (λ_ (F.map f)).symm$$$

Lean4

theorem whiskerRightIso_mapId (f : a ⟶ b) :
    whiskerRightIso (F.mapId a) (F.map f) = (F.mapComp (𝟙 a) f).symm ≪≫ F.map₂Iso (λ_ f) ≪≫ (λ_ (F.map f)).symm := by
  simp [mapComp_id_left]

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