group_theory.group_action.quotient

source

@[class]

structure mul_action.quotient_action {α : Type u} (β : Type v) [group α] [monoid β] [mul_action β α] (H : subgroup α) :

Prop

inv_mul_mem : ∀ (b : β) {a a' : α}, a⁻¹ * a' ∈ H → (b • a)⁻¹ * b • a' ∈ H

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

Instances of this typeclass

source

@[class]

structure add_action.quotient_action {α : Type u_1} (β : Type u_2) [add_group α] [add_monoid β] [add_action β α] (H : add_subgroup α) :

Prop

inv_mul_mem : ∀ (b : β) {a a' : α}, -a + a' ∈ H → -(b +ᵥ a) + (b +ᵥ a') ∈ H

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

Instances of this typeclass

source

@[protected, instance]

def mul_action.left_quotient_action {α : Type u} [group α] (H : subgroup α) :

mul_action.quotient_action α H

source

@[protected, instance]

def add_action.left_quotient_action {α : Type u} [add_group α] (H : add_subgroup α) :

add_action.quotient_action α H

source

@[protected, instance]

def add_action.right_quotient_action {α : Type u} [add_group α] (H : add_subgroup α) :

add_action.quotient_action ↥(⇑add_subgroup.opposite H.normalizer) H

source

@[protected, instance]

def mul_action.right_quotient_action {α : Type u} [group α] (H : subgroup α) :

mul_action.quotient_action ↥(⇑subgroup.opposite H.normalizer) H

source

@[protected, instance]

def add_action.right_quotient_action' {α : Type u} [add_group α] (H : add_subgroup α) [hH : H.normal] :

add_action.quotient_action αᵃᵒᵖ H

source

@[protected, instance]

def mul_action.right_quotient_action' {α : Type u} [group α] (H : subgroup α) [hH : H.normal] :

mul_action.quotient_action αᵐᵒᵖ H

source

@[protected, instance]

def add_action.quotient {α : Type u} (β : Type v) [add_group α] [add_monoid β] [add_action β α] (H : add_subgroup α) [add_action.quotient_action β H] :

add_action β (α ⧸ H)

Equations

add_action.quotient β H = {to_has_vadd := {vadd := λ (b : β), quotient.map' (has_vadd.vadd b) _}, zero_vadd := _, add_vadd := _}

source

@[protected, instance]

def mul_action.quotient {α : Type u} (β : Type v) [group α] [monoid β] [mul_action β α] (H : subgroup α) [mul_action.quotient_action β H] :

mul_action β (α ⧸ H)

Equations

mul_action.quotient β H = {to_has_smul := {smul := λ (b : β), quotient.map' (has_smul.smul b) _}, one_smul := _, mul_smul := _}

source

@[simp]

theorem mul_action.quotient.smul_mk {α : Type u} {β : Type v} [group α] [monoid β] [mul_action β α] (H : subgroup α) [mul_action.quotient_action β H] (b : β) (a : α) :

b • quotient_group.mk a = quotient_group.mk (b • a)

source

@[simp]

theorem add_action.quotient.vadd_mk {α : Type u} {β : Type v} [add_group α] [add_monoid β] [add_action β α] (H : add_subgroup α) [add_action.quotient_action β H] (b : β) (a : α) :

b +ᵥ quotient_add_group.mk a = quotient_add_group.mk (b +ᵥ a)

source

@[simp]

theorem mul_action.quotient.smul_coe {α : Type u} {β : Type v} [group α] [monoid β] [mul_action β α] (H : subgroup α) [mul_action.quotient_action β H] (b : β) (a : α) :

b • ↑a = ↑(b • a)

source

@[simp]

theorem add_action.quotient.vadd_coe {α : Type u} {β : Type v} [add_group α] [add_monoid β] [add_action β α] (H : add_subgroup α) [add_action.quotient_action β H] (b : β) (a : α) :

b +ᵥ ↑a = ↑(b +ᵥ a)

source

@[simp]

theorem mul_action.quotient.mk_smul_out' {α : Type u} {β : Type v} [group α] [monoid β] [mul_action β α] (H : subgroup α) [mul_action.quotient_action β H] (b : β) (q : α ⧸ H) :

quotient_group.mk (b • quotient.out' q) = b • q

source

@[simp]

theorem add_action.quotient.mk_vadd_out' {α : Type u} {β : Type v} [add_group α] [add_monoid β] [add_action β α] (H : add_subgroup α) [add_action.quotient_action β H] (b : β) (q : α ⧸ H) :

quotient_add_group.mk (b +ᵥ quotient.out' q) = b +ᵥ q

source

@[simp]

theorem mul_action.quotient.coe_smul_out' {α : Type u} {β : Type v} [group α] [monoid β] [mul_action β α] (H : subgroup α) [mul_action.quotient_action β H] (b : β) (q : α ⧸ H) :

↑(b • quotient.out' q) = b • q

source

@[simp]

theorem add_action.quotient.coe_vadd_out' {α : Type u} {β : Type v} [add_group α] [add_monoid β] [add_action β α] (H : add_subgroup α) [add_action.quotient_action β H] (b : β) (q : α ⧸ H) :

↑(b +ᵥ quotient.out' q) = b +ᵥ q

source

theorem quotient_group.out'_conj_pow_minimal_period_mem {α : Type u} [group α] (H : subgroup α) (a : α) (q : α ⧸ H) :

(quotient.out' q)⁻¹ * a ^ function.minimal_period (has_smul.smul a) q * quotient.out' q ∈ H

source

def mul_action_hom.to_quotient {α : Type u} [group α] (H : subgroup α) :

α →[α] α ⧸ H

The canonical map to the left cosets.

Equations

mul_action_hom.to_quotient H = {to_fun := coe coe_to_lift, map_smul' := _}

source

@[simp]

theorem mul_action_hom.to_quotient_apply {α : Type u} [group α] (H : subgroup α) (g : α) :

⇑(mul_action_hom.to_quotient H) g = ↑g

source

@[protected, instance]

def mul_action.mul_left_cosets_comp_subtype_val {α : Type u} [group α] (H I : subgroup α) :

mul_action ↥I (α ⧸ H)

Equations

mul_action.mul_left_cosets_comp_subtype_val H I = mul_action.comp_hom (α ⧸ H) I.subtype

source

@[protected, instance]

def add_action.add_left_cosets_comp_subtype_val {α : Type u} [add_group α] (H I : add_subgroup α) :

add_action ↥I (α ⧸ H)

Equations

add_action.add_left_cosets_comp_subtype_val H I = add_action.comp_hom (α ⧸ H) I.subtype

source

def add_action.of_quotient_stabilizer (α : Type u) {β : Type v} [add_group α] [add_action α β] (x : β) (g : α ⧸ add_action.stabilizer α x) :

β

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

Equations

add_action.of_quotient_stabilizer α x g = quotient.lift_on' g (λ (_x : α), _x +ᵥ x) _

source

def mul_action.of_quotient_stabilizer (α : Type u) {β : Type v} [group α] [mul_action α β] (x : β) (g : α ⧸ mul_action.stabilizer α x) :

β

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

Equations

mul_action.of_quotient_stabilizer α x g = quotient.lift_on' g (λ (_x : α), _x • x) _

source

@[simp]

theorem add_action.of_quotient_stabilizer_mk (α : Type u) {β : Type v} [add_group α] [add_action α β] (x : β) (g : α) :

add_action.of_quotient_stabilizer α x (quotient_add_group.mk g) = g +ᵥ x

source

@[simp]

theorem mul_action.of_quotient_stabilizer_mk (α : Type u) {β : Type v} [group α] [mul_action α β] (x : β) (g : α) :

mul_action.of_quotient_stabilizer α x (quotient_group.mk g) = g • x

source

theorem mul_action.of_quotient_stabilizer_mem_orbit (α : Type u) {β : Type v} [group α] [mul_action α β] (x : β) (g : α ⧸ mul_action.stabilizer α x) :

mul_action.of_quotient_stabilizer α x g ∈ mul_action.orbit α x

source

theorem add_action.of_quotient_stabilizer_mem_orbit (α : Type u) {β : Type v} [add_group α] [add_action α β] (x : β) (g : α ⧸ add_action.stabilizer α x) :

add_action.of_quotient_stabilizer α x g ∈ add_action.orbit α x

source

theorem add_action.of_quotient_stabilizer_vadd (α : Type u) {β : Type v} [add_group α] [add_action α β] (x : β) (g : α) (g' : α ⧸ add_action.stabilizer α x) :

add_action.of_quotient_stabilizer α x (g +ᵥ g') = g +ᵥ add_action.of_quotient_stabilizer α x g'

source

theorem mul_action.of_quotient_stabilizer_smul (α : Type u) {β : Type v} [group α] [mul_action α β] (x : β) (g : α) (g' : α ⧸ mul_action.stabilizer α x) :

mul_action.of_quotient_stabilizer α x (g • g') = g • mul_action.of_quotient_stabilizer α x g'

source

theorem mul_action.injective_of_quotient_stabilizer (α : Type u) {β : Type v} [group α] [mul_action α β] (x : β) :

function.injective (mul_action.of_quotient_stabilizer α x)

source

theorem add_action.injective_of_quotient_stabilizer (α : Type u) {β : Type v} [add_group α] [add_action α β] (x : β) :

function.injective (add_action.of_quotient_stabilizer α x)

source

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

↥(add_action.orbit α b) ≃ α ⧸ add_action.stabilizer α b

Orbit-stabilizer theorem.

Equations

add_action.orbit_equiv_quotient_stabilizer α b = (equiv.of_bijective (λ (g : α ⧸ add_action.stabilizer α b), ⟨add_action.of_quotient_stabilizer α b g, _⟩) _).symm

source

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

↥(mul_action.orbit α b) ≃ α ⧸ mul_action.stabilizer α b

Orbit-stabilizer theorem.

Equations

mul_action.orbit_equiv_quotient_stabilizer α b = (equiv.of_bijective (λ (g : α ⧸ mul_action.stabilizer α b), ⟨mul_action.of_quotient_stabilizer α b g, _⟩) _).symm

source

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

↥(add_action.orbit α b) × ↥(add_action.stabilizer α b) ≃ α

Orbit-stabilizer theorem.

Equations

add_action.orbit_sum_stabilizer_equiv_add_group α b = ((add_action.orbit_equiv_quotient_stabilizer α b).prod_congr (equiv.refl ↥(add_action.stabilizer α b))).trans add_subgroup.add_group_equiv_quotient_times_add_subgroup.symm

source

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

↥(mul_action.orbit α b) × ↥(mul_action.stabilizer α b) ≃ α

Orbit-stabilizer theorem.

Equations

mul_action.orbit_prod_stabilizer_equiv_group α b = ((mul_action.orbit_equiv_quotient_stabilizer α b).prod_congr (equiv.refl ↥(mul_action.stabilizer α b))).trans subgroup.group_equiv_quotient_times_subgroup.symm

source

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

fintype.card ↥(add_action.orbit α b) * fintype.card ↥(add_action.stabilizer α b) = fintype.card α

Orbit-stabilizer theorem.

source

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

fintype.card ↥(mul_action.orbit α b) * fintype.card ↥(mul_action.stabilizer α b) = fintype.card α

Orbit-stabilizer theorem.

source

@[simp]

theorem add_action.orbit_equiv_quotient_stabilizer_symm_apply (α : Type u) {β : Type v} [add_group α] [add_action α β] (b : β) (a : α) :

↑(⇑((add_action.orbit_equiv_quotient_stabilizer α b).symm) ↑a) = a +ᵥ b

source

@[simp]

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

↑(⇑((mul_action.orbit_equiv_quotient_stabilizer α b).symm) ↑a) = a • b

source

@[simp]

theorem add_action.stabilizer_quotient {G : Type u_1} [add_group G] (H : add_subgroup G) :

add_action.stabilizer G ↑0 = H

source

@[simp]

theorem mul_action.stabilizer_quotient {G : Type u_1} [group G] (H : subgroup G) :

mul_action.stabilizer G ↑1 = H

source

noncomputable def mul_action.self_equiv_sigma_orbits_quotient_stabilizer' (α : Type u) (β : Type v) [group α] [mul_action α β] {φ : quotient (mul_action.orbit_rel α β) → β} (hφ : function.left_inverse quotient.mk' φ) :

β ≃ Σ (ω : quotient (mul_action.orbit_rel α β)), α ⧸ mul_action.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 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

mul_action.self_equiv_sigma_orbits_quotient_stabilizer' α β hφ = (mul_action.self_equiv_sigma_orbits' α β _inst_2).trans (equiv.sigma_congr_right (λ (ω : quotient (mul_action.orbit_rel α β)), (equiv.set.of_eq _).trans (mul_action.orbit_equiv_quotient_stabilizer α (φ ω))))

source

noncomputable def add_action.self_equiv_sigma_orbits_quotient_stabilizer' (α : Type u) (β : Type v) [add_group α] [add_action α β] {φ : quotient (add_action.orbit_rel α β) → β} (hφ : function.left_inverse quotient.mk' φ) :

β ≃ Σ (ω : quotient (add_action.orbit_rel α β)), α ⧸ add_action.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 add_action.self_equiv_sigma_orbits_quotient_stabilizer as a special case.

Equations

add_action.self_equiv_sigma_orbits_quotient_stabilizer' α β hφ = (add_action.self_equiv_sigma_orbits' α β _inst_2).trans (equiv.sigma_congr_right (λ (ω : quotient (add_action.orbit_rel α β)), (equiv.set.of_eq _).trans (add_action.orbit_equiv_quotient_stabilizer α (φ ω))))

source

theorem add_action.card_eq_sum_card_add_group_sub_card_stabilizer' (α : Type u) (β : Type v) [add_group α] [add_action α β] [fintype α] [fintype β] [fintype (quotient (add_action.orbit_rel α β))] [Π (b : β), fintype ↥(add_action.stabilizer α b)] {φ : quotient (add_action.orbit_rel α β) → β} (hφ : function.left_inverse quotient.mk' φ) :

fintype.card β = finset.univ.sum (λ (ω : quotient (add_action.orbit_rel α β)), fintype.card α / fintype.card ↥(add_action.stabilizer α (φ ω)))

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'.

source

theorem mul_action.card_eq_sum_card_group_div_card_stabilizer' (α : Type u) (β : Type v) [group α] [mul_action α β] [fintype α] [fintype β] [fintype (quotient (mul_action.orbit_rel α β))] [Π (b : β), fintype ↥(mul_action.stabilizer α b)] {φ : quotient (mul_action.orbit_rel α β) → β} (hφ : function.left_inverse quotient.mk' φ) :

fintype.card β = finset.univ.sum (λ (ω : quotient (mul_action.orbit_rel α β)), fintype.card α / fintype.card ↥(mul_action.stabilizer α (φ ω)))

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'.

source

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

β ≃ Σ (ω : quotient (add_action.orbit_rel α β)), α ⧸ add_action.stabilizer α ω.out'

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

Equations

add_action.self_equiv_sigma_orbits_quotient_stabilizer α β = add_action.self_equiv_sigma_orbits_quotient_stabilizer' α β _

source

noncomputable def mul_action.self_equiv_sigma_orbits_quotient_stabilizer (α : Type u) (β : Type v) [group α] [mul_action α β] :

β ≃ Σ (ω : quotient (mul_action.orbit_rel α β)), α ⧸ mul_action.stabilizer α ω.out'

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

Equations

mul_action.self_equiv_sigma_orbits_quotient_stabilizer α β = mul_action.self_equiv_sigma_orbits_quotient_stabilizer' α β _

source

theorem mul_action.card_eq_sum_card_group_div_card_stabilizer (α : Type u) (β : Type v) [group α] [mul_action α β] [fintype α] [fintype β] [fintype (quotient (mul_action.orbit_rel α β))] [Π (b : β), fintype ↥(mul_action.stabilizer α b)] :

fintype.card β = finset.univ.sum (λ (ω : quotient (mul_action.orbit_rel α β)), fintype.card α / fintype.card ↥(mul_action.stabilizer α ω.out'))

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

source

theorem add_action.card_eq_sum_card_add_group_sub_card_stabilizer (α : Type u) (β : Type v) [add_group α] [add_action α β] [fintype α] [fintype β] [fintype (quotient (add_action.orbit_rel α β))] [Π (b : β), fintype ↥(add_action.stabilizer α b)] :

fintype.card β = finset.univ.sum (λ (ω : quotient (add_action.orbit_rel α β)), fintype.card α / fintype.card ↥(add_action.stabilizer α ω.out'))

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

source

noncomputable def add_action.sigma_fixed_by_equiv_orbits_sum_add_group (α : Type u) (β : Type v) [add_group α] [add_action α β] :

(Σ (a : α), ↥(add_action.fixed_by α β a)) ≃ quotient (add_action.orbit_rel α β) × α

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

add_action.sigma_fixed_by_equiv_orbits_sum_add_group α β = ((((((((equiv.subtype_prod_equiv_sigma_subtype (λ (a : α) (x : β), x ∈ add_action.fixed_by α β a)).symm.trans ((equiv.prod_comm α β).subtype_equiv _)).trans (equiv.subtype_prod_equiv_sigma_subtype (λ (b : β) (a : α), a ∈ add_action.stabilizer α b))).trans (add_action.self_equiv_sigma_orbits α β).sigma_congr_left').trans (equiv.sigma_assoc (λ (ω : quotient (add_action.orbit_rel α β)) (b : ↥(add_action.orbit α ω.out')), ↥(add_action.stabilizer α ↑b)))).trans (equiv.sigma_congr_right (λ (ω : quotient (add_action.orbit_rel α β)), equiv.sigma_congr_right (λ (_x : ↥(add_action.orbit α ω.out')), add_action.sigma_fixed_by_equiv_orbits_sum_add_group._match_1 α β ω _x)))).trans (equiv.sigma_congr_right (λ (ω : quotient (add_action.orbit_rel α β)), equiv.sigma_equiv_prod ↥(add_action.orbit α ω.out') ↥(add_action.stabilizer α ω.out')))).trans (equiv.sigma_congr_right (λ (ω : quotient (add_action.orbit_rel α β)), add_action.orbit_sum_stabilizer_equiv_add_group α ω.out'))).trans (equiv.sigma_equiv_prod (quotient (add_action.orbit_rel α β)) α)
add_action.sigma_fixed_by_equiv_orbits_sum_add_group._match_1 α β ω ⟨b, hb⟩ = (add_action.stabilizer_equiv_stabilizer_of_orbit_rel hb).to_equiv

source

noncomputable def mul_action.sigma_fixed_by_equiv_orbits_prod_group (α : Type u) (β : Type v) [group α] [mul_action α β] :

(Σ (a : α), ↥(mul_action.fixed_by α β a)) ≃ quotient (mul_action.orbit_rel α β) × α

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

mul_action.sigma_fixed_by_equiv_orbits_prod_group α β = ((((((((equiv.subtype_prod_equiv_sigma_subtype (λ (a : α) (x : β), x ∈ mul_action.fixed_by α β a)).symm.trans ((equiv.prod_comm α β).subtype_equiv _)).trans (equiv.subtype_prod_equiv_sigma_subtype (λ (b : β) (a : α), a ∈ mul_action.stabilizer α b))).trans (mul_action.self_equiv_sigma_orbits α β).sigma_congr_left').trans (equiv.sigma_assoc (λ (ω : quotient (mul_action.orbit_rel α β)) (b : ↥(mul_action.orbit α ω.out')), ↥(mul_action.stabilizer α ↑b)))).trans (equiv.sigma_congr_right (λ (ω : quotient (mul_action.orbit_rel α β)), equiv.sigma_congr_right (λ (_x : ↥(mul_action.orbit α ω.out')), mul_action.sigma_fixed_by_equiv_orbits_prod_group._match_1 α β ω _x)))).trans (equiv.sigma_congr_right (λ (ω : quotient (mul_action.orbit_rel α β)), equiv.sigma_equiv_prod ↥(mul_action.orbit α ω.out') ↥(mul_action.stabilizer α ω.out')))).trans (equiv.sigma_congr_right (λ (ω : quotient (mul_action.orbit_rel α β)), mul_action.orbit_prod_stabilizer_equiv_group α ω.out'))).trans (equiv.sigma_equiv_prod (quotient (mul_action.orbit_rel α β)) α)
mul_action.sigma_fixed_by_equiv_orbits_prod_group._match_1 α β ω ⟨b, hb⟩ = (mul_action.stabilizer_equiv_stabilizer_of_orbit_rel hb).to_equiv

source

theorem add_action.sum_card_fixed_by_eq_card_orbits_add_card_add_group (α : Type u) (β : Type v) [add_group α] [add_action α β] [fintype α] [Π (a : α), fintype ↥(add_action.fixed_by α β a)] [fintype (quotient (add_action.orbit_rel α β))] :

finset.univ.sum (λ (a : α), fintype.card ↥(add_action.fixed_by α β a)) = fintype.card (quotient (add_action.orbit_rel α β)) * 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.

source

theorem mul_action.sum_card_fixed_by_eq_card_orbits_mul_card_group (α : Type u) (β : Type v) [group α] [mul_action α β] [fintype α] [Π (a : α), fintype ↥(mul_action.fixed_by α β a)] [fintype (quotient (mul_action.orbit_rel α β))] :

finset.univ.sum (λ (a : α), fintype.card ↥(mul_action.fixed_by α β a)) = fintype.card (quotient (mul_action.orbit_rel α β)) * 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.

source

@[protected, instance]

def add_action.is_pretransitive_quotient (G : Type u_1) [add_group G] (H : add_subgroup G) :

add_action.is_pretransitive G (G ⧸ H)

source

@[protected, instance]

def mul_action.is_pretransitive_quotient (G : Type u_1) [group G] (H : subgroup G) :

mul_action.is_pretransitive G (G ⧸ H)

source

theorem subgroup.normal_core_eq_ker {G : Type u_1} [group G] (H : subgroup G) :

H.normal_core = (mul_action.to_perm_hom G (G ⧸ H)).ker

source

noncomputable def subgroup.quotient_centralizer_embedding {G : Type u_1} [group G] (g : G) :

G ⧸ subgroup.centralizer ↑(subgroup.zpowers g) ↪ ↥(commutator_set G)

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

Equations

subgroup.quotient_centralizer_embedding g = ((mul_action.orbit_equiv_quotient_stabilizer (conj_act G) g).trans (subgroup.quotient_equiv_of_eq _)).symm.to_embedding.trans {to_fun := λ (x : ↥(mul_action.orbit (conj_act G) g)), ⟨↑x * g⁻¹, _⟩, inj' := _}
_ = _

source

theorem subgroup.quotient_centralizer_embedding_apply {G : Type u_1} [group G] (g x : G) :

⇑(subgroup.quotient_centralizer_embedding g) ↑x = ⟨⁅x, g⁆, _⟩

source

noncomputable def subgroup.quotient_center_embedding {G : Type u_1} [group G] {S : set G} (hS : subgroup.closure S = ⊤) :

G ⧸ subgroup.center G ↪ ↥S → ↥(commutator_set G)

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

Equations

subgroup.quotient_center_embedding hS = (subgroup.quotient_equiv_of_eq _).to_embedding.trans ((subgroup.quotient_infi_embedding (λ (g : ↥S), subgroup.centralizer ↑(subgroup.zpowers ↑g))).trans (function.embedding.Pi_congr_right (λ (g : ↥S), subgroup.quotient_centralizer_embedding ↑g)))

source

theorem subgroup.quotient_center_embedding_apply {G : Type u_1} [group G] {S : set G} (hS : subgroup.closure S = ⊤) (g : G) (s : ↥S) :

⇑(subgroup.quotient_center_embedding hS) ↑g s = ⟨⁅g, ↑s⁆, _⟩

mathlib3 documentation

Properties of group actions involving quotient groups #