Lemmas about subgroups within the permutations (self-equivalences) of a type α #

This file provides extra lemmas about some Subgroups that exist within Equiv.Perm α. GroupTheory.Subgroup depends on GroupTheory.Perm.Basic, so these need to be in a separate file.

It also provides decidable instances on membership in these subgroups, since MonoidHom.decidableMemRange cannot be inferred without the help of a lambda. The presence of these instances induces a Fintype instance on the QuotientGroup.Quotient of these subgroups.

instance Equiv.Perm.sigmaCongrRightHom.decidableMemRange {α : Type u_1} {β : αType u_2} [DecidableEq α] [(a : α) → DecidableEq (β a)] [Fintype α] [(a : α) → Fintype (β a)] :
noncomputable def Equiv.Perm.subgroupOfMulAction (G : Type u_1) (H : Type u_2) [Group G] [MulAction G H] [FaithfulSMul G H] :

Cayley's theorem: Every group G is isomorphic to a subgroup of the symmetric group acting on G. Note that we generalize this to an arbitrary "faithful" group action by G. Setting H = G recovers the usual statement of Cayley's theorem via RightCancelMonoid.faithfulSMul

Instances For