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.
@[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
- equiv.perm.sum_congr_hom.decidable_mem_range = λ (x : equiv.perm (α ⊕ β)), infer_instance
@[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 β)
@[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
- equiv.perm.sigma_congr_right_hom.decidable_mem_range = λ (x : equiv.perm (Σ (a : α), β a)), infer_instance
@[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))
@[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
@[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})
def
equiv.perm.subgroup_of_mul_action
(G : Type u_1)
(H : Type u_2)
[group G]
[mul_action G H]
[has_faithful_scalar 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_scalar