mapActionCongr — Mathlib

English

If e : F ≅ F' is an isomorphism of functors, then there is an isomorphism between the corresponding action functors: F.mapAction G ≅ F'.mapAction G.

Русский

Если e : F ≅ F' — это изоморфизм функторов, то соответствующие отображения действий дают изоморфизм F.mapAction G ≅ F'.mapAction G.

LaTeX

$$$F.mapAction G \cong F'.mapAction G$$$

Lean4

/-- `Functor.mapAction` preserves isomorphisms of functors. -/
@[simps! hom inv]
def mapActionCongr {F F' : V ⥤ W} (e : F ≅ F') : F.mapAction G ≅ F'.mapAction G :=
  NatIso.ofComponents (fun X ↦ Action.mkIso (e.app X.V))

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