mathlib3 documentation

group_theory.group_action.conj_act

Conjugation action of a group on itself #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

conj_act G = G

Instances for conj_act

@[protected, instance]

def conj_act.group {G : Type u_3} [group G] :

group (conj_act G)

Equations

conj_act.group = id

@[protected, instance]

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

div_inv_monoid (conj_act G)

Equations

conj_act.div_inv_monoid = id

@[protected, instance]

def conj_act.group_with_zero {G : Type u_3} [group_with_zero G] :

group_with_zero (conj_act G)

Equations

conj_act.group_with_zero = id

@[protected, instance]

def conj_act.fintype {G : Type u_3} [fintype G] :

fintype (conj_act G)

Equations

conj_act.fintype = id

@[simp]

theorem conj_act.card {G : Type u_3} [fintype G] :

fintype.card (conj_act G) = fintype.card G

@[protected, instance]

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

inhabited (conj_act G)

Equations

conj_act.inhabited = {default := 1}

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

conj_act G ≃* G

Reinterpret g : conj_act G as an element of G.

Equations

conj_act.of_conj_act = {to_fun := id (conj_act G), inv_fun := id G, left_inv := _, right_inv := _, map_mul' := _}

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

G ≃* conj_act G

Reinterpret g : G as an element of conj_act G.

Equations

conj_act.to_conj_act = conj_act.of_conj_act.symm

@[protected]

def conj_act.rec {G : Type u_3} [div_inv_monoid G] {C : conj_act G → Sort 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

conj_act.rec h = h

@[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]

theorem conj_act.of_mul_symm_eq {G : Type u_3} [div_inv_monoid G] :

conj_act.of_conj_act.symm = conj_act.to_conj_act

@[simp]

theorem conj_act.to_mul_symm_eq {G : Type u_3} [div_inv_monoid G] :

conj_act.to_conj_act.symm = conj_act.of_conj_act

@[simp]

theorem conj_act.to_conj_act_of_conj_act {G : Type u_3} [div_inv_monoid G] (x : conj_act G) :

⇑conj_act.to_conj_act (⇑conj_act.of_conj_act x) = x

@[simp]

theorem conj_act.of_conj_act_to_conj_act {G : Type u_3} [div_inv_monoid G] (x : G) :

⇑conj_act.of_conj_act (⇑conj_act.to_conj_act x) = x

@[simp]

theorem conj_act.of_conj_act_one {G : Type u_3} [div_inv_monoid G] :

⇑conj_act.of_conj_act 1 = 1

@[simp]

theorem conj_act.to_conj_act_one {G : Type u_3} [div_inv_monoid G] :

⇑conj_act.to_conj_act 1 = 1

@[simp]

theorem conj_act.of_conj_act_inv {G : Type u_3} [div_inv_monoid G] (x : conj_act G) :

⇑conj_act.of_conj_act x⁻¹ = (⇑conj_act.of_conj_act x)⁻¹

@[simp]

theorem conj_act.to_conj_act_inv {G : Type u_3} [div_inv_monoid G] (x : G) :

⇑conj_act.to_conj_act x⁻¹ = (⇑conj_act.to_conj_act x)⁻¹

@[simp]

theorem conj_act.of_conj_act_mul {G : Type u_3} [div_inv_monoid G] (x y : conj_act G) :

⇑conj_act.of_conj_act (x * y) = ⇑conj_act.of_conj_act x * ⇑conj_act.of_conj_act y

@[simp]

theorem conj_act.to_conj_act_mul {G : Type u_3} [div_inv_monoid G] (x y : G) :

⇑conj_act.to_conj_act (x * y) = ⇑conj_act.to_conj_act x * ⇑conj_act.to_conj_act y

@[protected, instance]

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

has_smul (conj_act G) G

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)⁻¹}

theorem conj_act.smul_def {G : Type u_3} [div_inv_monoid G] (g : conj_act G) (h : G) :

g • h = ⇑conj_act.of_conj_act g * h * (⇑conj_act.of_conj_act g)⁻¹

@[protected, instance]

def conj_act.has_units_scalar {M : Type u_2} [monoid M] :

has_smul (conj_act Mˣ) M

Equations

conj_act.has_units_scalar = {smul := λ (g : conj_act Mˣ) (h : M), ↑(⇑conj_act.of_conj_act g) * h * ↑(⇑conj_act.of_conj_act g)⁻¹}

theorem conj_act.units_smul_def {M : Type u_2} [monoid M] (g : conj_act Mˣ) (h : M) :

g • h = ↑(⇑conj_act.of_conj_act g) * h * ↑(⇑conj_act.of_conj_act g)⁻¹

@[protected, instance]

def conj_act.units_mul_distrib_mul_action {M : Type u_2} [monoid M] :

mul_distrib_mul_action (conj_act Mˣ) M

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 := _}

@[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] :

smul_comm_class α (conj_act 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] :

smul_comm_class (conj_act Mˣ) α M

@[protected, instance]

def conj_act.units_mul_semiring_action {R : Type u_5} [semiring R] :

mul_semiring_action (conj_act Rˣ) R

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_zero := _, smul_add := _}, smul_one := _, smul_mul := _}

@[simp]

theorem conj_act.of_conj_act_zero {G₀ : Type u_4} [group_with_zero G₀] :

⇑conj_act.of_conj_act 0 = 0

@[simp]

theorem conj_act.to_conj_act_zero {G₀ : Type u_4} [group_with_zero G₀] :

⇑conj_act.to_conj_act 0 = 0

@[protected, instance]

def conj_act.mul_action₀ {G₀ : Type u_4} [group_with_zero G₀] :

mul_action (conj_act G₀) G₀

Equations

conj_act.mul_action₀ = {to_has_smul := {smul := has_smul.smul conj_act.has_smul}, one_smul := _, mul_smul := _}

@[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.distrib_mul_action₀ {K : Type u_6} [division_ring K] :

distrib_mul_action (conj_act K) K

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_zero := _, smul_add := _}

@[protected, instance]

def conj_act.mul_distrib_mul_action {G : Type u_3} [group G] :

mul_distrib_mul_action (conj_act G) G

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 := _}

@[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] :

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] :

smul_comm_class (conj_act G) α G

theorem conj_act.smul_eq_mul_aut_conj {G : Type u_3} [group G] (g : conj_act G) (h : G) :

g • h = ⇑(⇑mul_aut.conj (⇑conj_act.of_conj_act g)) h

theorem conj_act.fixed_points_eq_center {G : Type u_3} [group G] :

mul_action.fixed_points (conj_act G) G = ↑(subgroup.center G)

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

@[simp]

theorem conj_act.mem_orbit_conj_act {G : Type u_3} [group G] {g h : G} :

g ∈ mul_action.orbit (conj_act G) h ↔ is_conj g h

theorem conj_act.orbit_rel_conj_act {G : Type u_3} [group G] :

(mul_action.orbit_rel (conj_act G) G).rel = is_conj

theorem conj_act.stabilizer_eq_centralizer {G : Type u_3} [group G] (g : G) :

mul_action.stabilizer (conj_act G) g = subgroup.centralizer ↑(subgroup.zpowers (⇑conj_act.to_conj_act g))

@[protected, instance]

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

has_smul (conj_act G) ↥H

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

Equations

conj_act.subgroup.conj_action = {smul := λ (g : conj_act G) (h : ↥H), ⟨g • ↑h, _⟩}

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] :

mul_distrib_mul_action (conj_act G) ↥H

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

def mul_aut.conj_normal {G : Type u_3} [group G] {H : subgroup G} [hH : H.normal] :

G →* mul_aut ↥H

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

Equations

mul_aut.conj_normal = (mul_distrib_mul_action.to_mul_aut (conj_act G) ↥H).comp conj_act.to_conj_act.to_monoid_hom

@[simp]

theorem mul_aut.conj_normal_apply {G : Type u_3} [group G] {H : subgroup G} [H.normal] (g : G) (h : ↥H) :

↑(⇑(⇑mul_aut.conj_normal g) 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) :

↑(⇑(mul_equiv.symm (⇑mul_aut.conj_normal g)) 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) :

↑(⇑(⇑mul_aut.conj_normal g)⁻¹ h) = g⁻¹ * ↑h * g

theorem mul_aut.conj_normal_coe {G : Type u_3} [group G] {H : subgroup G} [H.normal] {h : ↥H} :

⇑mul_aut.conj_normal ↑h = ⇑mul_aut.conj 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] :

(subgroup.map H.subtype K).normal