Theorems · Definition · group theory

SubAddAction.ofStabilizer.conjMap

{G : Type u_3} →
  [inst : AddGroup G] →
    {α : Type u_4} →
      [inst_1 : AddAction G α] →
        {g : G} →
          {a b : α} →
            (hg : b = g +ᵥ a) →
              ↥(SubAddAction.ofStabilizer G a) →ₑ[⇑(AddAction.stabilizerEquivStabilizer hg)]
                ↥(SubAddAction.ofStabilizer G b)

Conjugation induces an equivariant map between the SubAddAction 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 32 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupAddAction