# mathlib3documentation

group_theory.group_action.quotient

# Properties of group actions involving quotient groups #

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

This file proves properties of group actions which use the quotient group construction, notably

• the orbit-stabilizer theorem card_orbit_mul_card_stabilizer_eq_card_group
• the class formula card_eq_sum_card_group_div_card_stabilizer'
• Burnside's lemma sum_card_fixed_by_eq_card_orbits_mul_card_group
@[class]
structure mul_action.quotient_action {α : Type u} (β : Type v) [group α] [monoid β] [ α] (H : subgroup α) :
Prop

A typeclass for when a mul_action β α descends to the quotient α ⧸ H.

Instances of this typeclass
@[class]
Prop

A typeclass for when an add_action β α descends to the quotient α ⧸ H.

Instances of this typeclass
@[protected, instance]
def mul_action.left_quotient_action {α : Type u} [group α] (H : subgroup α) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
def mul_action.right_quotient_action {α : Type u} [group α] (H : subgroup α) :
@[protected, instance]
@[protected, instance]
def mul_action.right_quotient_action' {α : Type u} [group α] (H : subgroup α) [hH : H.normal] :
@[protected, instance]
H)
Equations
@[protected, instance]
def mul_action.quotient {α : Type u} (β : Type v) [group α] [monoid β] [ α] (H : subgroup α)  :
H)
Equations
@[simp]
theorem mul_action.quotient.smul_mk {α : Type u} {β : Type v} [group α] [monoid β] [ α] (H : subgroup α) (b : β) (a : α) :
@[simp]
@[simp]
theorem mul_action.quotient.smul_coe {α : Type u} {β : Type v} [group α] [monoid β] [ α] (H : subgroup α) (b : β) (a : α) :
b a = (b a)
@[simp]
b +ᵥ a = (b +ᵥ a)
@[simp]
theorem mul_action.quotient.mk_smul_out' {α : Type u} {β : Type v} [group α] [monoid β] [ α] (H : subgroup α) (b : β) (q : α H) :
= b q
@[simp]
theorem add_action.quotient.mk_vadd_out' {α : Type u} {β : Type v} [add_group α] [add_monoid β] [ α] (H : add_subgroup α) (b : β) (q : α H) :
= b +ᵥ q
@[simp]
theorem mul_action.quotient.coe_smul_out' {α : Type u} {β : Type v} [group α] [monoid β] [ α] (H : subgroup α) (b : β) (q : α H) :
(b = b q
@[simp]
theorem add_action.quotient.coe_vadd_out' {α : Type u} {β : Type v} [add_group α] [add_monoid β] [ α] (H : add_subgroup α) (b : β) (q : α H) :
(b +ᵥ = b +ᵥ q
theorem quotient_group.out'_conj_pow_minimal_period_mem {α : Type u} [group α] (H : subgroup α) (a : α) (q : α H) :
def mul_action_hom.to_quotient {α : Type u} [group α] (H : subgroup α) :
α →[α] α H

The canonical map to the left cosets.

Equations
@[simp]
theorem mul_action_hom.to_quotient_apply {α : Type u} [group α] (H : subgroup α) (g : α) :
@[protected, instance]
def mul_action.mul_left_cosets_comp_subtype_val {α : Type u} [group α] (H I : subgroup α) :
H)
Equations
@[protected, instance]
Equations
def add_action.of_quotient_stabilizer (α : Type u) {β : Type v} [add_group α] [ β] (x : β) (g : α ) :
β

The canonical map from the quotient of the stabilizer to the set.

Equations
• = (λ (_x : α), _x +ᵥ x) _
def mul_action.of_quotient_stabilizer (α : Type u) {β : Type v} [group α] [ β] (x : β) (g : α ) :
β

The canonical map from the quotient of the stabilizer to the set.

Equations
• = (λ (_x : α), _x x) _
@[simp]
theorem add_action.of_quotient_stabilizer_mk (α : Type u) {β : Type v} [add_group α] [ β] (x : β) (g : α) :
@[simp]
theorem mul_action.of_quotient_stabilizer_mk (α : Type u) {β : Type v} [group α] [ β] (x : β) (g : α) :
= g x
theorem mul_action.of_quotient_stabilizer_mem_orbit (α : Type u) {β : Type v} [group α] [ β] (x : β) (g : α ) :
theorem add_action.of_quotient_stabilizer_mem_orbit (α : Type u) {β : Type v} [add_group α] [ β] (x : β) (g : α ) :
theorem add_action.of_quotient_stabilizer_vadd (α : Type u) {β : Type v} [add_group α] [ β] (x : β) (g : α) (g' : α ) :
(g +ᵥ g') =
theorem mul_action.of_quotient_stabilizer_smul (α : Type u) {β : Type v} [group α] [ β] (x : β) (g : α) (g' : α ) :
(g g') =
theorem mul_action.injective_of_quotient_stabilizer (α : Type u) {β : Type v} [group α] [ β] (x : β) :
theorem add_action.injective_of_quotient_stabilizer (α : Type u) {β : Type v} [add_group α] [ β] (x : β) :
noncomputable def add_action.orbit_equiv_quotient_stabilizer (α : Type u) {β : Type v} [add_group α] [ β] (b : β) :
b)

Orbit-stabilizer theorem.

Equations
noncomputable def mul_action.orbit_equiv_quotient_stabilizer (α : Type u) {β : Type v} [group α] [ β] (b : β) :
b)

Orbit-stabilizer theorem.

Equations
noncomputable def add_action.orbit_sum_stabilizer_equiv_add_group (α : Type u) {β : Type v} [add_group α] [ β] (b : β) :
b) × α

Orbit-stabilizer theorem.

Equations
noncomputable def mul_action.orbit_prod_stabilizer_equiv_group (α : Type u) {β : Type v} [group α] [ β] (b : β) :
b) × α

Orbit-stabilizer theorem.

Equations
theorem add_action.card_orbit_add_card_stabilizer_eq_card_add_group (α : Type u) {β : Type v} [add_group α] [ β] (b : β) [fintype α] [fintype b)] [fintype ] :

Orbit-stabilizer theorem.

theorem mul_action.card_orbit_mul_card_stabilizer_eq_card_group (α : Type u) {β : Type v} [group α] [ β] (b : β) [fintype α] [fintype b)] [fintype ] :

Orbit-stabilizer theorem.

@[simp]
theorem add_action.orbit_equiv_quotient_stabilizer_symm_apply (α : Type u) {β : Type v} [add_group α] [ β] (b : β) (a : α) :
a) = a +ᵥ b
@[simp]
theorem mul_action.orbit_equiv_quotient_stabilizer_symm_apply (α : Type u) {β : Type v} [group α] [ β] (b : β) (a : α) :
a) = a b
@[simp]
@[simp]
theorem mul_action.stabilizer_quotient {G : Type u_1} [group G] (H : subgroup G) :
noncomputable def mul_action.self_equiv_sigma_orbits_quotient_stabilizer' (α : Type u) (β : Type v) [group α] [ β] {φ : β}  :
β Σ (ω : quotient β)), α (φ ω)

Class formula : given G a group acting on X and φ a function mapping each orbit of X under this action (that is, each element of the quotient of X by the relation orbit_rel G X) to an element in this orbit, this gives a (noncomputable) bijection between X and the disjoint union of G/Stab(φ(ω)) over all orbits ω. In most cases you'll want φ to be quotient.out', so we provide mul_action.self_equiv_sigma_orbits_quotient_stabilizer as a special case.

Equations
noncomputable def add_action.self_equiv_sigma_orbits_quotient_stabilizer' (α : Type u) (β : Type v) [add_group α] [ β] {φ : β}  :
β Σ (ω : quotient β)), α (φ ω)

Class formula : given G an additive group acting on X and φ a function mapping each orbit of X under this action (that is, each element of the quotient of X by the relation orbit_rel G X) to an element in this orbit, this gives a (noncomputable) bijection between X and the disjoint union of G/Stab(φ(ω)) over all orbits ω. In most cases you'll want φ to be quotient.out', so we provide add_action.self_equiv_sigma_orbits_quotient_stabilizer as a special case.

Equations
theorem add_action.card_eq_sum_card_add_group_sub_card_stabilizer' (α : Type u) (β : Type v) [add_group α] [ β] [fintype α] [fintype β] [fintype (quotient β))] [Π (b : β), ] {φ : β}  :
= finset.univ.sum (λ (ω : quotient β)), / fintype.card (φ ω)))

Class formula for a finite group acting on a finite type. See add_action.card_eq_sum_card_add_group_div_card_stabilizer for a specialized version using quotient.out'.

theorem mul_action.card_eq_sum_card_group_div_card_stabilizer' (α : Type u) (β : Type v) [group α] [ β] [fintype α] [fintype β] [fintype (quotient β))] [Π (b : β), ] {φ : β}  :
= finset.univ.sum (λ (ω : quotient β)), / fintype.card (φ ω)))

Class formula for a finite group acting on a finite type. See mul_action.card_eq_sum_card_group_div_card_stabilizer for a specialized version using quotient.out'.

noncomputable def add_action.self_equiv_sigma_orbits_quotient_stabilizer (α : Type u) (β : Type v) [add_group α] [ β] :
β Σ (ω : quotient β)),

Class formula. This is a special case of add_action.self_equiv_sigma_orbits_quotient_stabilizer' with φ = quotient.out'.

Equations
noncomputable def mul_action.self_equiv_sigma_orbits_quotient_stabilizer (α : Type u) (β : Type v) [group α] [ β] :
β Σ (ω : quotient β)),

Class formula. This is a special case of mul_action.self_equiv_sigma_orbits_quotient_stabilizer' with φ = quotient.out'.

Equations
theorem mul_action.card_eq_sum_card_group_div_card_stabilizer (α : Type u) (β : Type v) [group α] [ β] [fintype α] [fintype β] [fintype (quotient β))] [Π (b : β), ] :
= finset.univ.sum (λ (ω : quotient β)),

Class formula for a finite group acting on a finite type.

theorem add_action.card_eq_sum_card_add_group_sub_card_stabilizer (α : Type u) (β : Type v) [add_group α] [ β] [fintype α] [fintype β] [fintype (quotient β))] [Π (b : β), ] :
= finset.univ.sum (λ (ω : quotient β)),

Class formula for a finite group acting on a finite type.

(Σ (a : α), a)) × α

Burnside's lemma : a (noncomputable) bijection between the disjoint union of all {x ∈ X | g • x = x} for g ∈ G and the product G × X/G, where G is an additive group acting on X and X/Gdenotes the quotient of X by the relation orbit_rel G X.

Equations
noncomputable def mul_action.sigma_fixed_by_equiv_orbits_prod_group (α : Type u) (β : Type v) [group α] [ β] :
(Σ (a : α), a)) × α

Burnside's lemma : a (noncomputable) bijection between the disjoint union of all {x ∈ X | g • x = x} for g ∈ G and the product G × X/G, where G is a group acting on X and X/Gdenotes the quotient of X by the relation orbit_rel G X.

Equations
theorem add_action.sum_card_fixed_by_eq_card_orbits_add_card_add_group (α : Type u) (β : Type v) [add_group α] [ β] [fintype α] [Π (a : α), fintype a)] [fintype (quotient β))] :
finset.univ.sum (λ (a : α), fintype.card a)) =

Burnside's lemma : given a finite additive group G acting on a set X, the average number of elements fixed by each g ∈ G is the number of orbits.

theorem mul_action.sum_card_fixed_by_eq_card_orbits_mul_card_group (α : Type u) (β : Type v) [group α] [ β] [fintype α] [Π (a : α), fintype a)] [fintype (quotient β))] :
finset.univ.sum (λ (a : α), fintype.card a)) =

Burnside's lemma : given a finite group G acting on a set X, the average number of elements fixed by each g ∈ G is the number of orbits.

@[protected, instance]
@[protected, instance]
def mul_action.is_pretransitive_quotient (G : Type u_1) [group G] (H : subgroup G) :
(G H)
theorem subgroup.normal_core_eq_ker {G : Type u_1} [group G] (H : subgroup G) :
H.normal_core = (G H)).ker
noncomputable def subgroup.quotient_centralizer_embedding {G : Type u_1} [group G] (g : G) :

Cosets of the centralizer of an element embed into the set of commutators.

Equations
theorem subgroup.quotient_centralizer_embedding_apply {G : Type u_1} [group G] (g x : G) :
= x, g, _⟩
noncomputable def subgroup.quotient_center_embedding {G : Type u_1} [group G] {S : set G} (hS : = ) :

If G is generated by S, then the quotient by the center embeds into S-indexed sequences of commutators.

Equations
theorem subgroup.quotient_center_embedding_apply {G : Type u_1} [group G] {S : set G} (hS : = ) (g : G) (s : S) :
= g, s, _⟩