Theorems · Definition · group theory

SubMulAction.ofStabilizer.conjMap

{G : Type u_1} →
  [inst : Group G] →
    {α : Type u_2} →
      [inst_1 : MulAction G α] →
        {g : G} →
          {a b : α} →
            (hg : b = g • a) →
              ↥(SubMulAction.ofStabilizer G a) →ₑ[⇑(MulAction.stabilizerEquivStabilizer hg)]
                ↥(SubMulAction.ofStabilizer G b)

Conjugation induces an equivariant map between the SubMulAction of the stabilizer of a point and that of its translate.

Defined in

Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Cited by

6 results in Mathlib

Foundations

Depth 31 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupMulAction