Theorems · Definition · group theory

SubAddAction.ofFixingAddSubgroup_insert_map

{M : Type u_1} →
  {α : Type u_2} →
    [inst : AddGroup M] →
      [inst_1 : AddAction M α] →
        (a : α) →
          (s : Set ↥(SubAddAction.ofStabilizer M a)) →
            ↥(SubAddAction.ofFixingAddSubgroup M
                  (insert a (Subtype.val '' s))) →ₑ[⇑(SubAddAction.fixingAddSubgroupInsertEquiv a s)]
              ↥(SubAddAction.ofFixingAddSubgroup (↥(AddAction.stabilizer M a)) s)

The identity map of fixing additive subgroup of stabilizer into the fixing additive 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

AddGroupAddAction