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 ∈ MonoidHom.range (Equiv.Perm.sumCongrHom α β)

Equations

• Equiv.Perm.sumCongrHom.decidableMemRange x = inferInstance

@[simp]

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

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 ∈ MonoidHom.range (Equiv.Perm.sigmaCongrRightHom β)

Equations

• Equiv.Perm.sigmaCongrRightHom.decidableMemRange x = inferInstance

@[simp]

theorem Equiv.Perm.sigmaCongrRightHom.card_range {α : Type u_1} {β : α → Type u_2} [Fintype ↥(MonoidHom.range (Equiv.Perm.sigmaCongrRightHom β))] [Fintype ((a : α) → Equiv.Perm (β a))] : Fintype.card ↥(MonoidHom.range (Equiv.Perm.sigmaCongrRightHom β)) = Fintype.card ((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 α)] : DecidablePred fun (x : Equiv.Perm α) => x ∈ MonoidHom.range (Equiv.Perm.subtypeCongrHom p)

Equations

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

@[simp]

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

Equations

• One or more equations did not get rendered due to their size.