English
For a finite group G acting on a finite set β, the size of β equals the sum over orbit representatives of the index of the stabilizers in G.
Русский
Для конечной группы G acting на конечном наборе β размер β равен сумме по представителям орбит индексов стабилизаторов в G.
LaTeX
$$$|\beta| = \sum_{\omega \in \Omega} \frac{|G|}{|\operatorname{stabilizer}(G,\beta(\omega))|}$$$
Lean4
/-- **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φ)]
