Theorems · Definition · group theory

SubMulAction.map_ofFixingSubgroupUnion

(M : Type u_1) →
  {α : Type u_2} →
    [inst : Group M] →
      [inst_1 : MulAction M α] →
        (s t : Set α) →
          have ψ := fun m => ⟨⟨↑m, ⋯⟩, ⋯⟩;
          ↥(SubMulAction.ofFixingSubgroup M (s ∪ t)) →ₑ[ψ]
            ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t))

The identity between the iterated SubMulAction of the fixingSubgroup and the SubMulAction of the fixingSubgroup of the union, as an equivariant map.

Defined in

Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupMulAction