Documentation

Mathlib.GroupTheory.Perm.Subgroup

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.sumCongrHom.decidableMemRange {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β] :
DecidablePred fun (x : Equiv.Perm (α β)) => x (Equiv.Perm.sumCongrHom α β).range
Equations
instance Equiv.Perm.sigmaCongrRightHom.decidableMemRange {α : Type u_1} {β : αType u_2} [DecidableEq α] [(a : α) → DecidableEq (β a)] [Fintype α] [(a : α) → Fintype (β a)] :
DecidablePred fun (x : Equiv.Perm ((a : α) × β a)) => x (Equiv.Perm.sigmaCongrRightHom β).range
Equations
@[simp]
theorem Equiv.Perm.sigmaCongrRightHom.card_range {α : Type u_1} {β : αType u_2} [Fintype (Equiv.Perm.sigmaCongrRightHom β).range] [Fintype ((a : α) → Equiv.Perm (β a))] :
instance Equiv.Perm.subtypeCongrHom.decidableMemRange {α : Type u_1} (p : αProp) [DecidablePred p] [Fintype (Equiv.Perm { a : α // p a } × Equiv.Perm { a : α // ¬p a })] [DecidableEq (Equiv.Perm α)] :
Equations
@[simp]
theorem Equiv.Perm.subtypeCongrHom.card_range {α : Type u_1} (p : αProp) [DecidablePred p] [Fintype (Equiv.Perm.subtypeCongrHom p).range] [Fintype (Equiv.Perm { a : α // p a } × Equiv.Perm { a : α // ¬p a })] :
Fintype.card (Equiv.Perm.subtypeCongrHom p).range = Fintype.card (Equiv.Perm { a : α // p a } × Equiv.Perm { a : α // ¬p a })
noncomputable def Equiv.Perm.subgroupOfMulAction (G : Type u_1) (H : Type u_2) [Group G] [MulAction G H] [FaithfulSMul G H] :
G ≃* (MulAction.toPermHom G H).range

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

Equations
Instances For