instFullActionMapActionOfFaithful

English

Let F: V → W be a functor that is full and faithful, and let G be a monoid. Then the induced functor mapAction G : Action V G → Action W G is full; i.e., every morphism between F.mapAction G X and F.mapAction G Y arises from a morphism X → Y in V via F.mapAction G.

Русский

Пусть F: V → W — функтор, полный и точный, и пусть G — моноид. Тогда порожденный функтор mapAction G: Action V G → Action W G полно; то есть любой мороморфизм между F.mapAction G X и F.mapAction G Y восходит к мороморфизму X → Y в V через F.mapAction G.

LaTeX

$$$Full((F.mapAction G))$$$

Lean4

instance (F : V ⥤ W) (G : Type*) [Monoid G] [F.Faithful] [F.Full] : (F.mapAction G).Full :=
  ((Functor.FullyFaithful.ofFullyFaithful F).mapAction G).full

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