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 MulAction.card_orbit_mul_card_stabilizer_eq_card_group
• the class formula MulAction.selfEquivSigmaOrbitsQuotientStabilizer'
• Burnside's lemma MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group,

as well as their analogues for additive groups.

class MulAction.QuotientAction {G : Type u} (X : Type v) [Group G] [Monoid X] [MulAction X G] (H : Subgroup G) : Prop

A typeclass for when a MulAction X G descends to the quotient G ⧸ H.

• inv_mul_mem (b : X) {a a' : G} : 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 G ⧸ H.

class AddAction.QuotientAction {G : Type u} (X : Type v) [AddGroup G] [AddMonoid X] [AddAction X G] (H : AddSubgroup G) : Prop

A typeclass for when an AddAction X G descends to the quotient G ⧸ H.

• inv_mul_mem (x : X) {g g' : G} : -g + g' ∈ H → -(x +ᵥ g) + (x +ᵥ g') ∈ 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 G ⧸ H.

instance MulAction.left_quotientAction {G : Type u} [Group G] (H : Subgroup G) : QuotientAction G H

instance AddAction.left_quotientAction {G : Type u} [AddGroup G] (H : AddSubgroup G) : QuotientAction G H

instance MulAction.right_quotientAction {G : Type u} [Group G] (H : Subgroup G) : QuotientAction (↥(Subgroup.normalizer ↑H).op) H

instance AddAction.right_quotientAction {G : Type u} [AddGroup G] (H : AddSubgroup G) : QuotientAction (↥(AddSubgroup.normalizer ↑H).op) H

instance MulAction.right_quotientAction' {G : Type u} [Group G] (H : Subgroup G) [hH : H.Normal] : QuotientAction Gᵐᵒᵖ H

instance AddAction.right_quotientAction' {G : Type u} [AddGroup G] (H : AddSubgroup G) [hH : H.Normal] : QuotientAction Gᵃᵒᵖ H

@[instance_reducible]

instance MulAction.quotient {G : Type u} (X : Type v) [Group G] [Monoid X] [MulAction X G] (H : Subgroup G) [QuotientAction X H] : MulAction X (G ⧸ H)

@[instance_reducible]

instance AddAction.quotient {G : Type u} (X : Type v) [AddGroup G] [AddMonoid X] [AddAction X G] (H : AddSubgroup G) [QuotientAction X H] : AddAction X (G ⧸ H)

@[simp]

theorem MulAction.Quotient.smul_mk {G : Type u} {X : Type v} [Group G] [Monoid X] [MulAction X G] (H : Subgroup G) [QuotientAction X H] (b : X) (g : G) : b • ↑g = ↑(b • g)

@[simp]

theorem AddAction.Quotient.vadd_mk {G : Type u} {X : Type v} [AddGroup G] [AddMonoid X] [AddAction X G] (H : AddSubgroup G) [QuotientAction X H] (b : X) (g : G) : b +ᵥ ↑g = ↑(b +ᵥ g)

@[simp]

theorem MulAction.Quotient.smul_coe {G : Type u} {X : Type v} [Group G] [Monoid X] [MulAction X G] (H : Subgroup G) [QuotientAction X H] (b : X) (g : G) : b • ↑g = ↑(b • g)

@[simp]

theorem AddAction.Quotient.vadd_coe {G : Type u} {X : Type v} [AddGroup G] [AddMonoid X] [AddAction X G] (H : AddSubgroup G) [QuotientAction X H] (b : X) (g : G) : b +ᵥ ↑g = ↑(b +ᵥ g)

@[simp]

theorem MulAction.Quotient.mk_smul_out {G : Type u} {X : Type v} [Group G] [Monoid X] [MulAction X G] (H : Subgroup G) [QuotientAction X H] (b : X) (q : G ⧸ H) : ↑(b • Quotient.out q) = b • q

@[simp]

theorem AddAction.Quotient.mk_vadd_out {G : Type u} {X : Type v} [AddGroup G] [AddMonoid X] [AddAction X G] (H : AddSubgroup G) [QuotientAction X H] (b : X) (q : G ⧸ H) : ↑(b +ᵥ Quotient.out q) = b +ᵥ q

theorem MulAction.Quotient.coe_smul_out {G : Type u} {X : Type v} [Group G] [Monoid X] [MulAction X G] (H : Subgroup G) [QuotientAction X H] (b : X) (q : G ⧸ H) : ↑(b • Quotient.out q) = b • q

theorem AddAction.Quotient.coe_vadd_out {G : Type u} {X : Type v} [AddGroup G] [AddMonoid X] [AddAction X G] (H : AddSubgroup G) [QuotientAction X H] (b : X) (q : G ⧸ H) : ↑(b +ᵥ Quotient.out q) = b +ᵥ q

theorem QuotientGroup.out_conj_pow_minimalPeriod_mem {G : Type u} [Group G] (H : Subgroup G) (g : G) (q : G ⧸ H) : (Quotient.out q)⁻¹ * g ^ Function.minimalPeriod (fun (x : G ⧸ H) => g • x) q * Quotient.out q ∈ H

def MulActionHom.toQuotient {G : Type u} [Group G] (H : Subgroup G) : G →ₑ[id] G ⧸ H

The canonical map to the left cosets.

@[simp]

theorem MulActionHom.toQuotient_apply {G : Type u} [Group G] (H : Subgroup G) (g : G) : (toQuotient H) g = ↑g

@[simp]

theorem MulAction.coe_quotient_smul {G : Type u} {X : Type v} [Group G] {H : Subgroup G} [H.Normal] [SMul G X] [MulAction (G ⧸ H) X] [IsScalarTower G (G ⧸ H) X] (g : G) (x : X) : ↑g • x = g • x

@[simp]

theorem AddAction.coe_quotient_vadd {G : Type u} {X : Type v} [AddGroup G] {H : AddSubgroup G} [H.Normal] [VAdd G X] [AddAction (G ⧸ H) X] [VAddAssocClass G (G ⧸ H) X] (g : G) (x : X) : ↑g +ᵥ x = g +ᵥ x

def MulAction.ofQuotientStabilizer (G : Type u) {X : Type v} [Group G] [MulAction G X] (x : X) (g : G ⧸ stabilizer G x) : X

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

def AddAction.ofQuotientStabilizer (G : Type u) {X : Type v} [AddGroup G] [AddAction G X] (x : X) (g : G ⧸ stabilizer G x) : X

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

@[simp]

theorem MulAction.ofQuotientStabilizer_mk (G : Type u) {X : Type v} [Group G] [MulAction G X] (x : X) (g : G) : ofQuotientStabilizer G x ↑g = g • x

@[simp]

theorem AddAction.ofQuotientStabilizer_mk (G : Type u) {X : Type v} [AddGroup G] [AddAction G X] (x : X) (g : G) : ofQuotientStabilizer G x ↑g = g +ᵥ x

theorem MulAction.ofQuotientStabilizer_mem_orbit (G : Type u) {X : Type v} [Group G] [MulAction G X] (x : X) (g : G ⧸ stabilizer G x) : ofQuotientStabilizer G x g ∈ orbit G x

theorem AddAction.ofQuotientStabilizer_mem_orbit (G : Type u) {X : Type v} [AddGroup G] [AddAction G X] (x : X) (g : G ⧸ stabilizer G x) : ofQuotientStabilizer G x g ∈ orbit G x

theorem MulAction.ofQuotientStabilizer_smul (G : Type u) {X : Type v} [Group G] [MulAction G X] (x : X) (g : G) (g' : G ⧸ stabilizer G x) : ofQuotientStabilizer G x (g • g') = g • ofQuotientStabilizer G x g'

theorem AddAction.ofQuotientStabilizer_vadd (G : Type u) {X : Type v} [AddGroup G] [AddAction G X] (x : X) (g : G) (g' : G ⧸ stabilizer G x) : ofQuotientStabilizer G x (g +ᵥ g') = g +ᵥ ofQuotientStabilizer G x g'

theorem MulAction.injective_ofQuotientStabilizer (G : Type u) {X : Type v} [Group G] [MulAction G X] (x : X) : Function.Injective (ofQuotientStabilizer G x)

theorem AddAction.injective_ofQuotientStabilizer (G : Type u) {X : Type v} [AddGroup G] [AddAction G X] (x : X) : Function.Injective (ofQuotientStabilizer G x)

noncomputable def MulAction.orbitEquivQuotientStabilizer (G : Type u) {X : Type v} [Group G] [MulAction G X] (b : X) : ↑(orbit G b) ≃ G ⧸ stabilizer G b

Orbit-stabilizer theorem.

noncomputable def AddAction.orbitEquivQuotientStabilizer (G : Type u) {X : Type v} [AddGroup G] [AddAction G X] (b : X) : ↑(orbit G b) ≃ G ⧸ stabilizer G b

Orbit-stabilizer theorem.

noncomputable def MulAction.orbitProdStabilizerEquivGroup (G : Type u) {X : Type v} [Group G] [MulAction G X] (b : X) : ↑(orbit G b) × ↥(stabilizer G b) ≃ G

Orbit-stabilizer theorem.

noncomputable def AddAction.orbitProdStabilizerEquivAddGroup (G : Type u) {X : Type v} [AddGroup G] [AddAction G X] (b : X) : ↑(orbit G b) × ↥(stabilizer G b) ≃ G

Orbit-stabilizer theorem.

theorem MulAction.card_orbit_mul_card_stabilizer_eq_card_group (G : Type u) {X : Type v} [Group G] [MulAction G X] (b : X) [Fintype G] [Fintype ↑(orbit G b)] [Fintype ↥(stabilizer G b)] : Fintype.card ↑(orbit G b) * Fintype.card ↥(stabilizer G b) = Fintype.card G

Orbit-stabilizer theorem.

theorem AddAction.card_orbit_mul_card_stabilizer_eq_card_addGroup (G : Type u) {X : Type v} [AddGroup G] [AddAction G X] (b : X) [Fintype G] [Fintype ↑(orbit G b)] [Fintype ↥(stabilizer G b)] : Fintype.card ↑(orbit G b) * Fintype.card ↥(stabilizer G b) = Fintype.card G

Orbit-stabilizer theorem.

@[simp]

theorem MulAction.orbitEquivQuotientStabilizer_symm_apply (G : Type u) {X : Type v} [Group G] [MulAction G X] (b : X) (g : G) : ↑((orbitEquivQuotientStabilizer G b).symm ↑g) = g • b

@[simp]

theorem AddAction.orbitEquivQuotientStabilizer_symm_apply (G : Type u) {X : Type v} [AddGroup G] [AddAction G X] (b : X) (g : G) : ↑((orbitEquivQuotientStabilizer G b).symm ↑g) = g +ᵥ b

@[simp]

theorem MulAction.stabilizer_quotient {G : Type u_1} [Group G] (H : Subgroup G) : stabilizer G ↑1 = H

@[simp]

theorem AddAction.stabilizer_quotient {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : stabilizer G ↑0 = H

noncomputable def MulAction.selfEquivSigmaOrbitsQuotientStabilizer' (G : Type u) (X : Type v) [Group G] [MulAction G X] {φ : Quotient (orbitRel G X) → X} (hφ : Function.LeftInverse Quotient.mk'' φ) : X ≃ (ω : Quotient (orbitRel G X)) × G ⧸ stabilizer G (φ ω)

Class formula : let G be a group acting on X and let φ be a function mapping each orbit of X under this action (that is, each element of the quotient of G by the relation orbitRel G X) to an element in this orbit. We provide 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.

noncomputable def AddAction.selfEquivSigmaOrbitsQuotientStabilizer' (G : Type u) (X : Type v) [AddGroup G] [AddAction G X] {φ : Quotient (orbitRel G X) → X} (hφ : Function.LeftInverse Quotient.mk'' φ) : X ≃ (ω : Quotient (orbitRel G X)) × G ⧸ stabilizer G (φ ω)

Class formula : let G be an additive group acting on X and let φ be 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 definition is 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.

noncomputable def MulAction.selfEquivSigmaOrbitsQuotientStabilizer (G : Type u) (X : Type v) [Group G] [MulAction G X] : X ≃ (ω : Quotient (orbitRel G X)) × G ⧸ stabilizer G ω.out

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

noncomputable def AddAction.selfEquivSigmaOrbitsQuotientStabilizer (G : Type u) (X : Type v) [AddGroup G] [AddAction G X] : X ≃ (ω : Quotient (orbitRel G X)) × G ⧸ stabilizer G ω.out

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

noncomputable def MulAction.sigmaFixedByEquivOrbitsProdGroup (G : Type u) (X : Type v) [Group G] [MulAction G X] : (g : G) × ↑(fixedBy X g) ≃ Quotient (orbitRel G X) × G

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

noncomputable def AddAction.sigmaFixedByEquivOrbitsProdAddGroup (G : Type u) (X : Type v) [AddGroup G] [AddAction G X] : (g : G) × ↑(fixedBy X g) ≃ Quotient (orbitRel G X) × G

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

theorem MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group (G : Type u) (X : Type v) [Group G] [MulAction G X] [Fintype G] [(g : G) → Fintype ↑(fixedBy X g)] [Fintype (Quotient (orbitRel G X))] : ∑ g : G, Fintype.card ↑(fixedBy X g) = Fintype.card (Quotient (orbitRel G X)) * Fintype.card G

Burnside's lemma : given a finite group G acting on a type X, the sum the orders of the stabilisers coincides with the number of orbits multiplied by the order of G.

Wikidata Q1330377

theorem AddAction.sum_card_fixedBy_eq_card_orbits_mul_card_addGroup (G : Type u) (X : Type v) [AddGroup G] [AddAction G X] [Fintype G] [(g : G) → Fintype ↑(fixedBy X g)] [Fintype (Quotient (orbitRel G X))] : ∑ g : G, Fintype.card ↑(fixedBy X g) = Fintype.card (Quotient (orbitRel G X)) * Fintype.card G

Burnside's lemma : given a finite additive group G acting on a type X, the sum the orders of the stabilisers coincides with the number of orbits multiplied by the order of G.

Wikidata Q1330377

instance MulAction.isPretransitive_quotient (G : Type u_1) [Group G] (H : Subgroup G) : IsPretransitive G (G ⧸ H)

instance AddAction.isPretransitive_quotient (G : Type u_1) [AddGroup G] (H : AddSubgroup G) : IsPretransitive G (G ⧸ H)

instance MulAction.finite_quotient_of_pretransitive_of_finite_quotient {G : Type u} (X : Type v) [Group G] [MulAction G X] [IsPretransitive G X] {H : Subgroup G} [Finite (G ⧸ H)] : Finite (orbitRel.Quotient (↥H) X)

instance AddAction.finite_quotient_of_pretransitive_of_finite_quotient {G : Type u} (X : Type v) [AddGroup G] [AddAction G X] [IsPretransitive G X] {H : AddSubgroup G} [Finite (G ⧸ H)] : Finite (orbitRel.Quotient (↥H) X)

noncomputable def MulAction.equivSubgroupOrbitsSetoidComap {G : Type u} {X : Type v} [Group G] [MulAction G X] (H : Subgroup G) (ω : Quotient (orbitRel G X)) : orbitRel.Quotient ↥H ↑(orbitRel.Quotient.orbit ω) ≃ Quotient (Setoid.comap Subtype.val (orbitRel (↥H) X))

A bijection between the quotient of the action of a subgroup H on an orbit, and a corresponding quotient expressed in terms of Setoid.comap Subtype.val.

noncomputable def AddAction.equivAddSubgroupOrbitsSetoidComap {G : Type u} {X : Type v} [AddGroup G] [AddAction G X] (H : AddSubgroup G) (ω : Quotient (orbitRel G X)) : orbitRel.Quotient ↥H ↑(orbitRel.Quotient.orbit ω) ≃ Quotient (Setoid.comap Subtype.val (orbitRel (↥H) X))

A bijection between the quotient of the action of an additive subgroup H on an orbit, and a corresponding quotient expressed in terms of Setoid.comap Subtype.val.

noncomputable def MulAction.equivSubgroupOrbits {G : Type u} (X : Type v) [Group G] [MulAction G X] (H : Subgroup G) : orbitRel.Quotient (↥H) X ≃ (ω : Quotient (orbitRel G X)) × orbitRel.Quotient ↥H ↑(orbitRel.Quotient.orbit ω)

A bijection between the orbits under the action of a subgroup H on X, and the orbits under the action of H on each orbit under the action of G.

noncomputable def AddAction.equivAddSubgroupOrbits {G : Type u} (X : Type v) [AddGroup G] [AddAction G X] (H : AddSubgroup G) : orbitRel.Quotient (↥H) X ≃ (ω : Quotient (orbitRel G X)) × orbitRel.Quotient ↥H ↑(orbitRel.Quotient.orbit ω)

A bijection between the orbits under the action of an additive subgroup H on X, and the orbits under the action of H on each orbit under the action of G.

instance MulAction.finite_quotient_of_finite_quotient_of_finite_quotient {G : Type u} {X : Type v} [Group G] [MulAction G X] {H : Subgroup G} [Finite (orbitRel.Quotient G X)] [Finite (G ⧸ H)] : Finite (orbitRel.Quotient (↥H) X)

instance AddAction.finite_quotient_of_finite_quotient_of_finite_quotient {G : Type u} {X : Type v} [AddGroup G] [AddAction G X] {H : AddSubgroup G} [Finite (orbitRel.Quotient G X)] [Finite (G ⧸ H)] : Finite (orbitRel.Quotient (↥H) X)

noncomputable def MulAction.equivSubgroupOrbitsQuotientGroup {G : Type u} {X : Type v} [Group G] [MulAction G X] (x : X) [IsPretransitive G X] [IsCancelSMul G X] (H : Subgroup G) : orbitRel.Quotient (↥H) X ≃ G ⧸ H

Given a group acting freely and transitively, an equivalence between the orbits under the action of a subgroup and the quotient of the group by the subgroup.

noncomputable def AddAction.equivAddSubgroupOrbitsQuotientAddGroup {G : Type u} {X : Type v} [AddGroup G] [AddAction G X] (x : X) [IsPretransitive G X] [IsCancelVAdd G X] (H : AddSubgroup G) : orbitRel.Quotient (↥H) X ≃ G ⧸ H

Given an additive group acting freely and transitively, an equivalence between the orbits under the action of an additive subgroup and the quotient of the group by the subgroup.

noncomputable def MulAction.selfEquivOrbitsQuotientProd' {G : Type u} {X : Type v} [Group G] [MulAction G X] {φ : Quotient (orbitRel G X) → X} (hφ : Function.LeftInverse Quotient.mk'' φ) (h : ∀ (b : X), stabilizer G b = ⊥) : X ≃ Quotient (orbitRel G X) × G

If G acts on X with trivial stabilizers, X is equivalent to the product of the quotient of X by G and G. See MulAction.selfEquivOrbitsQuotientProd with φ = Quotient.out.

noncomputable def AddAction.selfEquivOrbitsQuotientProd' {G : Type u} {X : Type v} [AddGroup G] [AddAction G X] {φ : Quotient (orbitRel G X) → X} (hφ : Function.LeftInverse Quotient.mk'' φ) (h : ∀ (b : X), stabilizer G b = ⊥) : X ≃ Quotient (orbitRel G X) × G

If G acts freely on X, X is equivalent to the product of the quotient of X by G and G. See AddAction.selfEquivOrbitsQuotientProd with φ = Quotient.out.

noncomputable def MulAction.selfEquivOrbitsQuotientProd {G : Type u} {X : Type v} [Group G] [MulAction G X] (h : ∀ (b : X), stabilizer G b = ⊥) : X ≃ Quotient (orbitRel G X) × G

If G acts freely on X, X is equivalent to the product of the quotient of X by G and G.

noncomputable def AddAction.selfEquivOrbitsQuotientProd {G : Type u} {X : Type v} [AddGroup G] [AddAction G X] (h : ∀ (b : X), stabilizer G b = ⊥) : X ≃ Quotient (orbitRel G X) × G

If G acts freely on X, X is equivalent to the product of the quotient of X by G and G.

theorem ConjClasses.card_carrier {G : Type u_1} [Group G] [Fintype G] (g : G) [Fintype ↑(ConjClasses.mk g).carrier] [Fintype ↥(MulAction.stabilizer (ConjAct G) g)] : Fintype.card ↑(ConjClasses.mk g).carrier = Fintype.card G / Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)

theorem Subgroup.normalCore_eq_ker {G : Type u_1} [Group G] (H : Subgroup G) : H.normalCore = (MulAction.toPermHom G (G ⧸ H)).ker

noncomputable def Subgroup.quotientCentralizerEmbedding {G : Type u_1} [Group G] (g : G) : G ⧸ centralizer {g} ↪ ↑(commutatorSet G)

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

theorem Subgroup.quotientCentralizerEmbedding_apply {G : Type u_1} [Group G] (g x : G) : (quotientCentralizerEmbedding g) ↑x = ⟨⁅x, g⁆, ⋯⟩

noncomputable def Subgroup.quotientCenterEmbedding {G : Type u_1} [Group G] {S : Set G} (hS : closure S = ⊤) : G ⧸ center G ↪ ↑S → ↑(commutatorSet G)

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

theorem Subgroup.quotientCenterEmbedding_apply {G : Type u_1} [Group G] {S : Set G} (hS : closure S = ⊤) (g : G) (s : ↑S) : (quotientCenterEmbedding hS) (↑g) s = ⟨⁅g, ↑s⁆, ⋯⟩