# mathlibdocumentation

group_theory.group_action.conj_act

# 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 on M, when M is a monoid
• conj_act G₀ to act on G₀, when G₀ is a group_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.

def conj_act (G : Type u_3) :
Type u_3

A type alias for a group G. conj_act G acts on G by conjugation

Equations
• = G
Instances for conj_act
@[protected, instance]
def conj_act.group {G : Type u_3} [group G] :
Equations
@[protected, instance]
def conj_act.div_inv_monoid {G : Type u_3}  :
Equations
@[protected, instance]
def conj_act.group_with_zero {G : Type u_3}  :
Equations
@[protected, instance]
def conj_act.fintype {G : Type u_3} [fintype G] :
Equations
@[simp]
theorem conj_act.card {G : Type u_3} [fintype G] :
@[protected, instance]
def conj_act.inhabited {G : Type u_3}  :
Equations
def conj_act.of_conj_act {G : Type u_3}  :
≃* G

Reinterpret g : conj_act G as an element of G.

Equations
def conj_act.to_conj_act {G : Type u_3}  :
G ≃*

Reinterpret g : G as an element of conj_act G.

Equations
@[protected]
def conj_act.rec {G : Type u_3} {C : Sort u_1} (h : Π (g : G), ) (g : conj_act G) :
C g

A recursor for conj_act, for use as induction x using conj_act.rec when x : conj_act G.

Equations
@[simp]
theorem conj_act.forall {G : Type u_3} (p : → Prop) :
(∀ (x : conj_act G), p x) ∀ (x : G),
@[simp]
theorem conj_act.of_mul_symm_eq {G : Type u_3}  :
@[simp]
theorem conj_act.to_mul_symm_eq {G : Type u_3}  :
@[simp]
theorem conj_act.to_conj_act_of_conj_act {G : Type u_3} (x : conj_act G) :
@[simp]
theorem conj_act.of_conj_act_to_conj_act {G : Type u_3} (x : G) :
@[simp]
theorem conj_act.of_conj_act_one {G : Type u_3}  :
@[simp]
theorem conj_act.to_conj_act_one {G : Type u_3}  :
@[simp]
theorem conj_act.of_conj_act_inv {G : Type u_3} (x : conj_act G) :
@[simp]
theorem conj_act.to_conj_act_inv {G : Type u_3} (x : G) :
@[simp]
theorem conj_act.of_conj_act_mul {G : Type u_3} (x y : conj_act G) :
@[simp]
theorem conj_act.to_conj_act_mul {G : Type u_3} (x y : G) :
@[protected, instance]
def conj_act.has_smul {G : Type u_3}  :
Equations
theorem conj_act.smul_def {G : Type u_3} (g : conj_act G) (h : G) :
g h =
@[protected, instance]
def conj_act.has_units_scalar {M : Type u_2} [monoid M] :
M
Equations
theorem conj_act.units_smul_def {M : Type u_2} [monoid M] (g : conj_act Mˣ) (h : M) :
g h =
@[protected, instance]
def conj_act.units_mul_distrib_mul_action {M : Type u_2} [monoid M] :
Equations
@[protected, instance]
def conj_act.units_smul_comm_class (α : Type u_1) {M : Type u_2} [monoid M] [ M] [ M] [ M] :
(conj_act Mˣ) M
@[protected, instance]
def conj_act.units_smul_comm_class' (α : Type u_1) {M : Type u_2} [monoid M] [ M] [ M] [ M] :
α M
@[protected, instance]
def conj_act.units_mul_semiring_action {R : Type u_5} [semiring R] :
Equations
@[simp]
theorem conj_act.of_conj_act_zero {G₀ : Type u_4} [group_with_zero G₀] :
@[simp]
theorem conj_act.to_conj_act_zero {G₀ : Type u_4} [group_with_zero G₀] :
@[protected, instance]
def conj_act.mul_action₀ {G₀ : Type u_4} [group_with_zero G₀] :
mul_action (conj_act G₀) G₀
Equations
@[protected, instance]
def conj_act.smul_comm_class₀ (α : Type u_1) {G₀ : Type u_4} [group_with_zero G₀] [ G₀] [ G₀ G₀] [ G₀ G₀] :
(conj_act G₀) G₀
@[protected, instance]
def conj_act.smul_comm_class₀' (α : Type u_1) {G₀ : Type u_4} [group_with_zero G₀] [ G₀] [ α G₀] [ G₀ G₀] :
α G₀
@[protected, instance]
def conj_act.distrib_mul_action₀ {K : Type u_6}  :
Equations
@[protected, instance]
def conj_act.mul_distrib_mul_action {G : Type u_3} [group G] :
Equations
@[protected, instance]
def conj_act.smul_comm_class (α : Type u_1) {G : Type u_3} [group G] [ G] [ G] [ G] :
(conj_act G) G
@[protected, instance]
def conj_act.smul_comm_class' (α : Type u_1) {G : Type u_3} [group G] [ G] [ G] [ G] :
α G
theorem conj_act.smul_eq_mul_aut_conj {G : Type u_3} [group G] (g : conj_act G) (h : G) :
g h =
theorem conj_act.fixed_points_eq_center {G : Type u_3} [group G] :

The set of fixed points of the conjugation action of G on itself is the center of G.

@[protected, instance]
def conj_act.subgroup.conj_action {G : Type u_3} [group G] {H : subgroup G} [hH : H.normal] :

As normal subgroups are closed under conjugation, they inherit the conjugation action of the underlying group.

Equations
theorem conj_act.subgroup.coe_conj_smul {G : Type u_3} [group G] {H : subgroup G} [hH : H.normal] (g : conj_act G) (h : H) :
(g h) = g h
@[protected, instance]
def conj_act.subgroup.conj_mul_distrib_mul_action {G : Type u_3} [group G] {H : subgroup G} [hH : H.normal] :
Equations
def mul_aut.conj_normal {G : Type u_3} [group G] {H : subgroup G} [hH : H.normal] :
G →*

Group conjugation on a normal subgroup. Analogous to mul_aut.conj.

Equations
@[simp]
theorem mul_aut.conj_normal_apply {G : Type u_3} [group G] {H : subgroup G} [H.normal] (g : G) (h : H) :
h) = g * h * g⁻¹
@[simp]
theorem mul_aut.conj_normal_symm_apply {G : Type u_3} [group G] {H : subgroup G} [H.normal] (g : G) (h : H) :
h) = g⁻¹ * h * g
@[simp]
theorem mul_aut.conj_normal_inv_apply {G : Type u_3} [group G] {H : subgroup G} [H.normal] (g : G) (h : H) :
h) = g⁻¹ * h * g
theorem mul_aut.conj_normal_coe {G : Type u_3} [group G] {H : subgroup G} [H.normal] {h : H} :
@[protected, instance]
def conj_act.normal_of_characteristic_of_normal {G : Type u_3} [group G] {H : subgroup G} [hH : H.normal] {K : subgroup H} [h : K.characteristic] :
K).normal