mapActionComp — Mathlib

English

MapAction is functorial in the functor: there is a natural isomorphism between ((F ⋙ F').mapAction G) and (F.mapAction G ⋙ F'.mapAction G).

Русский

MapAction тривиален по отношению к функтору: существует естественное изоморфизм между ((F ⋙ F').mapAction G) и (F.mapAction G ⋙ F'.mapAction G).

LaTeX

$$$ (F \circ F').mapAction G \cong (F.mapAction G) \circ (F'.mapAction G) $$$

Lean4

/-- `Functor.mapAction` is functorial in the functor. -/
@[simps! hom inv]
def mapActionComp {T : Type*} [Category T] (F : V ⥤ W) (F' : W ⥤ T) :
    (F ⋙ F').mapAction G ≅ F.mapAction G ⋙ F'.mapAction G :=
  NatIso.ofComponents (fun X ↦ Iso.refl _)

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