doc-next-gen

Mathlib.GroupTheory.GroupAction.Quotient

Module docstring

{"# 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.card_eq_sum_card_group_div_card_stabilizer' * Burnside's lemma MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group,

as well as their analogues for additive groups. "}

MulAction.QuotientAction structure
Full source 
/-- A typeclass for when a `MulAction β α` descends to the quotient `α ⧸ H`. -/
class QuotientAction : Prop where
  /-- 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`. -/
  inv_mul_mem : ∀ (b : β) {a a' : α}, a⁻¹a⁻¹ * a' ∈ H → (b • a)⁻¹(b • a)⁻¹ * b • a' ∈ H
Quotient action typeclass
Informal description
A typeclass indicating when a multiplicative action of a group $\beta$ on a set $\alpha$ can be descended to the quotient set $\alpha \mkern-7mu\mathbin{/}\mkern-8mu H$, where $H$ is a subgroup of $\alpha$.
AddAction.QuotientAction structure
{α : Type u} (β : Type v) [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α)
Full source 
/-- A typeclass for when an `AddAction β α` descends to the quotient `α ⧸ H`. -/
class _root_.AddAction.QuotientAction {α : Type u} (β : Type v) [AddGroup α] [AddMonoid β]
  [AddAction β α] (H : AddSubgroup α) : Prop where
  /-- 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`. -/
  inv_mul_mem : ∀ (b : β) {a a' : α}, -a + a' ∈ H → -(b +ᵥ a) + (b +ᵥ a') ∈ H
Additive Action on Quotient Space
Informal description
A typeclass indicating that an additive action of `β` on `α` descends to the quotient space `α ⧸ H`, where `H` is an additive subgroup of `α`. This means the action is compatible with the quotient structure.
MulAction.right_quotientAction instance
: QuotientAction (normalizer H).op H
Full source 
@[to_additive]
instance right_quotientAction : QuotientAction (normalizer H).op H :=
  ⟨fun b c _ _ => by
    rwa [smul_def, smul_def, smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, ← mul_assoc,
      mem_normalizer_iff'.mp b.prop, mul_assoc, mul_inv_cancel_left]⟩
Opposite Normalizer Action on Quotient Group
Informal description
For a group $\alpha$ and a subgroup $H$ of $\alpha$, the opposite group of the normalizer of $H$ has a well-defined action on the quotient space $\alpha \mkern-7mu\mathbin{/}\mkern-8mu H$.
MulAction.right_quotientAction' instance
[hH : H.Normal] : QuotientAction αᵐᵒᵖ H
Full source 
@[to_additive]
instance right_quotientAction' [hH : H.Normal] : QuotientAction αᵐᵒᵖ H :=
  ⟨fun _ _ _ _ => by
    rwa [smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, mul_assoc, hH.mem_comm_iff, mul_assoc,
      mul_inv_cancel_right]⟩
Opposite Group Action on Quotient by Normal Subgroup
Informal description
For a group $\alpha$ and a normal subgroup $H$ of $\alpha$, the opposite group $\alpha^\text{op}$ has a well-defined action on the quotient space $\alpha / H$.
MulAction.quotient instance
[QuotientAction β H] : MulAction β (α ⧸ H)
Full source 
@[to_additive]
instance quotient [QuotientAction β H] : MulAction β (α ⧸ H) where
  smul b :=
    Quotient.map' (b • ·) fun _ _ h =>
      leftRel_apply.mpr <| QuotientAction.inv_mul_mem b <| leftRel_apply.mp h
  one_smul q := Quotient.inductionOn' q fun a => congr_arg Quotient.mk'' (one_smul β a)
  mul_smul b b' q := Quotient.inductionOn' q fun a => congr_arg Quotient.mk'' (mul_smul b b' a)
Group Action on Quotient Set
Informal description
For a group $\beta$ acting on a set $\alpha$ and a subgroup $H$ of $\alpha$, if the action satisfies the `QuotientAction` condition, then $\beta$ also acts on the quotient set $\alpha / H$.
MulAction.Quotient.smul_mk theorem
[QuotientAction β H] (b : β) (a : α) : (b • QuotientGroup.mk a : α ⧸ H) = QuotientGroup.mk (b • a)
Full source 
@[to_additive (attr := simp)]
theorem Quotient.smul_mk [QuotientAction β H] (b : β) (a : α) :
    (b • QuotientGroup.mk a : α ⧸ H) = QuotientGroup.mk (b • a) :=
  rfl
Compatibility of Group Action with Quotient: $b \cdot [a] = [b \cdot a]$
Informal description
Let $\beta$ be a group acting on a set $\alpha$, and let $H$ be a subgroup of $\alpha$ such that the action satisfies the `QuotientAction` condition. Then for any $b \in \beta$ and $a \in \alpha$, the action of $b$ on the equivalence class $[a]$ in the quotient set $\alpha / H$ is equal to the equivalence class of the action of $b$ on $a$, i.e., $b \cdot [a] = [b \cdot a]$.
MulAction.Quotient.smul_coe theorem
[QuotientAction β H] (b : β) (a : α) : b • (a : α ⧸ H) = (↑(b • a) : α ⧸ H)
Full source 
@[to_additive (attr := simp)]
theorem Quotient.smul_coe [QuotientAction β H] (b : β) (a : α) :
    b • (a : α ⧸ H) = (↑(b • a) : α ⧸ H) :=
  rfl
Compatibility of Group Action with Quotient: $b \cdot [a] = [b \cdot a]$
Informal description
Let $\beta$ be a group acting on a set $\alpha$, and let $H$ be a subgroup of $\alpha$ such that the action satisfies the `QuotientAction` condition. Then for any $b \in \beta$ and $a \in \alpha$, the action of $b$ on the equivalence class of $a$ in the quotient set $\alpha / H$ is equal to the equivalence class of the action of $b$ on $a$, i.e., $b \cdot [a] = [b \cdot a]$, where $[a]$ denotes the equivalence class of $a$ in $\alpha / H$.
MulAction.Quotient.mk_smul_out theorem
[QuotientAction β H] (b : β) (q : α ⧸ H) : QuotientGroup.mk (b • q.out) = b • q
Full source 
@[to_additive (attr := simp)]
theorem Quotient.mk_smul_out [QuotientAction β H] (b : β) (q : α ⧸ H) :
    QuotientGroup.mk (b • q.out) = b • q := by rw [← Quotient.smul_mk, QuotientGroup.out_eq']
Compatibility of Group Action with Quotient Representatives: $[b \cdot q.\text{out}] = b \cdot q$
Informal description
Let $\beta$ be a group acting on a set $\alpha$, and let $H$ be a subgroup of $\alpha$ such that the action satisfies the `QuotientAction` condition. For any $b \in \beta$ and any equivalence class $q \in \alpha / H$, the equivalence class of the action of $b$ on a representative $q.\text{out}$ of $q$ is equal to the action of $b$ on $q$, i.e., $[b \cdot q.\text{out}] = b \cdot q$.
MulAction.Quotient.coe_smul_out theorem
[QuotientAction β H] (b : β) (q : α ⧸ H) : ↑(b • q.out) = b • q
Full source 
@[to_additive]
theorem Quotient.coe_smul_out [QuotientAction β H] (b : β) (q : α ⧸ H) : ↑(b • q.out) = b • q := by
  simp
Compatibility of Group Action with Quotient Representatives: $[b \cdot q.\text{out}] = b \cdot q$
Informal description
Let $\beta$ be a group acting on a set $\alpha$, and let $H$ be a subgroup of $\alpha$ such that the action satisfies the `QuotientAction` condition. For any $b \in \beta$ and any equivalence class $q \in \alpha / H$, the equivalence class of the action of $b$ on a representative $q.\text{out}$ of $q$ is equal to the action of $b$ on $q$, i.e., $[b \cdot q.\text{out}] = b \cdot q$.
QuotientGroup.out_conj_pow_minimalPeriod_mem theorem
(a : α) (q : α ⧸ H) : q.out⁻¹ * a ^ Function.minimalPeriod (a • ·) q * q.out ∈ H
Full source 
theorem _root_.QuotientGroup.out_conj_pow_minimalPeriod_mem (a : α) (q : α ⧸ H) :
    q.out⁻¹q.out⁻¹ * a ^ Function.minimalPeriod (a • ·) q * q.out ∈ H := by
  rw [mul_assoc, ← QuotientGroup.eq, QuotientGroup.out_eq', ← smul_eq_mul, Quotient.mk_smul_out,
    eq_comm, pow_smul_eq_iff_minimalPeriod_dvd]
Conjugate Power of Minimal Period Lies in Subgroup for Quotient Action
Informal description
Let $\alpha$ be a group and $H$ a subgroup of $\alpha$. For any element $a \in \alpha$ and any coset $q \in \alpha/H$, the conjugate of $a$ raised to the minimal period of the action of $a$ on $q$, multiplied by a representative $q.\text{out}$ of $q$, lies in $H$. That is, \[ q.\text{out}^{-1} \cdot a^{k} \cdot q.\text{out} \in H \] where $k$ is the minimal period of the action $a \cdot q$.
MulActionHom.toQuotient definition
(H : Subgroup α) : α →[α] α ⧸ H
Full source 
/-- The canonical map to the left cosets. -/
def _root_.MulActionHom.toQuotient (H : Subgroup α) : α →[α] α ⧸ H where
  toFun := (↑); map_smul' := Quotient.smul_coe H
Canonical map to left cosets
Informal description
The canonical map from a group $\alpha$ to the left coset space $\alpha / H$ of a subgroup $H$, which is equivariant with respect to the group action of $\alpha$ on itself by left multiplication and the induced action on the quotient space.
MulActionHom.toQuotient_apply theorem
(H : Subgroup α) (g : α) : MulActionHom.toQuotient H g = g
Full source 
@[simp]
theorem _root_.MulActionHom.toQuotient_apply (H : Subgroup α) (g : α) :
    MulActionHom.toQuotient H g = g :=
  rfl
Canonical quotient map evaluation: $g \mapsto gH$
Informal description
For any subgroup $H$ of a group $\alpha$ and any element $g \in \alpha$, the canonical equivariant homomorphism to the quotient space $\alpha/H$ maps $g$ to its coset $gH$, i.e., the image of $g$ under the quotient map is simply its coset in $\alpha/H$.
MulAction.ofQuotientStabilizer definition
(g : α ⧸ MulAction.stabilizer α x) : β
Full source 
/-- The canonical map from the quotient of the stabilizer to the set. -/
@[to_additive "The canonical map from the quotient of the stabilizer to the set. "]
def ofQuotientStabilizer (g : α ⧸ MulAction.stabilizer α x) : β :=
  Quotient.liftOn' g (· • x) fun g1 g2 H =>
    calc
      g1 • x = g1 • (g1⁻¹ * g2) • x := congr_arg _ (leftRel_apply.mp H).symm
      _ = g2 • x := by rw [smul_smul, mul_inv_cancel_left]
Canonical map from quotient of stabilizer to orbit
Informal description
The canonical map from the quotient group \( \alpha / \text{stabilizer}(\alpha, x) \) to the set \( \beta \), defined by lifting the group action \( g \mapsto g \cdot x \) to the quotient. Specifically, for any coset \( g \) in the quotient, the map sends \( g \) to \( g \cdot x \), where \( g \) is any representative of the coset. This is well-defined because if \( g_1 \) and \( g_2 \) are in the same coset (i.e., \( g_1^{-1} g_2 \) stabilizes \( x \)), then \( g_1 \cdot x = g_2 \cdot x \).
MulAction.ofQuotientStabilizer_mk theorem
(g : α) : ofQuotientStabilizer α x (QuotientGroup.mk g) = g • x
Full source 
@[to_additive (attr := simp)]
theorem ofQuotientStabilizer_mk (g : α) : ofQuotientStabilizer α x (QuotientGroup.mk g) = g • x :=
  rfl
Canonical Map Evaluation on Cosets: $\text{ofQuotientStabilizer}(\alpha, x)([g]) = g \cdot x$
Informal description
For any element $g$ in the group $\alpha$, the canonical map from the quotient group $\alpha / \text{stabilizer}(\alpha, x)$ to the orbit of $x$ satisfies \[ \text{ofQuotientStabilizer}(\alpha, x)([g]) = g \cdot x, \] where $[g]$ denotes the coset of $g$ in the quotient $\alpha / \text{stabilizer}(\alpha, x)$ and $g \cdot x$ is the action of $g$ on $x$.
MulAction.ofQuotientStabilizer_mem_orbit theorem
(g) : ofQuotientStabilizer α x g ∈ orbit α x
Full source 
@[to_additive]
theorem ofQuotientStabilizer_mem_orbit (g) : ofQuotientStabilizerofQuotientStabilizer α x g ∈ orbit α x :=
  Quotient.inductionOn' g fun g => ⟨g, rfl⟩
Image of Quotient Stabilizer Map Lies in Orbit
Informal description
For any element $g$ in the quotient group $\alpha / \text{stabilizer}(\alpha, x)$, the image of $g$ under the canonical map $\text{ofQuotientStabilizer}$ lies in the orbit of $x$ under the action of $\alpha$. In other words, $\text{ofQuotientStabilizer}(\alpha, x)(g) \in \text{orbit}(\alpha, x)$.
MulAction.ofQuotientStabilizer_smul theorem
(g : α) (g' : α ⧸ MulAction.stabilizer α x) : ofQuotientStabilizer α x (g • g') = g • ofQuotientStabilizer α x g'
Full source 
@[to_additive]
theorem ofQuotientStabilizer_smul (g : α) (g' : α ⧸ MulAction.stabilizer α x) :
    ofQuotientStabilizer α x (g • g') = g • ofQuotientStabilizer α x g' :=
  Quotient.inductionOn' g' fun _ => mul_smul _ _ _
Equivariance of the Quotient Stabilizer Map
Informal description
For any element $g$ in the group $\alpha$ and any coset $g'$ in the quotient group $\alpha / \text{stabilizer}(\alpha, x)$, the canonical map $\text{ofQuotientStabilizer}$ satisfies the equivariance property: \[ \text{ofQuotientStabilizer}(\alpha, x)(g \cdot g') = g \cdot \text{ofQuotientStabilizer}(\alpha, x)(g'), \] where the left dot denotes the group action on the quotient and the right dot denotes the group action on the orbit.
MulAction.injective_ofQuotientStabilizer theorem
: Function.Injective (ofQuotientStabilizer α x)
Full source 
@[to_additive]
theorem injective_ofQuotientStabilizer : Function.Injective (ofQuotientStabilizer α x) :=
  fun y₁ y₂ =>
  Quotient.inductionOn₂' y₁ y₂ fun g₁ g₂ (H : g₁ • x = g₂ • x) =>
    Quotient.sound' <| by
      rw [leftRel_apply]
      show (g₁⁻¹ * g₂) • x = x
      rw [mul_smul, ← H, inv_smul_smul]
Injectivity of the Quotient Stabilizer Map to Orbit
Informal description
The canonical map from the quotient group $\alpha / \text{stabilizer}(\alpha, x)$ to the orbit of $x$ under the action of $\alpha$ is injective. In other words, if two cosets $g_1$ and $g_2$ in $\alpha / \text{stabilizer}(\alpha, x)$ satisfy $\text{ofQuotientStabilizer}(\alpha, x)(g_1) = \text{ofQuotientStabilizer}(\alpha, x)(g_2)$, then $g_1 = g_2$.
MulAction.orbitEquivQuotientStabilizer definition
(b : β) : orbit α b ≃ α ⧸ stabilizer α b
Full source 
/-- **Orbit-stabilizer theorem**. -/
@[to_additive "Orbit-stabilizer theorem."]
noncomputable def orbitEquivQuotientStabilizer (b : β) : orbitorbit α b ≃ α ⧸ stabilizer α b :=
  Equiv.symm <|
    Equiv.ofBijective (fun g => ⟨ofQuotientStabilizer α b g, ofQuotientStabilizer_mem_orbit α b g⟩)
      ⟨fun x y hxy => injective_ofQuotientStabilizer α b (by convert congr_arg Subtype.val hxy),
        fun ⟨_, ⟨g, hgb⟩⟩ => ⟨g, Subtype.eq hgb⟩⟩
Orbit-Stabilizer Bijection
Informal description
For a group $\alpha$ acting on a type $\beta$ and an element $b \in \beta$, there is a bijection between the orbit of $b$ under the action of $\alpha$ and the quotient group $\alpha / \text{stabilizer}(\alpha, b)$. This bijection is given by the canonical map that sends each coset $g \cdot \text{stabilizer}(\alpha, b)$ to the element $g \cdot b$ in the orbit.
MulAction.orbitProdStabilizerEquivGroup definition
(b : β) : orbit α b × stabilizer α b ≃ α
Full source 
/-- Orbit-stabilizer theorem. -/
@[to_additive AddAction.orbitProdStabilizerEquivAddGroup "Orbit-stabilizer theorem."]
noncomputable def orbitProdStabilizerEquivGroup (b : β) : orbitorbit α b × stabilizer α borbit α b × stabilizer α b ≃ α :=
  (Equiv.prodCongr (orbitEquivQuotientStabilizer α _) (Equiv.refl _)).trans
    Subgroup.groupEquivQuotientProdSubgroup.symm
Bijection between orbit-stabilizer product and group
Informal description
For a group $\alpha$ acting on a type $\beta$ and an element $b \in \beta$, there is a bijection between the product of the orbit of $b$ and its stabilizer subgroup, and the group $\alpha$ itself. This bijection is constructed by combining the orbit-stabilizer bijection with the canonical equivalence between the quotient group $\alpha / \text{stabilizer}(\alpha, b)$ and the product of the quotient group with the stabilizer subgroup.
MulAction.card_orbit_mul_card_stabilizer_eq_card_group theorem
(b : β) [Fintype α] [Fintype <| orbit α b] [Fintype <| stabilizer α b] : Fintype.card (orbit α b) * Fintype.card (stabilizer α b) = Fintype.card α
Full source 
/-- Orbit-stabilizer theorem. -/
@[to_additive AddAction.card_orbit_mul_card_stabilizer_eq_card_addGroup "Orbit-stabilizer theorem."]
theorem card_orbit_mul_card_stabilizer_eq_card_group (b : β) [Fintype α] [Fintype <| orbit α b]
    [Fintype <| stabilizer α b] :
    Fintype.card (orbit α b) * Fintype.card (stabilizer α b) = Fintype.card α := by
  rw [← Fintype.card_prod, Fintype.card_congr (orbitProdStabilizerEquivGroup α b)]
Orbit-Stabilizer Theorem: $|\text{orbit}| \cdot |\text{stabilizer}| = |G|$
Informal description
Let $G$ be a finite group acting on a type $\beta$, and let $b \in \beta$. If the orbit $\text{orbit}_G(b)$ and the stabilizer subgroup $\text{stabilizer}_G(b)$ are both finite, then the product of their cardinalities equals the cardinality of $G$: \[|\text{orbit}_G(b)| \cdot |\text{stabilizer}_G(b)| = |G|.\]
MulAction.orbitEquivQuotientStabilizer_symm_apply theorem
(b : β) (a : α) : ((orbitEquivQuotientStabilizer α b).symm a : β) = a • b
Full source 
@[to_additive (attr := simp)]
theorem orbitEquivQuotientStabilizer_symm_apply (b : β) (a : α) :
    ((orbitEquivQuotientStabilizer α b).symm a : β) = a • b :=
  rfl
Inverse Orbit-Stabilizer Bijection Evaluates to Group Action
Informal description
For a group $\alpha$ acting on a type $\beta$ and an element $b \in \beta$, the inverse of the orbit-stabilizer bijection evaluated at $a \in \alpha$ is equal to the action of $a$ on $b$, i.e., $(\text{orbitEquivQuotientStabilizer}_{\alpha}(b))^{-1}(a) = a \cdot b$.
MulAction.stabilizer_quotient theorem
{G} [Group G] (H : Subgroup G) : MulAction.stabilizer G ((1 : G) : G ⧸ H) = H
Full source 
@[to_additive (attr := simp)]
theorem stabilizer_quotient {G} [Group G] (H : Subgroup G) :
    MulAction.stabilizer G ((1 : G) : G ⧸ H) = H := by
  ext
  simp [QuotientGroup.eq]
Stabilizer of Identity in Quotient Group Equals Subgroup
Informal description
For a group $G$ and a subgroup $H$ of $G$, the stabilizer subgroup of the identity element $1$ in the quotient group $G/H$ is equal to $H$ itself. That is, $\text{stabilizer}_G(1_{G/H}) = H$.
MulAction.selfEquivSigmaOrbitsQuotientStabilizer' definition
{φ : Ω → β} (hφ : LeftInverse Quotient.mk'' φ) : β ≃ Σ ω : Ω, α ⧸ stabilizer α (φ ω)
Full source 
/-- **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. -/
@[to_additive
      "**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. "]
noncomputable def selfEquivSigmaOrbitsQuotientStabilizer' {φ : Ω → β}
    (hφ : LeftInverse Quotient.mk'' φ) : β ≃ Σω : Ω, α ⧸ stabilizer α (φ ω) :=
  calc
    β ≃ Σω : Ω, orbitRel.Quotient.orbit ω := selfEquivSigmaOrbits' α β
    _ ≃ Σω : Ω, α ⧸ stabilizer α (φ ω) :=
      Equiv.sigmaCongrRight fun ω =>
        (Equiv.setCongr <| orbitRel.Quotient.orbit_eq_orbit_out _ hφ).trans <|
          orbitEquivQuotientStabilizer α (φ ω)
Bijection between a set and the disjoint union of coset spaces of stabilizers under group action
Informal description
Given a group $G$ acting on a set $X$, and a function $\varphi$ mapping each orbit $\omega$ in the quotient $X/G$ to a representative $\varphi(\omega) \in \omega$, there is a bijection between $X$ and the disjoint union of the coset spaces $G/\text{Stab}(\varphi(\omega))$ over all orbits $\omega \in X/G$. Here, $\text{Stab}(x)$ denotes the stabilizer subgroup of $x \in X$.
MulAction.card_eq_sum_card_group_div_card_stabilizer' theorem
[Fintype α] [Fintype β] [Fintype Ω] [∀ b : β, Fintype <| stabilizer α b] {φ : Ω → β} (hφ : LeftInverse Quotient.mk'' φ) : Fintype.card β = ∑ ω : Ω, Fintype.card α / Fintype.card (stabilizer α (φ ω))
Full source 
/-- **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`. -/
@[to_additive
      "**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 card_eq_sum_card_group_div_card_stabilizer' [Fintype α] [Fintype β] [Fintype Ω]
    [∀ b : β, Fintype <| stabilizer α b] {φ : Ω → β} (hφ : LeftInverse Quotient.mk'' φ) :
    Fintype.card β = ∑ ω : Ω, Fintype.card α / Fintype.card (stabilizer α (φ ω)) := by
  classical
    have : ∀ ω : Ω, Fintype.card α / Fintype.card (stabilizer α (φ ω)) =
        Fintype.card (α ⧸ stabilizer α (φ ω)) := by
      intro ω
      rw [Fintype.card_congr (@Subgroup.groupEquivQuotientProdSubgroup α _ (stabilizer α <| φ ω)),
        Fintype.card_prod, Nat.mul_div_cancel]
      exact Fintype.card_pos_iff.mpr (by infer_instance)
    simp_rw [this, ← Fintype.card_sigma,
      Fintype.card_congr (selfEquivSigmaOrbitsQuotientStabilizer' α β hφ)]
Class Formula for Group Actions with Orbit Representatives
Informal description
Let $G$ be a finite group acting on a finite set $X$. Let $\Omega$ be the set of orbits of this action, and for each orbit $\omega \in \Omega$, let $\varphi(\omega)$ be a representative of $\omega$ (i.e., $\varphi$ is a section of the quotient map). Then the cardinality of $X$ is equal to the sum over all orbits $\omega$ of the index of the stabilizer subgroup of $\varphi(\omega)$ in $G$: \[ |X| = \sum_{\omega \in \Omega} \frac{|G|}{|\text{Stab}_G(\varphi(\omega))|}. \]
MulAction.selfEquivSigmaOrbitsQuotientStabilizer definition
: β ≃ Σ ω : Ω, α ⧸ stabilizer α ω.out
Full source 
/-- **Class formula**. This is a special case of
`MulAction.self_equiv_sigma_orbits_quotient_stabilizer'` with `φ = Quotient.out`. -/
@[to_additive
      "**Class formula**. This is a special case of
      `AddAction.self_equiv_sigma_orbits_quotient_stabilizer'` with `φ = Quotient.out`. "]
noncomputable def selfEquivSigmaOrbitsQuotientStabilizer : β ≃ Σω : Ω, α ⧸ stabilizer α ω.out :=
  selfEquivSigmaOrbitsQuotientStabilizer' α β Quotient.out_eq'
Bijection between a set and the disjoint union of coset spaces of stabilizers under group action (using orbit representatives)
Informal description
Given a group $G$ acting on a set $X$, there is a bijection between $X$ and the disjoint union of the coset spaces $G/\text{Stab}(\omega.\text{out})$ over all orbits $\omega \in X/G$, where $\omega.\text{out}$ is a representative of the orbit $\omega$ and $\text{Stab}(x)$ denotes the stabilizer subgroup of $x \in X$.
MulAction.card_eq_sum_card_group_div_card_stabilizer theorem
[Fintype α] [Fintype β] [Fintype Ω] [∀ b : β, Fintype <| stabilizer α b] : Fintype.card β = ∑ ω : Ω, Fintype.card α / Fintype.card (stabilizer α ω.out)
Full source 
/-- **Class formula** for a finite group acting on a finite type. -/
@[to_additive "**Class formula** for a finite group acting on a finite type."]
theorem card_eq_sum_card_group_div_card_stabilizer [Fintype α] [Fintype β] [Fintype Ω]
    [∀ b : β, Fintype <| stabilizer α b] :
    Fintype.card β = ∑ ω : Ω, Fintype.card α / Fintype.card (stabilizer α ω.out) :=
  card_eq_sum_card_group_div_card_stabilizer' α β Quotient.out_eq'
Class Formula for Finite Group Actions
Informal description
Let $G$ be a finite group acting on a finite set $X$. Let $\Omega$ be the set of orbits of this action. Then the cardinality of $X$ is equal to the sum over all orbits $\omega \in \Omega$ of the index of the stabilizer subgroup of any representative of $\omega$ in $G$: \[ |X| = \sum_{\omega \in \Omega} \frac{|G|}{|\text{Stab}_G(\omega.\text{out})|}. \]
MulAction.sigmaFixedByEquivOrbitsProdGroup definition
: (Σ a : α, fixedBy β a) ≃ Ω × α
Full source 
/-- **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`. -/
@[to_additive AddAction.sigmaFixedByEquivOrbitsProdAddGroup
      "**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/G`denotes the quotient of `X` by the relation `orbitRel G X`. "]
noncomputable def sigmaFixedByEquivOrbitsProdGroup : (Σa : α, fixedBy β a) ≃ Ω × α :=
  calc
    (Σa : α, fixedBy β a) ≃ { ab : α × β // ab.1 • ab.2 = ab.2 } :=
      (Equiv.subtypeProdEquivSigmaSubtype _).symm
    _ ≃ { ba : β × α // ba.2 • ba.1 = ba.1 }calc
    (Σa : α, fixedBy β a) ≃ { ab : α × β // ab.1 • ab.2 = ab.2 } :=
      (Equiv.subtypeProdEquivSigmaSubtype _).symm
    _ ≃ { ba : β × α // ba.2 • ba.1 = ba.1 } := (Equiv.prodComm α β).subtypeEquiv fun _ => Iff.rfl
    _ ≃ Σb : β, stabilizer α bcalc
    (Σa : α, fixedBy β a) ≃ { ab : α × β // ab.1 • ab.2 = ab.2 } :=
      (Equiv.subtypeProdEquivSigmaSubtype _).symm
    _ ≃ { ba : β × α // ba.2 • ba.1 = ba.1 } := (Equiv.prodComm α β).subtypeEquiv fun _ => Iff.rfl
    _ ≃ Σb : β, stabilizer α b :=
      Equiv.subtypeProdEquivSigmaSubtype fun (b : β) a => a ∈ stabilizer α b
    _ ≃ Σωb : Σω : Ω, orbit α ω.out, stabilizer α (ωb.2 : β)calc
    (Σa : α, fixedBy β a) ≃ { ab : α × β // ab.1 • ab.2 = ab.2 } :=
      (Equiv.subtypeProdEquivSigmaSubtype _).symm
    _ ≃ { ba : β × α // ba.2 • ba.1 = ba.1 } := (Equiv.prodComm α β).subtypeEquiv fun _ => Iff.rfl
    _ ≃ Σb : β, stabilizer α b :=
      Equiv.subtypeProdEquivSigmaSubtype fun (b : β) a => a ∈ stabilizer α b
    _ ≃ Σωb : Σω : Ω, orbit α ω.out, stabilizer α (ωb.2 : β) :=
      (selfEquivSigmaOrbits α β).sigmaCongrLeft'
    _ ≃ Σω : Ω, Σb : orbit α ω.out, stabilizer α (b : β)calc
    (Σa : α, fixedBy β a) ≃ { ab : α × β // ab.1 • ab.2 = ab.2 } :=
      (Equiv.subtypeProdEquivSigmaSubtype _).symm
    _ ≃ { ba : β × α // ba.2 • ba.1 = ba.1 } := (Equiv.prodComm α β).subtypeEquiv fun _ => Iff.rfl
    _ ≃ Σb : β, stabilizer α b :=
      Equiv.subtypeProdEquivSigmaSubtype fun (b : β) a => a ∈ stabilizer α b
    _ ≃ Σωb : Σω : Ω, orbit α ω.out, stabilizer α (ωb.2 : β) :=
      (selfEquivSigmaOrbits α β).sigmaCongrLeft'
    _ ≃ Σω : Ω, Σb : orbit α ω.out, stabilizer α (b : β) :=
      Equiv.sigmaAssoc fun (ω : Ω) (b : orbit α ω.out) => stabilizer α (b : β)
    _ ≃ Σω : Ω, Σ _ : orbit α ω.out, stabilizer α ω.outcalc
    (Σa : α, fixedBy β a) ≃ { ab : α × β // ab.1 • ab.2 = ab.2 } :=
      (Equiv.subtypeProdEquivSigmaSubtype _).symm
    _ ≃ { ba : β × α // ba.2 • ba.1 = ba.1 } := (Equiv.prodComm α β).subtypeEquiv fun _ => Iff.rfl
    _ ≃ Σb : β, stabilizer α b :=
      Equiv.subtypeProdEquivSigmaSubtype fun (b : β) a => a ∈ stabilizer α b
    _ ≃ Σωb : Σω : Ω, orbit α ω.out, stabilizer α (ωb.2 : β) :=
      (selfEquivSigmaOrbits α β).sigmaCongrLeft'
    _ ≃ Σω : Ω, Σb : orbit α ω.out, stabilizer α (b : β) :=
      Equiv.sigmaAssoc fun (ω : Ω) (b : orbit α ω.out) => stabilizer α (b : β)
    _ ≃ Σω : Ω, Σ _ : orbit α ω.out, stabilizer α ω.out :=
      Equiv.sigmaCongrRight fun _ =>
        Equiv.sigmaCongrRight fun ⟨_, hb⟩ => (stabilizerEquivStabilizerOfOrbitRel hb).toEquiv
    _ ≃ Σω : Ω, orbit α ω.out × stabilizer α ω.outcalc
    (Σa : α, fixedBy β a) ≃ { ab : α × β // ab.1 • ab.2 = ab.2 } :=
      (Equiv.subtypeProdEquivSigmaSubtype _).symm
    _ ≃ { ba : β × α // ba.2 • ba.1 = ba.1 } := (Equiv.prodComm α β).subtypeEquiv fun _ => Iff.rfl
    _ ≃ Σb : β, stabilizer α b :=
      Equiv.subtypeProdEquivSigmaSubtype fun (b : β) a => a ∈ stabilizer α b
    _ ≃ Σωb : Σω : Ω, orbit α ω.out, stabilizer α (ωb.2 : β) :=
      (selfEquivSigmaOrbits α β).sigmaCongrLeft'
    _ ≃ Σω : Ω, Σb : orbit α ω.out, stabilizer α (b : β) :=
      Equiv.sigmaAssoc fun (ω : Ω) (b : orbit α ω.out) => stabilizer α (b : β)
    _ ≃ Σω : Ω, Σ _ : orbit α ω.out, stabilizer α ω.out :=
      Equiv.sigmaCongrRight fun _ =>
        Equiv.sigmaCongrRight fun ⟨_, hb⟩ => (stabilizerEquivStabilizerOfOrbitRel hb).toEquiv
    _ ≃ Σω : Ω, orbit α ω.out × stabilizer α ω.out :=
      Equiv.sigmaCongrRight fun _ => Equiv.sigmaEquivProd _ _
    _ ≃ Σ _ : Ω, αcalc
    (Σa : α, fixedBy β a) ≃ { ab : α × β // ab.1 • ab.2 = ab.2 } :=
      (Equiv.subtypeProdEquivSigmaSubtype _).symm
    _ ≃ { ba : β × α // ba.2 • ba.1 = ba.1 } := (Equiv.prodComm α β).subtypeEquiv fun _ => Iff.rfl
    _ ≃ Σb : β, stabilizer α b :=
      Equiv.subtypeProdEquivSigmaSubtype fun (b : β) a => a ∈ stabilizer α b
    _ ≃ Σωb : Σω : Ω, orbit α ω.out, stabilizer α (ωb.2 : β) :=
      (selfEquivSigmaOrbits α β).sigmaCongrLeft'
    _ ≃ Σω : Ω, Σb : orbit α ω.out, stabilizer α (b : β) :=
      Equiv.sigmaAssoc fun (ω : Ω) (b : orbit α ω.out) => stabilizer α (b : β)
    _ ≃ Σω : Ω, Σ _ : orbit α ω.out, stabilizer α ω.out :=
      Equiv.sigmaCongrRight fun _ =>
        Equiv.sigmaCongrRight fun ⟨_, hb⟩ => (stabilizerEquivStabilizerOfOrbitRel hb).toEquiv
    _ ≃ Σω : Ω, orbit α ω.out × stabilizer α ω.out :=
      Equiv.sigmaCongrRight fun _ => Equiv.sigmaEquivProd _ _
    _ ≃ Σ _ : Ω, α := Equiv.sigmaCongrRight fun ω => orbitProdStabilizerEquivGroup α ω.out
    _ ≃ Ω × α := Equiv.sigmaEquivProd Ω α
Bijection between fixed points and orbits-quotient-group product
Informal description
There exists a bijection between the disjoint union of all fixed points sets $\{x \in \beta \mid a \cdot x = x\}$ for each $a \in \alpha$ and the product of the quotient space $\Omega = \beta/G$ (where $G$ is the group acting on $\beta$) with the group $\alpha$ itself. This bijection is constructed through a series of equivalences involving stabilizers, orbits, and the orbit-stabilizer theorem.
MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group theorem
[Fintype α] [∀ a : α, Fintype <| fixedBy β a] [Fintype Ω] : (∑ a : α, Fintype.card (fixedBy β a)) = Fintype.card Ω * Fintype.card α
Full source 
/-- **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. -/
@[to_additive AddAction.sum_card_fixedBy_eq_card_orbits_mul_card_addGroup
      "**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 sum_card_fixedBy_eq_card_orbits_mul_card_group [Fintype α] [∀ a : α, Fintype <| fixedBy β a]
    [Fintype Ω] : (∑ a : α, Fintype.card (fixedBy β a)) = Fintype.card Ω * Fintype.card α := by
  rw [← Fintype.card_prod, ← Fintype.card_sigma,
    Fintype.card_congr (sigmaFixedByEquivOrbitsProdGroup α β)]
Burnside's Lemma: $\sum_{g \in G} |\text{Fix}(g)| = |\Omega| \cdot |G|$
Informal description
Let $G$ be a finite group acting on a finite set $X$, and let $\Omega$ be the set of orbits of this action. Then the sum over all group elements $g \in G$ of the number of fixed points of $g$ in $X$ equals the product of the number of orbits $|\Omega|$ and the order of the group $|G|$. In symbols: \[ \sum_{g \in G} |\{x \in X \mid g \cdot x = x\}| = |\Omega| \cdot |G|. \]
MulAction.isPretransitive_quotient instance
(G) [Group G] (H : Subgroup G) : IsPretransitive G (G ⧸ H)
Full source 
@[to_additive]
instance isPretransitive_quotient (G) [Group G] (H : Subgroup G) : IsPretransitive G (G ⧸ H) where
  exists_smul_eq := by
    { rintro ⟨x⟩ ⟨y⟩
      refine ⟨y * x⁻¹, QuotientGroup.eq.mpr ?_⟩
      simp only [smul_eq_mul, H.one_mem, inv_mul_cancel, inv_mul_cancel_right]}
Transitivity of Group Action on Quotient Space
Informal description
For any group $G$ and subgroup $H$ of $G$, the action of $G$ on the quotient space $G/H$ is pretransitive (i.e., there is a single orbit).
MulAction.finite_quotient_of_pretransitive_of_finite_quotient instance
[IsPretransitive α β] {H : Subgroup α} [Finite (α ⧸ H)] : Finite <| orbitRel.Quotient H β
Full source 
@[to_additive]
instance finite_quotient_of_pretransitive_of_finite_quotient [IsPretransitive α β] {H : Subgroup α}
    [Finite (α ⧸ H)] : Finite <| orbitRel.Quotient H β := by
  rcases isEmpty_or_nonempty β with he | ⟨⟨b⟩⟩
  · exact Quotient.finite _
  · have h' : Finite (Quotient (rightRel H)) :=
      Finite.of_equiv _ (quotientRightRelEquivQuotientLeftRel _).symm
    let f : Quotient (rightRel H) → orbitRel.Quotient H β :=
      fun a ↦ Quotient.liftOn' a (fun g ↦ ⟦g • b⟧) fun g₁ g₂ r ↦ by
        replace r := Setoid.symm' _ r
        rw [rightRel_eq] at r
        simp only [Quotient.eq, orbitRel_apply, mem_orbit_iff]
        exact ⟨⟨g₁ * g₂⁻¹, r⟩, by simp [mul_smul]⟩
    exact Finite.of_surjective f ((Quotient.surjective_liftOn' _).2
      (Quotient.mk''_surjective.comp (MulAction.surjective_smul _ _)))
Finiteness of Quotient under Pretransitive Group Action with Finite Quotient
Informal description
For a group $G$ acting pretransitively on a type $\beta$ and a subgroup $H$ of $G$ such that the quotient $G/H$ is finite, the quotient of $\beta$ by the orbit relation induced by $H$ is also finite.
MulAction.equivSubgroupOrbitsSetoidComap definition
(H : Subgroup α) (ω : Ω) : orbitRel.Quotient H (orbitRel.Quotient.orbit ω) ≃ Quotient ((orbitRel H β).comap (Subtype.val : Quotient.mk (orbitRel α β) ⁻¹' { ω } → β))
Full source 
/-- 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`. -/
@[to_additive "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 equivSubgroupOrbitsSetoidComap (H : Subgroup α) (ω : Ω) :
    orbitRel.QuotientorbitRel.Quotient H (orbitRel.Quotient.orbit ω) ≃
      Quotient ((orbitRel H β).comap (Subtype.val : Quotient.mk (orbitRel α β) ⁻¹' {ω} → β)) where
  toFun := fun q ↦ q.liftOn' (fun x ↦ ⟦⟨↑x, by
    simp only [Set.mem_preimage, Set.mem_singleton_iff]
    have hx := x.property
    rwa [orbitRel.Quotient.mem_orbit] at hx⟩⟧) fun a b h ↦ by
      simp only [← Quotient.eq, orbitRel.Quotient.subgroup_quotient_eq_iff] at h
      simp only [Quotient.eq] at h ⊢
      exact h
  invFun := fun q ↦ q.liftOn' (fun x ↦ ⟦⟨↑x, by
    have hx := x.property
    simp only [Set.mem_preimage, Set.mem_singleton_iff] at hx
    rwa [orbitRel.Quotient.mem_orbit, @Quotient.mk''_eq_mk]⟩⟧) fun a b h ↦ by
      rw [Setoid.comap_rel, ← Quotient.eq'', @Quotient.mk''_eq_mk] at h
      simp only [orbitRel.Quotient.subgroup_quotient_eq_iff]
      exact h
  left_inv := by
    simp only [LeftInverse]
    intro q
    induction q using Quotient.inductionOn'
    rfl
  right_inv := by
    simp only [Function.RightInverse, LeftInverse]
    intro q
    induction q using Quotient.inductionOn'
    rfl
Bijection between subgroup orbit quotient and setoid-comap quotient
Informal description
Given a group $G$ acting on a set $\beta$, a subgroup $H$ of $G$, and an element $\omega$ in the quotient space $\beta/G$ (where elements are orbits under $G$), there is a bijection between: 1. The quotient of the orbit of $\omega$ under the action of $H$, and 2. The quotient of the preimage of $\{\omega\}$ in $\beta$ under the equivalence relation induced by the $H$-action (via `Setoid.comap`). In other words, this establishes an equivalence between two ways of forming quotient spaces involving the subgroup action on an orbit.
MulAction.equivSubgroupOrbits definition
(H : Subgroup α) : orbitRel.Quotient H β ≃ Σ ω : Ω, orbitRel.Quotient H (orbitRel.Quotient.orbit ω)
Full source 
/-- A bijection between the orbits under the action of a subgroup `H` on `β`, and the orbits
under the action of `H` on each orbit under the action of `G`. -/
@[to_additive "A bijection between the orbits under the action of an additive subgroup `H` on `β`,
and the orbits under the action of `H` on each orbit under the action of `G`."]
noncomputable def equivSubgroupOrbits (H : Subgroup α) :
    orbitRel.QuotientorbitRel.Quotient H β ≃ Σω : Ω, orbitRel.Quotient H (orbitRel.Quotient.orbit ω) :=
  (Setoid.sigmaQuotientEquivOfLe (orbitRel_subgroup_le H)).symm.trans
    (Equiv.sigmaCongrRight fun ω ↦ (equivSubgroupOrbitsSetoidComap H ω).symm)
Bijection between subgroup orbit quotient and $G$-orbit-wise subgroup orbit quotients
Informal description
Given a group $G$ acting on a set $\beta$ and a subgroup $H$ of $G$, there is a bijection between: 1. The quotient of $\beta$ by the orbit relation induced by $H$, and 2. The dependent sum over all orbits $\omega$ in $\beta/G$ (the quotient by the $G$-action) of the quotient of $\omega$ by the $H$-action. In other words, this establishes an equivalence between the $H$-orbit quotient of $\beta$ and the collection of $H$-orbit quotients of each $G$-orbit in $\beta$.
MulAction.finite_quotient_of_finite_quotient_of_finite_quotient instance
{H : Subgroup α} [Finite (orbitRel.Quotient α β)] [Finite (α ⧸ H)] : Finite <| orbitRel.Quotient H β
Full source 
@[to_additive]
instance finite_quotient_of_finite_quotient_of_finite_quotient {H : Subgroup α}
    [Finite (orbitRel.Quotient α β)] [Finite (α ⧸ H)] :
    Finite <| orbitRel.Quotient H β := by
  rw [(equivSubgroupOrbits β H).finite_iff]
  infer_instance
Finiteness of Quotient under Subgroup Action with Finite Quotients
Informal description
For a group $G$ acting on a set $\beta$ and a subgroup $H$ of $G$, if both the quotient of $\beta$ by the $G$-action and the quotient group $G/H$ are finite, then the quotient of $\beta$ by the $H$-action is also finite.
MulAction.equivSubgroupOrbitsQuotientGroup definition
[IsPretransitive α β] (free : ∀ y : β, MulAction.stabilizer α y = ⊥) (H : Subgroup α) : orbitRel.Quotient H β ≃ α ⧸ H
Full source 
/-- Given a group acting freely and transitively, an equivalence between the orbits under the
action of a subgroup and the quotient group. -/
@[to_additive "Given an additive group acting freely and transitively, an equivalence between the
orbits under the action of an additive subgroup and the quotient group."]
noncomputable def equivSubgroupOrbitsQuotientGroup [IsPretransitive α β]
    (free : ∀ y : β, MulAction.stabilizer α y = ⊥) (H : Subgroup α) :
    orbitRel.QuotientorbitRel.Quotient H β ≃ α ⧸ H where
  toFun := fun q ↦ q.liftOn' (fun y ↦ (exists_smul_eq α y x).choose) (by
    intro y₁ y₂ h
    rw [orbitRel_apply] at h
    rw [Quotient.eq'', leftRel_eq]
    dsimp only
    rcases h with ⟨g, rfl⟩
    dsimp only
    suffices (exists_smul_eq α (g • y₂) x).choose = (exists_smul_eq α y₂ x).choose * g⁻¹ by
      simp [this]
    rw [← inv_mul_eq_one, ← Subgroup.mem_bot, ← free ((g : α) • y₂)]
    simp only [mem_stabilizer_iff, smul_smul, mul_assoc, InvMemClass.coe_inv, inv_mul_cancel,
               mul_one]
    rw [← smul_smul, (exists_smul_eq α y₂ x).choose_spec, inv_smul_eq_iff,
        (exists_smul_eq α ((g : α) • y₂) x).choose_spec])
  invFun := fun q ↦ q.liftOn' (fun g ↦ ⟦g⁻¹ • x⟧) (by
    intro g₁ g₂ h
    rw [leftRel_eq] at h
    simp only
    rw [← @Quotient.mk''_eq_mk, Quotient.eq'', orbitRel_apply]
    exact ⟨⟨_, h⟩, by simp [mul_smul]⟩)
  left_inv := fun y ↦ by
    induction' y using Quotient.inductionOn' with y
    simp only [Quotient.liftOn'_mk'']
    rw [← @Quotient.mk''_eq_mk, Quotient.eq'', orbitRel_apply]
    convert mem_orbit_self _
    rw [inv_smul_eq_iff, (exists_smul_eq α y x).choose_spec]
  right_inv := fun g ↦ by
    induction' g using Quotient.inductionOn' with g
    simp only [Quotient.liftOn'_mk'', Quotient.liftOn'_mk, QuotientGroup.mk]
    rw [Quotient.eq'', leftRel_eq]
    simp only
    convert one_mem H
    · rw [inv_mul_eq_one, eq_comm, ← inv_mul_eq_one, ← Subgroup.mem_bot, ← free (g⁻¹ • x),
        mem_stabilizer_iff, mul_smul, (exists_smul_eq α (g⁻¹ • x) x).choose_spec]
Equivalence between orbits under subgroup action and quotient group
Informal description
Given a group $G$ acting freely and transitively on a type $\beta$, and a subgroup $H$ of $G$, there is an equivalence between the quotient of $\beta$ by the orbits of $H$ and the quotient group $G/H$. More precisely, if the action of $G$ on $\beta$ is transitive (i.e., for any $x, y \in \beta$, there exists $g \in G$ such that $g \cdot x = y$) and free (i.e., the stabilizer of any $y \in \beta$ is trivial), then the quotient $\beta/H$ (where two elements of $\beta$ are equivalent if they lie in the same $H$-orbit) is in bijection with the quotient group $G/H$.
MulAction.selfEquivOrbitsQuotientProd' definition
{φ : Quotient (MulAction.orbitRel α β) → β} (hφ : Function.LeftInverse Quotient.mk'' φ) (h : ∀ b : β, MulAction.stabilizer α b = ⊥) : β ≃ Quotient (MulAction.orbitRel α β) × α
Full source 
/-- If `α` acts on `β` with trivial stabilizers, `β` is equivalent
to the product of the quotient of `β` by `α` and `α`.
See `MulAction.selfEquivOrbitsQuotientProd` with `φ = Quotient.out`. -/
@[to_additive selfEquivOrbitsQuotientProd' "If `α` acts freely on `β`, `β` is equivalent
to the product of the quotient of `β` by `α` and `α`.
See `AddAction.selfEquivOrbitsQuotientProd` with `φ = Quotient.out`."]
noncomputable def selfEquivOrbitsQuotientProd'
    {φ : Quotient (MulAction.orbitRel α β) → β} (hφ : Function.LeftInverse Quotient.mk'' φ)
    (h : ∀ b : β, MulAction.stabilizer α b = ⊥) :
    β ≃ Quotient (MulAction.orbitRel α β) × α :=
  (MulAction.selfEquivSigmaOrbitsQuotientStabilizer' α β hφ).trans <|
    (Equiv.sigmaCongrRight <| fun _ ↦
      (Subgroup.quotientEquivOfEq (h _)).trans (QuotientGroup.quotientEquivSelf α)).trans <|
    Equiv.sigmaEquivProd _ _
Equivalence between a set with free group action and the product of its orbit quotient with the group
Informal description
Given a group $G$ acting on a set $X$ with trivial stabilizers (i.e., for every $x \in X$, the stabilizer subgroup $\text{Stab}(x)$ is trivial), and given a section $\varphi$ of the quotient map $X \to X/G$ (i.e., $\varphi$ maps each orbit in $X/G$ to a representative in $X$), there is an equivalence between $X$ and the product of the quotient $X/G$ with $G$. More precisely, the equivalence is given by the composition of three bijections: 1. The bijection between $X$ and the disjoint union of coset spaces $G/\text{Stab}(\varphi(\omega))$ over all orbits $\omega \in X/G$ (which simplifies to a disjoint union of copies of $G$ since stabilizers are trivial). 2. The bijection obtained by replacing each coset space $G/\text{Stab}(\varphi(\omega))$ with $G$ itself (since stabilizers are trivial). 3. The bijection between the disjoint union of copies of $G$ indexed by $X/G$ and the product $X/G \times G$.
MulAction.selfEquivOrbitsQuotientProd definition
(h : ∀ b : β, MulAction.stabilizer α b = ⊥) : β ≃ Quotient (MulAction.orbitRel α β) × α
Full source 
/-- If `α` acts freely on `β`, `β` is equivalent to the product of the quotient of `β` by `α` and
`α`. -/
@[to_additive selfEquivOrbitsQuotientProd
  "If `α` acts freely on `β`, `β` is equivalent to the product of the quotient of `β` by
`α` and `α`."]
noncomputable def selfEquivOrbitsQuotientProd (h : ∀ b : β, MulAction.stabilizer α b = ⊥) :
    β ≃ Quotient (MulAction.orbitRel α β) × α :=
  MulAction.selfEquivOrbitsQuotientProd' Quotient.out_eq' h
Equivalence between a freely acted set and the product of its orbit quotient with the group
Informal description
Given a group $G$ acting freely on a set $X$ (i.e., the stabilizer subgroup $\text{Stab}(x)$ is trivial for every $x \in X$), there is an equivalence between $X$ and the product of the quotient $X/G$ (the set of orbits under the action of $G$) with $G$ itself. More precisely, the equivalence is given by the map that sends each element $x \in X$ to the pair consisting of its orbit $[x] \in X/G$ and the unique group element $g \in G$ such that $g \cdot \varphi([x]) = x$, where $\varphi$ is a section of the quotient map $X \to X/G$.
ConjClasses.card_carrier theorem
{G : Type*} [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)
Full source 
theorem ConjClasses.card_carrier {G : Type*} [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) := by
  classical
  rw [Fintype.card_congr <| ConjAct.toConjAct (G := G) |>.toEquiv]
  rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct G) g, Nat.mul_div_cancel]
  · simp_rw [ConjAct.orbit_eq_carrier_conjClasses]
  · exact Fintype.card_pos_iff.mpr inferInstance
Cardinality of Conjugacy Class Equals Index of Stabilizer
Informal description
Let $G$ be a finite group and $g \in G$. If the conjugacy class of $g$ and the stabilizer of $g$ under the conjugation action of $G$ are both finite, then the cardinality of the conjugacy class of $g$ is equal to the index of the stabilizer subgroup in $G$: \[|\text{ConjClass}(g)| = \frac{|G|}{|\text{Stab}(g)|}.\]
Subgroup.normalCore_eq_ker theorem
: H.normalCore = (MulAction.toPermHom G (G ⧸ H)).ker
Full source 
theorem normalCore_eq_ker : H.normalCore = (MulAction.toPermHom G (G ⧸ H)).ker := by
  apply le_antisymm
  · intro g hg
    apply Equiv.Perm.ext
    refine fun q ↦ QuotientGroup.induction_on q ?_
    refine fun g' => (MulAction.Quotient.smul_mk H g g').trans (QuotientGroup.eq.mpr ?_)
    rw [smul_eq_mul, mul_inv_rev, ← inv_inv g', inv_inv]
    exact H.normalCore.inv_mem hg g'⁻¹
  · refine (Subgroup.normal_le_normalCore.mpr fun g hg => ?_)
    rw [← H.inv_mem_iff, ← mul_one g⁻¹, ← QuotientGroup.eq, ← mul_one g]
    exact (MulAction.Quotient.smul_mk H g 1).symm.trans (Equiv.Perm.ext_iff.mp hg (1 : G))
Normal Core as Kernel of Quotient Permutation Homomorphism
Informal description
For a group $G$ and a subgroup $H$ of $G$, the normal core of $H$ is equal to the kernel of the group homomorphism from $G$ to the permutation group of the quotient set $G/H$ induced by the group action.
Subgroup.quotientCentralizerEmbedding definition
(g : G) : G ⧸ centralizer (zpowers (g : G)) ↪ commutatorSet G
Full source 
/-- Cosets of the centralizer of an element embed into the set of commutators. -/
noncomputable def quotientCentralizerEmbedding (g : G) :
    G ⧸ centralizer (zpowers (g : G))G ⧸ centralizer (zpowers (g : G)) ↪ commutatorSet G :=
  ((MulAction.orbitEquivQuotientStabilizer (ConjAct G) g).trans
            (quotientEquivOfEq (ConjAct.stabilizer_eq_centralizer g))).symm.toEmbedding.trans
    ⟨fun x =>
      ⟨x * g⁻¹,
        let ⟨_, x, rfl⟩ := x
        ⟨x, g, rfl⟩⟩,
      fun _ _ => Subtype.ext ∘ mul_right_cancel ∘ Subtype.ext_iff.mp⟩
Embedding of Quotient by Centralizer into Commutator Set
Informal description
For a group \( G \) and an element \( g \in G \), there is an embedding of the quotient group \( G / \text{centralizer}(\langle g \rangle) \) into the set of commutators of \( G \). Here, \( \text{centralizer}(\langle g \rangle) \) denotes the centralizer of the cyclic subgroup generated by \( g \), and the embedding is constructed via the orbit-stabilizer bijection and the identification of the stabilizer with the centralizer.
Subgroup.quotientCentralizerEmbedding_apply theorem
(g : G) (x : G) : quotientCentralizerEmbedding g x = ⟨⁅x, g⁆, x, g, rfl⟩
Full source 
theorem quotientCentralizerEmbedding_apply (g : G) (x : G) :
    quotientCentralizerEmbedding g x = ⟨⁅x, g⁆, x, g, rfl⟩ :=
  rfl
Image of Quotient by Centralizer Embedding is Commutator $[x, g]$
Informal description
For any group $G$ and element $g \in G$, the embedding of the quotient group $G / \text{centralizer}(\langle g \rangle)$ into the commutator set of $G$ maps an element $x \in G$ to the commutator $[x, g]$, where $\langle [x, g], x, g, \text{rfl}\rangle$ denotes the commutator element in the commutator set.
Subgroup.quotientCenterEmbedding definition
{S : Set G} (hS : closure S = ⊤) : G ⧸ center G ↪ S → commutatorSet G
Full source 
/-- If `G` is generated by `S`, then the quotient by the center embeds into `S`-indexed sequences
of commutators. -/
noncomputable def quotientCenterEmbedding {S : Set G} (hS : closure S = ⊤) :
    G ⧸ center GG ⧸ center G ↪ S → commutatorSet G :=
  (quotientEquivOfEq (center_eq_infi' S hS)).toEmbedding.trans
    ((quotientiInfEmbedding _).trans
      (Function.Embedding.piCongrRight fun g => quotientCentralizerEmbedding (g : G)))
Embedding of quotient by center into commutator functions
Informal description
Given a group \( G \) and a generating set \( S \) (i.e., the subgroup generated by \( S \) is the whole group \( G \)), there exists an embedding of the quotient group \( G / \text{center}(G) \) into the set of functions from \( S \) to the commutator set of \( G \). Here, \( \text{center}(G) \) denotes the center of \( G \), and the commutator set consists of all commutators \( [g, s] \) for \( g \in G \) and \( s \in S \).
Subgroup.quotientCenterEmbedding_apply theorem
{S : Set G} (hS : closure S = ⊤) (g : G) (s : S) : quotientCenterEmbedding hS g s = ⟨⁅g, s⁆, g, s, rfl⟩
Full source 
theorem quotientCenterEmbedding_apply {S : Set G} (hS : closure S = ⊤) (g : G) (s : S) :
    quotientCenterEmbedding hS g s = ⟨⁅g, s⁆, g, s, rfl⟩ :=
  rfl
Image of Quotient Center Embedding is Commutator $[g, s]$
Informal description
Given a group $G$ and a generating set $S$ (i.e., the subgroup generated by $S$ is $G$), for any element $g \in G$ and $s \in S$, the image of $g$ under the quotient center embedding is the commutator $[g, s]$, represented as $\langle [g, s], g, s, \text{rfl}\rangle$ in the commutator set of $G$.