mathlib documentation

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:

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.

@[protected, instance]
def conj_act.group {G : Type u_3} [group G] :
Equations
@[protected, instance]
Equations
@[protected, instance]
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} [div_inv_monoid G] :
Equations
def conj_act.of_conj_act {G : Type u_3} [div_inv_monoid G] :

Reinterpret g : conj_act G as an element of G.

Equations
def conj_act.to_conj_act {G : Type u_3} [div_inv_monoid G] :

Reinterpret g : G as an element of conj_act G.

Equations
@[protected]
def conj_act.rec {G : Type u_3} [div_inv_monoid G] {C : conj_act GSort u_1} (h : Π (g : G), C (conj_act.to_conj_act 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} [div_inv_monoid G] (p : conj_act G → Prop) :
(∀ (x : conj_act G), p x) ∀ (x : G), p (conj_act.to_conj_act x)
@[simp]
@[simp]
@[protected, instance]
def conj_act.has_smul {G : Type u_3} [div_inv_monoid G] :
Equations
theorem conj_act.smul_def {G : Type u_3} [div_inv_monoid G] (g : conj_act G) (h : G) :
@[protected, instance]
def conj_act.has_units_scalar {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] [has_smul α M] [smul_comm_class α M M] [is_scalar_tower α M M] :
@[protected, instance]
def conj_act.units_smul_comm_class' (α : Type u_1) {M : Type u_2} [monoid M] [has_smul α M] [smul_comm_class M α M] [is_scalar_tower α M M] :
@[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₀] [has_smul α G₀] [smul_comm_class α G₀ G₀] [is_scalar_tower α G₀ G₀] :
smul_comm_class α (conj_act G₀) G₀
@[protected, instance]
def conj_act.smul_comm_class₀' (α : Type u_1) {G₀ : Type u_4} [group_with_zero G₀] [has_smul α G₀] [smul_comm_class G₀ α G₀] [is_scalar_tower α G₀ G₀] :
smul_comm_class (conj_act G₀) α G₀
@[protected, instance]
def conj_act.smul_comm_class (α : Type u_1) {G : Type u_3} [group G] [has_smul α G] [smul_comm_class α G G] [is_scalar_tower α G G] :
@[protected, instance]
def conj_act.smul_comm_class' (α : Type u_1) {G : Type u_3} [group G] [has_smul α G] [smul_comm_class G α G] [is_scalar_tower α G G] :
theorem conj_act.smul_eq_mul_aut_conj {G : Type u_3} [group G] (g : conj_act G) (h : 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]
Equations
def mul_aut.conj_normal {G : Type u_3} [group G] {H : subgroup G} [hH : H.normal] :

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) :
@[simp]
theorem mul_aut.conj_normal_symm_apply {G : Type u_3} [group G] {H : subgroup G} [H.normal] (g : G) (h : H) :
@[simp]
theorem mul_aut.conj_normal_inv_apply {G : Type u_3} [group G] {H : subgroup G} [H.normal] (g : G) (h : H) :
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] :