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
card_orbit_mul_card_stabilizer_eq_card_group
- the class formula
card_eq_sum_card_group_div_card_stabilizer'
- Burnside's lemma
sum_card_fixedBy_eq_card_orbits_mul_card_group
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
.
A typeclass for when a MulAction β α
descends to the quotient α ⧸ H
.
Instances
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
.
A typeclass for when an AddAction β α
descends to the quotient α ⧸ H
.
Instances
The canonical map from the quotient of the stabilizer to the set.
Instances For
The canonical map from the quotient of the stabilizer to the set.
Instances For
Instances For
Orbit-stabilizer theorem.
Instances For
Orbit-stabilizer theorem.
Instances For
Orbit-stabilizer theorem.
Instances For
Orbit-stabilizer theorem.
Instances For
Orbit-stabilizer theorem.
Orbit-stabilizer theorem.
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.
Instances For
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.
Instances For
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'
.
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'
.
Class formula. This is a special case of
AddAction.self_equiv_sigma_orbits_quotient_stabilizer'
with φ = Quotient.out'
.
Instances For
Class formula. This is a special case of
MulAction.self_equiv_sigma_orbits_quotient_stabilizer'
with φ = Quotient.out'
.
Instances For
Class formula for a finite group acting on a finite type.
Class formula for a finite group acting on a finite type.
Instances For
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
.
Instances For
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
.
Instances For
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.
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.
Cosets of the centralizer of an element embed into the set of commutators.
Instances For
If G
is generated by S
, then the quotient by the center embeds into S
-indexed sequences
of commutators.