Theorems · Definition · group theory

SubMulAction.ofFixingSubgroup_insert_map

{M : Type u_1} →
  {α : Type u_2} →
    [inst : Group M] →
      [inst_1 : MulAction M α] →
        (a : α) →
          (s : Set ↥(SubMulAction.ofStabilizer M a)) →
            ↥(SubMulAction.ofFixingSubgroup M
                  (insert a (Subtype.val '' s))) →ₑ[⇑(SubMulAction.fixingSubgroupInsertEquiv a s)]
              ↥(SubMulAction.ofFixingSubgroup (↥(MulAction.stabilizer M a)) s)

The identity map of fixing subgroup of stabilizer into the fixing subgroup of the extended set, as an equivariant map.

Defined in

Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupMulAction