mapAction — Mathlib

English

A fully faithful functor between V and W induces a fully faithful functor between Action V G and Action W G.

Русский

Полностью верный функтор между V и W индуцирует полнофидельный функтор между Action V G и Action W G.

LaTeX

$$FullyFaithful.mapAction {F : V ⥤ W} (h : F.FullyFaithful) (G : Type*) [Monoid G] : (F.mapAction G).FullyFaithful$$

Lean4

/-- A fully faithful functor between categories induces a fully faithful functor between
the categories of `G`-actions within those categories. -/
def mapAction {F : V ⥤ W} (h : F.FullyFaithful) (G : Type*) [Monoid G] : (F.mapAction G).FullyFaithful where
  preimage
    f := by
    refine ⟨h.preimage f.hom, fun _ ↦ h.map_injective ?_⟩
    simp only [map_comp, map_preimage]
    exact f.comm _

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