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:
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
.
Equations
Equations
A recursor for ConjAct
, for use as induction x
when x : ConjAct G
.
Equations
Instances For
Equations
Equations
The set of fixed points of the conjugation action of G
on itself is the center of G
.
Equations
The stabilizer of Mˣ
acting on itself by conjugation at x : Mˣ
is exactly the
units of the centralizer of x : M
.