mathlib documentation

group_theory.group_action.quotient

Properties of group actions involving quotient groups #

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

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

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

Instances of this typeclass
@[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
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[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
@[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
@[simp]
theorem mul_action.quotient.smul_mk {α : Type u} {β : Type v} [group α] [monoid β] [mul_action β α] (H : subgroup α) [mul_action.quotient_action β H] (b : β) (a : α) :
@[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 : α) :
@[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)
@[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)
@[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) :
@[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) :
@[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) :
@[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) :
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 α) :
Equations
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
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
@[simp]
theorem add_action.of_quotient_stabilizer_mk (α : Type u) {β : Type v} [add_group α] [add_action α β] (x : β) (g : α) :
@[simp]
theorem mul_action.of_quotient_stabilizer_mk (α : Type u) {β : Type v} [group α] [mul_action α β] (x : β) (g : α) :
theorem mul_action.of_quotient_stabilizer_mem_orbit (α : Type u) {β : Type v} [group α] [mul_action α β] (x : β) (g : α mul_action.stabilizer α x) :
theorem add_action.of_quotient_stabilizer_mem_orbit (α : Type u) {β : Type v} [add_group α] [add_action α β] (x : β) (g : α add_action.stabilizer α x) :
theorem add_action.of_quotient_stabilizer_vadd (α : Type u) {β : Type v} [add_group α] [add_action α β] (x : β) (g : α) (g' : α add_action.stabilizer α x) :
theorem mul_action.of_quotient_stabilizer_smul (α : Type u) {β : Type v} [group α] [mul_action α β] (x : β) (g : α) (g' : α mul_action.stabilizer α x) :
noncomputable def add_action.orbit_equiv_quotient_stabilizer (α : Type u) {β : Type v} [add_group α] [add_action α β] (b : β) :

Orbit-stabilizer theorem.

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

Orbit-stabilizer theorem.

Equations
@[simp]
theorem add_action.orbit_equiv_quotient_stabilizer_symm_apply (α : Type u) {β : Type v} [add_group α] [add_action α β] (b : β) (a : α) :
@[simp]
theorem mul_action.orbit_equiv_quotient_stabilizer_symm_apply (α : Type u) {β : Type v} [group α] [mul_action α β] (b : β) (a : α) :
@[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 α] [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
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

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

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 α] [add_action α β] :

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 α] [mul_action α β] :

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

Equations

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

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

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

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.

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]
theorem subgroup.normal_core_eq_ker {G : Type u_1} [group G] (H : subgroup G) :