map₂_leftUnitor_hom — Mathlib

English

For arrows f,g,fg with hfg, the second naturality condition of mapComp' holds: the right-hand side reduces to (F.map fg).map a via the naturality isomorphism.

Русский

Для стрел f,g,fg и hfg выполняется вторая естественность mapComp' — как правый член диаграммы сводится к (F.map fg).map a через естественность изоморфизма.

LaTeX

$$$ (F.mapComp' f g fg hfg).hom.app X ≫ (F.map g).map ((F.map f).map a) ≫ (F.mapComp' f g fg hfg).inv.app Y = (F.map fg).map a $$$

Lean4

@[reassoc, to_app]
theorem map₂_leftUnitor_hom {a b : B} (f : a ⟶ b) :
    (λ_ (F.map f)).hom = F.mapId a ▷ F.map f ≫ F.mapComp (𝟙 a) f ≫ F.map₂ (λ_ f).hom :=
  by
  rw [← PrelaxFunctor.map₂Iso_hom, ← assoc, ← Iso.comp_inv_eq, ← Iso.eq_inv_comp]
  simp only [Functor.mapIso_inv, PrelaxFunctor.mapFunctor_map, map₂_leftUnitor]

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