mathlib documentation

group_theory.perm.subgroup

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
@[protected, instance]
def equiv.perm.sum_congr_hom.decidable_mem_range {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :
decidable_pred (λ (_x : equiv.perm (α ⊕ β)), _x ∈ (equiv.perm.sum_congr_hom α β).range)
Equations
source
@[simp]
theorem equiv.perm.sum_congr_hom.card_range {α : Type u_1} {β : Type u_2} [fintype ↥((equiv.perm.sum_congr_hom α β).range)] [fintype (equiv.perm α × equiv.perm β)] :
fintype.card ↥((equiv.perm.sum_congr_hom α β).range) = fintype.card (equiv.perm α × equiv.perm β)
source
@[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)
Equations
source
@[simp]
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))] :
fintype.card ↥((equiv.perm.sigma_congr_right_hom β).range) = fintype.card (Π (a : α), equiv.perm (β a))
source
@[protected, instance]
def equiv.perm.subtype_congr_hom.decidable_mem_range {α : Type u_1} (p : α → Prop) [decidable_pred p] [fintype (equiv.perm {a // p a} × equiv.perm {a // ¬p a})] [decidable_eq (equiv.perm α)] :
decidable_pred (λ (_x : equiv.perm α), _x ∈ (equiv.perm.subtype_congr_hom p).range)
Equations
source
@[simp]
theorem equiv.perm.subtype_congr_hom.card_range {α : Type u_1} (p : α → Prop) [decidable_pred p] [fintype ↥((equiv.perm.subtype_congr_hom p).range)] [fintype (equiv.perm {a // p a} × equiv.perm {a // ¬p a})] :
fintype.card ↥((equiv.perm.subtype_congr_hom p).range) = fintype.card (equiv.perm {a // p a} × equiv.perm {a // ¬p a})
source
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] :
G ≃* ↥((mul_action.to_perm_hom 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 right_cancel_monoid.to_has_faithful_smul

Equations