Theorems · Theorem · category theory

Action.full_res

∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [inst_1 : Monoid G]
  [inst_2 : Monoid H] (f : G →* H), Function.Surjective ⇑f → (Action.res V f).Full

The functor from Action V H to Action V G induced by a monoid homomorphism f : G →* H is full if f is surjective.

Defined in

Mathlib.CategoryTheory.Action.Basic

Cited by

0 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryMonoidMonoid