Theorems · Definition · category theory

CategoryTheory.ActionCategory.stabilizerIsoEnd

(M : Type u_1) →
  [inst : Monoid M] →
    {X : Type u} →
      [inst_1 : MulAction M X] → (x : X) → ↥(MulAction.stabilizerSubmonoid M x) ≃* CategoryTheory.End ⟨(), x⟩

The stabilizer of a point is isomorphic to the endomorphism monoid at the corresponding point. In fact they are definitionally equivalent.

Defined in

Mathlib.CategoryTheory.Action

Cited by

2 results in Mathlib

Foundations

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

Assumes

MonoidMulAction