# Documentation

Mathlib.GroupTheory.GroupAction.Quotient

# Properties of group actions involving quotient groups #

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_fixedBy_eq_card_orbits_mul_card_group
class MulAction.QuotientAction {α : Type u} (β : Type v) [] [] [] (H : ) :
• inv_mul_mem : ∀ (b : β) {a a' : α}, a⁻¹ * a' H(b a)⁻¹ * b a' H

The action fulfils a normality condition on products that lie in H. This ensures that the action descends to an action on the quotient α ⧸ H.

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

Instances
class AddAction.QuotientAction {α : Type u_1} (β : Type u_2) [] [] [] (H : ) :
• inv_mul_mem : ∀ (b : β) {a a' : α}, -a + a' H-(b +ᵥ a) + (b +ᵥ a') H

The action fulfils a normality condition on summands that lie in H. This ensures that the action descends to an action on the quotient α ⧸ H.

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

Instances
instance AddAction.left_quotientAction {α : Type u} [] (H : ) :
theorem AddAction.left_quotientAction.proof_1 {α : Type u_1} [] (H : ) :
instance MulAction.left_quotientAction {α : Type u} [] (H : ) :
theorem AddAction.right_quotientAction.proof_1 {α : Type u_1} [] (H : ) :
instance AddAction.right_quotientAction {α : Type u} [] (H : ) :
instance MulAction.right_quotientAction {α : Type u} [] (H : ) :
MulAction.QuotientAction { x // x Subgroup.opposite () } H
instance AddAction.right_quotientAction' {α : Type u} [] (H : ) [hH : ] :
theorem AddAction.right_quotientAction'.proof_1 {α : Type u_1} [] (H : ) [hH : ] :
instance MulAction.right_quotientAction' {α : Type u} [] (H : ) [hH : ] :
instance AddAction.quotient {α : Type u} (β : Type v) [] [] [] (H : ) [] :
theorem AddAction.quotient.proof_2 {α : Type u_1} (β : Type u_2) [] [] [] (H : ) [] (q : α H) :
0 +ᵥ q = q
theorem AddAction.quotient.proof_1 {α : Type u_1} (β : Type u_2) [] [] [] (H : ) [] (b : β) :
∀ (x x_1 : α), Setoid.r x x_1Setoid.r ((fun x x_2 => x +ᵥ x_2) b x) ((fun x x_2 => x +ᵥ x_2) b x_1)
theorem AddAction.quotient.proof_3 {α : Type u_1} (β : Type u_2) [] [] [] (H : ) [] (b : β) (b' : β) (q : α H) :
b + b' +ᵥ q = b +ᵥ (b' +ᵥ q)
instance MulAction.quotient {α : Type u} (β : Type v) [] [] [] (H : ) [] :
MulAction β (α H)
@[simp]
theorem AddAction.Quotient.vadd_mk {α : Type u} {β : Type v} [] [] [] (H : ) [] (b : β) (a : α) :
b +ᵥ a = ↑(b +ᵥ a)
@[simp]
theorem MulAction.Quotient.smul_mk {α : Type u} {β : Type v} [] [] [] (H : ) [] (b : β) (a : α) :
b a = ↑(b a)
@[simp]
theorem AddAction.Quotient.vadd_coe {α : Type u} {β : Type v} [] [] [] (H : ) [] (b : β) (a : α) :
b +ᵥ a = ↑(b +ᵥ a)
@[simp]
theorem MulAction.Quotient.smul_coe {α : Type u} {β : Type v} [] [] [] (H : ) [] (b : β) (a : α) :
b a = ↑(b a)
@[simp]
theorem AddAction.Quotient.mk_vadd_out' {α : Type u} {β : Type v} [] [] [] (H : ) [] (b : β) (q : α H) :
↑() = b +ᵥ q
@[simp]
theorem MulAction.Quotient.mk_smul_out' {α : Type u} {β : Type v} [] [] [] (H : ) [] (b : β) (q : α H) :
↑() = b q
theorem AddAction.Quotient.coe_vadd_out' {α : Type u} {β : Type v} [] [] [] (H : ) [] (b : β) (q : α H) :
↑() = b +ᵥ q
theorem MulAction.Quotient.coe_smul_out' {α : Type u} {β : Type v} [] [] [] (H : ) [] (b : β) (q : α H) :
↑() = b q
theorem QuotientGroup.out'_conj_pow_minimalPeriod_mem {α : Type u} [] (H : ) (a : α) (q : α H) :
()⁻¹ * a ^ Function.minimalPeriod ((fun x x_1 => x x_1) a) q * H
def MulActionHom.toQuotient {α : Type u} [] (H : ) :
α →[α] α H

The canonical map to the left cosets.

Instances For
@[simp]
theorem MulActionHom.toQuotient_apply {α : Type u} [] (H : ) (g : α) :
↑() g = g
instance AddAction.addLeftCosetsCompSubtypeVal {α : Type u} [] (H : ) (I : ) :
AddAction { x // x I } (α H)
instance MulAction.mulLeftCosetsCompSubtypeVal {α : Type u} [] (H : ) (I : ) :
MulAction { x // x I } (α H)
theorem AddAction.ofQuotientStabilizer.proof_1 (α : Type u_1) {β : Type u_2} [] [] (x : β) (g1 : α) (g2 : α) (H : Setoid.r g1 g2) :
g1 +ᵥ x = g2 +ᵥ x
def AddAction.ofQuotientStabilizer (α : Type u) {β : Type v} [] [] (x : β) (g : ) :
β

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

Instances For
def MulAction.ofQuotientStabilizer (α : Type u) {β : Type v} [] [] (x : β) (g : ) :
β

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

Instances For
@[simp]
theorem AddAction.ofQuotientStabilizer_mk (α : Type u) {β : Type v} [] [] (x : β) (g : α) :
= g +ᵥ x
@[simp]
theorem MulAction.ofQuotientStabilizer_mk (α : Type u) {β : Type v} [] [] (x : β) (g : α) :
= g x
theorem AddAction.ofQuotientStabilizer_mem_orbit (α : Type u) {β : Type v} [] [] (x : β) (g : ) :
theorem MulAction.ofQuotientStabilizer_mem_orbit (α : Type u) {β : Type v} [] [] (x : β) (g : ) :
theorem AddAction.ofQuotientStabilizer_vadd (α : Type u) {β : Type v} [] [] (x : β) (g : α) (g' : ) :
theorem MulAction.ofQuotientStabilizer_smul (α : Type u) {β : Type v} [] [] (x : β) (g : α) (g' : ) :
theorem AddAction.injective_ofQuotientStabilizer (α : Type u) {β : Type v} [] [] (x : β) :
theorem MulAction.injective_ofQuotientStabilizer (α : Type u) {β : Type v} [] [] (x : β) :
abbrev AddAction.orbitEquivQuotientStabilizer.match_1 (α : Type u_2) {β : Type u_1} [] [] (b : β) (motive : ↑()Prop) :
(x : ↑()) → ((b : β) → (g : α) → (hgb : (fun m => m +ᵥ b) g = b) → motive { val := b, property := (_ : y, (fun m => m +ᵥ b) y = b) }) → motive x
Instances For
theorem AddAction.orbitEquivQuotientStabilizer.proof_1 (α : Type u_1) {β : Type u_2} [] [] (b : β) :
(Function.Injective fun g => { val := , property := (_ : ) }) Function.Surjective fun g => { val := , property := (_ : ) }
noncomputable def AddAction.orbitEquivQuotientStabilizer (α : Type u) {β : Type v} [] [] (b : β) :
↑()

Orbit-stabilizer theorem.

Instances For
noncomputable def MulAction.orbitEquivQuotientStabilizer (α : Type u) {β : Type v} [] [] (b : β) :
↑()

Orbit-stabilizer theorem.

Instances For
noncomputable def AddAction.orbitSumStabilizerEquivAddGroup (α : Type u) {β : Type v} [] [] (b : β) :
↑() × { x // } α

Orbit-stabilizer theorem.

Instances For
noncomputable def MulAction.orbitProdStabilizerEquivGroup (α : Type u) {β : Type v} [] [] (b : β) :
↑() × { x // } α

Orbit-stabilizer theorem.

Instances For
theorem AddAction.card_orbit_add_card_stabilizer_eq_card_addGroup (α : Type u) {β : Type v} [] [] (b : β) [] [Fintype ↑()] [Fintype { x // }] :
Fintype.card ↑() * Fintype.card { x // } =

Orbit-stabilizer theorem.

theorem MulAction.card_orbit_mul_card_stabilizer_eq_card_group (α : Type u) {β : Type v} [] [] (b : β) [] [Fintype ↑()] [Fintype { x // }] :
Fintype.card ↑() * Fintype.card { x // } =

Orbit-stabilizer theorem.

@[simp]
theorem AddAction.orbitEquivQuotientStabilizer_symm_apply (α : Type u) {β : Type v} [] [] (b : β) (a : α) :
↑(().symm a) = a +ᵥ b
@[simp]
theorem MulAction.orbitEquivQuotientStabilizer_symm_apply (α : Type u) {β : Type v} [] [] (b : β) (a : α) :
↑(().symm a) = a b
@[simp]
theorem AddAction.stabilizer_quotient {G : Type u_1} [] (H : ) :
= H
@[simp]
theorem MulAction.stabilizer_quotient {G : Type u_1} [] (H : ) :
= H
noncomputable def AddAction.selfEquivSigmaOrbitsQuotientStabilizer' (α : Type u) (β : Type v) [] [] {φ : β} (hφ : Function.LeftInverse Quotient.mk'' φ) :
β (ω : ) × α AddAction.stabilizer α (φ ω)

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 AddAction.selfEquivSigmaOrbitsQuotientStabilizer' as a special case.

Instances For
noncomputable def MulAction.selfEquivSigmaOrbitsQuotientStabilizer' (α : Type u) (β : Type v) [] [] {φ : β} (hφ : Function.LeftInverse Quotient.mk'' φ) :
β (ω : ) × α MulAction.stabilizer α (φ ω)

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 orbitRel 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 MulAction.selfEquivSigmaOrbitsQuotientStabilizer' as a special case.

Instances For
theorem AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer' (α : Type u) (β : Type v) [] [] [] [] [Fintype ()] [(b : β) → Fintype { x // }] {φ : β} (hφ : Function.LeftInverse Quotient.mk'' φ) :
= Finset.sum Finset.univ fun ω => / Fintype.card { x // x AddAction.stabilizer α (φ ω) }

Class formula for a finite group acting on a finite type. See AddAction.card_eq_sum_card_addGroup_div_card_stabilizer for a specialized version using Quotient.out'.

theorem MulAction.card_eq_sum_card_group_div_card_stabilizer' (α : Type u) (β : Type v) [] [] [] [] [Fintype ()] [(b : β) → Fintype { x // }] {φ : β} (hφ : Function.LeftInverse Quotient.mk'' φ) :
= Finset.sum Finset.univ fun ω => / Fintype.card { x // x MulAction.stabilizer α (φ ω) }

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

theorem AddAction.selfEquivSigmaOrbitsQuotientStabilizer.proof_1 (α : Type u_2) (β : Type u_1) [] [] (q : ) :
noncomputable def AddAction.selfEquivSigmaOrbitsQuotientStabilizer (α : Type u) (β : Type v) [] [] :
β (ω : ) ×

Class formula. This is a special case of AddAction.self_equiv_sigma_orbits_quotient_stabilizer' with φ = Quotient.out'.

Instances For
noncomputable def MulAction.selfEquivSigmaOrbitsQuotientStabilizer (α : Type u) (β : Type v) [] [] :
β (ω : ) ×

Class formula. This is a special case of MulAction.self_equiv_sigma_orbits_quotient_stabilizer' with φ = Quotient.out'.

Instances For
theorem AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer (α : Type u) (β : Type v) [] [] [] [] [Fintype ()] [(b : β) → Fintype { x // }] :
= Finset.sum Finset.univ fun ω => / Fintype.card { x // }

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

theorem MulAction.card_eq_sum_card_group_div_card_stabilizer (α : Type u) (β : Type v) [] [] [] [] [Fintype ()] [(b : β) → Fintype { x // }] :
= Finset.sum Finset.univ fun ω => / Fintype.card { x // }

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

theorem AddAction.sigmaFixedByEquivOrbitsSumAddGroup.proof_1 (α : Type u_1) (β : Type u_2) [] [] :
∀ (x : α × β), x.fst +ᵥ x.snd = x.snd x.fst +ᵥ x.snd = x.snd
abbrev AddAction.sigmaFixedByEquivOrbitsSumAddGroup.match_1 (α : Type u_2) (β : Type u_1) [] [] :
(x : ) → (motive : ↑()Sort u_3) → (x_1 : ↑()) → ((val : β) → (hb : val ) → motive { val := val, property := hb }) → motive x_1
Instances For
noncomputable def AddAction.sigmaFixedByEquivOrbitsSumAddGroup (α : Type u) (β : Type v) [] [] :
(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 orbitRel G X.

Instances For
noncomputable def MulAction.sigmaFixedByEquivOrbitsProdGroup (α : Type u) (β : Type v) [] [] :
(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/G denotes the quotient of X by the relation orbitRel G X.

Instances For
theorem AddAction.sum_card_fixedBy_eq_card_orbits_add_card_addGroup (α : Type u) (β : Type v) [] [] [] [(a : α) → Fintype ↑()] [Fintype ()] :
(Finset.sum Finset.univ fun a => Fintype.card ↑()) =

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 MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group (α : Type u) (β : Type v) [] [] [] [(a : α) → Fintype ↑()] [Fintype ()] :
(Finset.sum Finset.univ fun a => Fintype.card ↑()) =

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.

theorem ConjClasses.card_carrier {G : Type u_1} [] [] (g : G) [] [Fintype { x // x }] :
= / Fintype.card { x // x }
noncomputable def Subgroup.quotientCentralizerEmbedding {G : Type u_1} [] (g : G) :
↑()

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

Instances For
theorem Subgroup.quotientCentralizerEmbedding_apply {G : Type u_1} [] (g : G) (x : G) :
= { val := x, g, property := (_ : g₁ g₂, g₁, g₂ = x, g) }
noncomputable def Subgroup.quotientCenterEmbedding {G : Type u_1} [] {S : Set G} (hS : ) :
S↑()

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

Instances For
theorem Subgroup.quotientCenterEmbedding_apply {G : Type u_1} [] {S : Set G} (hS : ) (g : G) (s : S) :
↑() (g) s = { val := g, s, property := (_ : g₁ g₂, g₁, g₂ = g, s) }
theorem card_comm_eq_card_conjClasses_mul_card (G : Type u_1) [] :
Nat.card { p // Commute p.fst p.snd } = *