Conjugation action of a group on itself #
This file defines the conjugation action of a group on itself. See also MulAut.conj
for
the definition of conjugation as a homomorphism into the automorphism group.
Main definitions #
A type alias ConjAct G
is introduced for a group G
. The group ConjAct G
acts on G
by conjugation. The group ConjAct G
also acts on any normal subgroup of G
by conjugation.
As a generalization, this also allows:
ConjAct Mˣ
to act onM
, whenM
is aMonoid
ConjAct G₀
to act onG₀
, whenG₀
is aGroupWithZero
Implementation Notes #
The scalar action in defined in this file can also be written using MulAut.conj g • h
. This
has the advantage of not using the type alias ConjAct
, but the downside of this approach
is that some theorems about the group actions will not apply when since this
MulAut.conj g • h
describes an action of MulAut G
on G
, and not an action of G
.
Reinterpret g : ConjAct G
as an element of G
.
Instances For
Reinterpret g : G
as an element of ConjAct G
.
Instances For
A recursor for ConjAct
, for use as induction x using ConjAct.rec
when x : ConjAct G
.
Instances For
The set of fixed points of the conjugation action of G
on itself is the center of G
.
As normal subgroups are closed under conjugation, they inherit the conjugation action of the underlying group.
Group conjugation on a normal subgroup. Analogous to MulAut.conj
.
Instances For
The stabilizer of Mˣ
acting on itself by conjugation at x : Mˣ
is exactly the
units of the centralizer of x : M
.