Theorems · Inductive type · category theory

Action

(V : Type u_1) → [CategoryTheory.Category.{v_1, u_1} V] → (G : Type u_2) → [Monoid G] → Type (max (max u_1 u_2) v_1)

An Action V G represents a bundled action of the monoid G on an object of some category V. As an example, when V = ModuleCat R, this is an R-linear representation of G, while when V = Type this is a G-action.

Defined in

Mathlib.CategoryTheory.Action.Basic

Cited by

206 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

CategoryTheory.CategoryMonoid