Theorems · Definition · category theory

CategoryTheory.ActionCategory.back

{M : Type u_1} → [inst : Monoid M] → {X : Type u} → [inst_1 : MulAction M X] → CategoryTheory.ActionCategory M X → X

The canonical map ActionCategory M X → X. It is given by fun x => x.snd, but has a more explicit type.

Defined in

Mathlib.CategoryTheory.Action

Cited by

4 results in Mathlib

Foundations

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

Assumes

MonoidMulAction