mathlib documentation


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

This file provides extra lemmas about some subgroups that exist within equiv.perm α. group_theory.subgroup depends on group_theory.perm.basic, so these need to be in a separate file.

It also provides decidable instances on membership in these subgroups, since monoid_hom.decidable_mem_range cannot be inferred without the help of a lambda. The presence of these instances induces a fintype instance on the quotient_group.quotient of these subgroups.

@[protected, instance]
def equiv.perm.sum_congr_hom.decidable_mem_range {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :
@[protected, instance]
def equiv.perm.sigma_congr_right_hom.decidable_mem_range {α : Type u_1} {β : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (β a)] [fintype α] [Π (a : α), fintype (β a)] :
decidable_pred (λ (_x : equiv.perm (Σ (a : α), β a)), _x (equiv.perm.sigma_congr_right_hom β).range)
theorem equiv.perm.sigma_congr_right_hom.card_range {α : Type u_1} {β : α → Type u_2} [fintype ((equiv.perm.sigma_congr_right_hom β).range)] [fintype (Π (a : α), equiv.perm (β a))] :
noncomputable def equiv.perm.subgroup_of_mul_action (G : Type u_1) (H : Type u_2) [group G] [mul_action G H] [has_faithful_smul 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 right_cancel_monoid.to_has_faithful_smul