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.

In particular, we prove Cayley's theorem in Equiv.Perm.subgroupOfMulAction: every group G is isomorphic to a subgroup of the symmetric group acting on G.

instance Equiv.Perm.sumCongrHom.decidableMemRange {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β] : DecidablePred fun (x : Perm (α ⊕ β)) => x ∈ (sumCongrHom α β).range

Equations

• Equiv.Perm.sumCongrHom.decidableMemRange x✝ = inferInstance

@[simp]

theorem Equiv.Perm.sumCongrHom.card_range {α : Type u_1} {β : Type u_2} [Fintype ↥(sumCongrHom α β).range] [Fintype (Perm α × Perm β)] : Fintype.card ↥(sumCongrHom α β).range = Fintype.card (Perm α × Perm β)

instance Equiv.Perm.sigmaCongrRightHom.decidableMemRange {α : Type u_1} {β : α → Type u_2} [DecidableEq α] [(a : α) → DecidableEq (β a)] [Fintype α] [(a : α) → Fintype (β a)] : DecidablePred fun (x : Perm ((a : α) × β a)) => x ∈ (sigmaCongrRightHom β).range

Equations

• Equiv.Perm.sigmaCongrRightHom.decidableMemRange x✝ = inferInstance

@[simp]

theorem Equiv.Perm.sigmaCongrRightHom.card_range {α : Type u_1} {β : α → Type u_2} [Fintype ↥(sigmaCongrRightHom β).range] [Fintype ((a : α) → Perm (β a))] : Fintype.card ↥(sigmaCongrRightHom β).range = Fintype.card ((a : α) → Perm (β a))

instance Equiv.Perm.subtypeCongrHom.decidableMemRange {α : Type u_1} (p : α → Prop) [DecidablePred p] [Fintype (Perm { a : α // p a } × Perm { a : α // ¬p a })] [DecidableEq (Perm α)] : DecidablePred fun (x : Perm α) => x ∈ (subtypeCongrHom p).range

Equations

• Equiv.Perm.subtypeCongrHom.decidableMemRange p x✝ = inferInstance

@[simp]

theorem Equiv.Perm.subtypeCongrHom.card_range {α : Type u_1} (p : α → Prop) [DecidablePred p] [Fintype ↥(subtypeCongrHom p).range] [Fintype (Perm { a : α // p a } × Perm { a : α // ¬p a })] : Fintype.card ↥(subtypeCongrHom p).range = Fintype.card (Perm { a : α // p a } × 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

• Equiv.Perm.subgroupOfMulAction G H = MulEquiv.ofLeftInverse' (MulAction.toPermHom G H) ⋯