English
There is a natural bijection between the disjoint union of fixed-point sets under all group elements and the product of the orbit set with the group.
Русский
Существует естественная биекция между дизъюнктным объединением фиксированных точек по всем элементам группы и произведением множества орбит на саму группу.
LaTeX
$$(Σ a : α, fixedBy β a) ≃ Ω × α$$
Lean4
/-- **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 } := ((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 Ω α
