map₂_rightUnitor_hom — Mathlib

English

The left unitor at F.map f has its hom component given by the formula in terms of mapId, mapComp, and map₂, matching the standard Lefthand unitor form for Lax functors.

Русский

Левый унитор на F.map f имеет гом-компонент согласно формуле через mapId, mapComp и map₂, соответствуя стандартной форме для LaxFunctor.

LaTeX

$$$ (\lambda_ (F.map f)).hom = F.mapId a \; \triangleright \; F.map f ≫ F.mapComp (𝟙 a) f ≫ F.map₂ (λ_ f).hom $$$

Lean4

@[reassoc, to_app]
theorem map₂_rightUnitor_hom {a b : B} (f : a ⟶ b) :
    (ρ_ (F.map f)).hom = F.map f ◁ F.mapId b ≫ F.mapComp f (𝟙 b) ≫ 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₂_rightUnitor]

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