Conjugation action of a group on itself #
This file defines the conjugation action of a group on itself. See also mul_aut.conj
for
the definition of conjugation as a homomorphism into the automorphism group.
Main definitions #
A type alias conj_act G
is introduced for a group G
. The group conj_act G
acts on G
by conjugation. The group conj_act G
also acts on any normal subgroup of G
by conjugation.
As a generalization, this also allows:
conj_act Mˣ
to act onM
, whenM
is amonoid
conj_act G₀
to act onG₀
, whenG₀
is agroup_with_zero
Implementation Notes #
The scalar action in defined in this file can also be written using mul_aut.conj g • h
. This
has the advantage of not using the type alias conj_act
, but the downside of this approach
is that some theorems about the group actions will not apply when since this
mul_aut.conj g • h
describes an action of mul_aut G
on G
, and not an action of G
.
A type alias for a group G
. conj_act G
acts on G
by conjugation
Instances for conj_act
- conj_act.group
- conj_act.div_inv_monoid
- conj_act.group_with_zero
- conj_act.fintype
- conj_act.inhabited
- conj_act.has_smul
- conj_act.has_units_scalar
- conj_act.units_mul_distrib_mul_action
- conj_act.units_smul_comm_class
- conj_act.units_smul_comm_class'
- conj_act.units_mul_semiring_action
- conj_act.mul_action₀
- conj_act.smul_comm_class₀
- conj_act.smul_comm_class₀'
- conj_act.distrib_mul_action₀
- conj_act.mul_distrib_mul_action
- conj_act.smul_comm_class
- conj_act.smul_comm_class'
- conj_act.subgroup.conj_action
- conj_act.subgroup.conj_mul_distrib_mul_action
- conj_act.units_has_continuous_const_smul
Equations
Equations
Equations
Equations
Equations
- conj_act.inhabited = {default := 1}
Reinterpret g : G
as an element of conj_act G
.
Equations
A recursor for conj_act
, for use as induction x using conj_act.rec
when x : conj_act G
.
Equations
- conj_act.rec h = h
Equations
- conj_act.has_smul = {smul := λ (g : conj_act G) (h : G), ⇑conj_act.of_conj_act g * h * (⇑conj_act.of_conj_act g)⁻¹}
Equations
- conj_act.units_mul_distrib_mul_action = {to_mul_action := {to_has_smul := {smul := has_smul.smul conj_act.has_units_scalar}, one_smul := _, mul_smul := _}, smul_mul := _, smul_one := _}
Equations
- conj_act.units_mul_semiring_action = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := has_smul.smul conj_act.has_units_scalar}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, smul_one := _, smul_mul := _}
Equations
- conj_act.mul_action₀ = {to_has_smul := {smul := has_smul.smul conj_act.has_smul}, one_smul := _, mul_smul := _}
Equations
- conj_act.distrib_mul_action₀ = {to_mul_action := {to_has_smul := {smul := has_smul.smul conj_act.has_smul}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
Equations
- conj_act.mul_distrib_mul_action = {to_mul_action := {to_has_smul := {smul := has_smul.smul conj_act.has_smul}, one_smul := _, mul_smul := _}, smul_mul := _, smul_one := _}
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.
Equations
- conj_act.subgroup.conj_mul_distrib_mul_action = function.injective.mul_distrib_mul_action H.subtype conj_act.subgroup.conj_mul_distrib_mul_action._proof_1 conj_act.subgroup.coe_conj_smul
Group conjugation on a normal subgroup. Analogous to mul_aut.conj
.