mathlib documentation

group_theory.perm.subgroup

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.

source
@[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
@[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
@[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})