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

@[implicit_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)

Equations

• MulAction.quotient X H = { smul := fun (b : X) => Quotient.map' (fun (x : G) => b • x) ⋯, mul_smul := ⋯, one_smul := ⋯ }

@[implicit_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)

Equations

• AddAction.quotient X H = { vadd := fun (b : X) => Quotient.map' (fun (x : G) => b +ᵥ x) ⋯, add_vadd := ⋯, zero_vadd := ⋯ }

@[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.

Equations

• MulActionHom.toQuotient H = { toFun := QuotientGroup.mk, map_smul' := ⋯ }

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

@[implicit_reducible]

instance MulAction.mulLeftCosetsCompSubtypeVal {G : Type u} [Group G] (H I : Subgroup G) : MulAction (↥I) (G ⧸ H)

Equations

• MulAction.mulLeftCosetsCompSubtypeVal H I = MulAction.compHom (G ⧸ H) I.subtype

@[implicit_reducible]

instance AddAction.addLeftCosetsCompSubtypeVal {G : Type u} [AddGroup G] (H I : AddSubgroup G) : AddAction (↥I) (G ⧸ H)

Equations

• AddAction.addLeftCosetsCompSubtypeVal H I = AddAction.compHom (G ⧸ H) I.subtype

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.

Equations

• MulAction.ofQuotientStabilizer G x g = Quotient.liftOn' g (fun (x_1 : G) => x_1 • x) ⋯

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.

Equations

• AddAction.ofQuotientStabilizer G x g = Quotient.liftOn' g (fun (x_1 : G) => x_1 +ᵥ x) ⋯

@[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.

Equations

• MulAction.orbitEquivQuotientStabilizer G b = (Equiv.ofBijective (fun (g : G ⧸ MulAction.stabilizer G b) => ⟨MulAction.ofQuotientStabilizer G b g, ⋯⟩) ⋯).symm

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.

Equations

• AddAction.orbitEquivQuotientStabilizer G b = (Equiv.ofBijective (fun (g : G ⧸ AddAction.stabilizer G b) => ⟨AddAction.ofQuotientStabilizer G b g, ⋯⟩) ⋯).symm

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• MulAction.selfEquivSigmaOrbitsQuotientStabilizer G X = MulAction.selfEquivSigmaOrbitsQuotientStabilizer' G X ⋯

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.

Equations

• AddAction.selfEquivSigmaOrbitsQuotientStabilizer G X = AddAction.selfEquivSigmaOrbitsQuotientStabilizer' G X ⋯

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• MulAction.selfEquivOrbitsQuotientProd h = MulAction.selfEquivOrbitsQuotientProd' ⋯ h

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.

Equations

• AddAction.selfEquivOrbitsQuotientProd h = AddAction.selfEquivOrbitsQuotientProd' ⋯ h

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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⁆, ⋯⟩