instFaithfulActionMapAction — Mathlib

English

There is a faithful instance for the mapAction functor of a faithful functor F.

Русский

Существует верный инстанс для отображения Action через F.

LaTeX

$$instance (F : V ⥤ W) (G) [Monoid G] [F.Faithful] : (F.mapAction G).Faithful$$

Lean4

instance (F : V ⥤ W) (G : Type*) [Monoid G] [F.Faithful] : (F.mapAction G).Faithful where
  map_injective
    eq := by
    ext
    apply_fun (fun f ↦ f.hom) at eq
    exact F.map_injective eq

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