Properties of group actions involving quotient groups #
This file proves cardinality properties of group actions which use the quotient group construction, notably
- the class formula
MulAction.card_eq_sum_card_group_div_card_stabilizer'
card_comm_eq_card_conjClasses_mul_card
as well as their analogues for additive groups.
See Mathlib/GroupTheory/GroupAction/Quotient.lean
for the construction of isomorphisms used to
prove these cardinality properties.
These lemmas are separate because they require the development of cardinals.
theorem
MulAction.card_eq_sum_card_group_div_card_stabilizer'
(α : Type u_1)
(β : Type u_2)
[Group α]
[MulAction α β]
[Fintype α]
[Fintype β]
[Fintype (Quotient (orbitRel α β))]
[(b : β) → Fintype ↥(stabilizer α b)]
{φ : Quotient (orbitRel α β) → β}
(hφ : Function.LeftInverse Quotient.mk'' φ)
:
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
.
theorem
AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer'
(α : Type u_1)
(β : Type u_2)
[AddGroup α]
[AddAction α β]
[Fintype α]
[Fintype β]
[Fintype (Quotient (orbitRel α β))]
[(b : β) → Fintype ↥(stabilizer α b)]
{φ : Quotient (orbitRel α β) → β}
(hφ : Function.LeftInverse Quotient.mk'' φ)
:
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
.