Theorems · Definition · category theory

Action.forget

(V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    (G : Type u_2) → [inst_1 : Monoid G] → CategoryTheory.Functor (Action V G) V

(implementation) The forgetful functor from bundled actions to the underlying objects. Use the CategoryTheory.forget API provided by the ConcreteCategory instance below, rather than using this directly.

Defined in

Mathlib.CategoryTheory.Action.Basic

Cited by

17 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryMonoid