mapComp_id_right — Mathlib

English

The right unit property of mapComp for an identity morphism: the equation expresses that F.mapComp f (id b) together with F.map f and F.mapId b equals the right unitor via map₂.

Русский

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

LaTeX

$$$ F.mapComp f (id b) ≫ F.map f ◁ F.mapId b = F.map₂ (ρ_ f).hom ≫ (ρ_ (F.map f)).inv $$$

Lean4

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

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