mapComp_id_left — Mathlib

English

The left unit property of mapComp for an identity morphism: the equation expresses that F.mapComp (id a) f combined with F.mapId a and the left unitor reduces to the left-unitor expression via map₂.

Русский

Слева единичная свойства для mapComp с id: выражение F.mapComp (id a) f объединенное с F.mapId a и левым унитором сводится к выражению через map₂.

LaTeX

$$$ F.mapComp (id a) f ≫ F.mapId a ▷ F.map f = F.map₂ (λ_ f).hom ≫ (λ_ (F.map f)).inv $$$

Lean4

@[reassoc]
theorem mapComp_id_left {a b : B} (f : a ⟶ b) :
    F.mapComp (𝟙 a) f ≫ F.mapId a ▷ F.map f = F.map₂ (λ_ f).hom ≫ (λ_ (F.map f)).inv :=
  by
  rw [Iso.eq_comp_inv]
  simp only [Category.assoc]
  rw [← F.map₂_leftUnitor]

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