Documentation

Mathlib.GroupTheory.GroupAction.ConjAct

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:

ConjAct Mˣ to act on M, when M is a Monoid
ConjAct G₀ to act on G₀, when G₀ is a GroupWithZero

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.

def ConjAct (G : Type u_1) :

Type u_1

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

Equations

ConjAct G = G

instance ConjAct.instGroupConjAct {G : Type u_1} [inst : Group G] :

Group (ConjAct G)

Equations

ConjAct.instGroupConjAct = inst

instance ConjAct.instDivInvMonoidConjAct {G : Type u_1} [inst : DivInvMonoid G] :

DivInvMonoid (ConjAct G)

Equations

ConjAct.instDivInvMonoidConjAct = inst

instance ConjAct.instGroupWithZeroConjAct {G : Type u_1} [inst : GroupWithZero G] :

GroupWithZero (ConjAct G)

Equations

ConjAct.instGroupWithZeroConjAct = inst

instance ConjAct.instFintypeConjAct {G : Type u_1} [inst : Fintype G] :

Fintype (ConjAct G)

Equations

ConjAct.instFintypeConjAct = inst

@[simp]

theorem ConjAct.card {G : Type u_1} [inst : Fintype G] :

Fintype.card (ConjAct G) = Fintype.card G

instance ConjAct.instInhabitedConjAct {G : Type u_1} [inst : DivInvMonoid G] :

Inhabited (ConjAct G)

Equations

ConjAct.instInhabitedConjAct = { default := 1 }

def ConjAct.ofConjAct {G : Type u_1} [inst : DivInvMonoid G] :

ConjAct G ≃* G

Reinterpret g : ConjAct G as an element of G.

Equations

One or more equations did not get rendered due to their size.

def ConjAct.toConjAct {G : Type u_1} [inst : DivInvMonoid G] :

G ≃* ConjAct G

Reinterpret g : G as an element of ConjAct G.

Equations

ConjAct.toConjAct = MulEquiv.symm ConjAct.ofConjAct

def ConjAct.rec {G : Type u_1} [inst : DivInvMonoid G] {C : ConjAct G → Sort u_2} (h : (g : G) → C (↑ConjAct.toConjAct g)) (g : ConjAct G) :

C g

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

Equations

ConjAct.rec h = h

@[simp]

theorem ConjAct.forall {G : Type u_1} [inst : DivInvMonoid G] (p : ConjAct G → Prop) :

((x : ConjAct G) → p x) ↔ (x : G) → p (↑ConjAct.toConjAct x)

@[simp]

theorem ConjAct.of_mul_symm_eq {G : Type u_1} [inst : DivInvMonoid G] :

MulEquiv.symm ConjAct.ofConjAct = ConjAct.toConjAct

@[simp]

theorem ConjAct.to_mul_symm_eq {G : Type u_1} [inst : DivInvMonoid G] :

MulEquiv.symm ConjAct.toConjAct = ConjAct.ofConjAct

@[simp]

theorem ConjAct.toConjAct_ofConjAct {G : Type u_1} [inst : DivInvMonoid G] (x : ConjAct G) :

↑ConjAct.toConjAct (↑ConjAct.ofConjAct x) = x

@[simp]

theorem ConjAct.ofConjAct_toConjAct {G : Type u_1} [inst : DivInvMonoid G] (x : G) :

↑ConjAct.ofConjAct (↑ConjAct.toConjAct x) = x

theorem ConjAct.ofConjAct_one {G : Type u_1} [inst : DivInvMonoid G] :

↑ConjAct.ofConjAct 1 = 1

theorem ConjAct.toConjAct_one {G : Type u_1} [inst : DivInvMonoid G] :

↑ConjAct.toConjAct 1 = 1

@[simp]

theorem ConjAct.ofConjAct_inv {G : Type u_1} [inst : DivInvMonoid G] (x : ConjAct G) :

↑ConjAct.ofConjAct x⁻¹ = (↑ConjAct.ofConjAct x)⁻¹

@[simp]

theorem ConjAct.toConjAct_inv {G : Type u_1} [inst : DivInvMonoid G] (x : G) :

↑ConjAct.toConjAct x⁻¹ = (↑ConjAct.toConjAct x)⁻¹

theorem ConjAct.ofConjAct_mul {G : Type u_1} [inst : DivInvMonoid G] (x : ConjAct G) (y : ConjAct G) :

↑ConjAct.ofConjAct (x * y) = ↑ConjAct.ofConjAct x * ↑ConjAct.ofConjAct y

theorem ConjAct.toConjAct_mul {G : Type u_1} [inst : DivInvMonoid G] (x : G) (y : G) :

↑ConjAct.toConjAct (x * y) = ↑ConjAct.toConjAct x * ↑ConjAct.toConjAct y

instance ConjAct.instSMulConjAct {G : Type u_1} [inst : DivInvMonoid G] :

SMul (ConjAct G) G

Equations

ConjAct.instSMulConjAct = { smul := fun g h => ↑ConjAct.ofConjAct g * h * (↑ConjAct.ofConjAct g)⁻¹ }

theorem ConjAct.smul_def {G : Type u_1} [inst : DivInvMonoid G] (g : ConjAct G) (h : G) :

g • h = ↑ConjAct.ofConjAct g * h * (↑ConjAct.ofConjAct g)⁻¹

instance ConjAct.unitsScalar {M : Type u_1} [inst : Monoid M] :

SMul (ConjAct Mˣ) M

Equations

ConjAct.unitsScalar = { smul := fun g h => ↑(↑ConjAct.ofConjAct g) * h * ↑(↑ConjAct.ofConjAct g)⁻¹ }

theorem ConjAct.units_smul_def {M : Type u_1} [inst : Monoid M] (g : ConjAct Mˣ) (h : M) :

g • h = ↑(↑ConjAct.ofConjAct g) * h * ↑(↑ConjAct.ofConjAct g)⁻¹

instance ConjAct.unitsMulDistribMulAction {M : Type u_1} [inst : Monoid M] :

MulDistribMulAction (ConjAct Mˣ) M

Equations

One or more equations did not get rendered due to their size.

instance ConjAct.unitsSMulCommClass (α : Type u_1) {M : Type u_2} [inst : Monoid M] [inst : SMul α M] [inst : SMulCommClass α M M] [inst : IsScalarTower α M M] :

SMulCommClass α (ConjAct Mˣ) M

Equations

ConjAct.unitsSMulCommClass = ConjAct.unitsSMulCommClass.proof_1

instance ConjAct.unitsSMulCommClass' (α : Type u_1) {M : Type u_2} [inst : Monoid M] [inst : SMul α M] [inst : SMulCommClass M α M] [inst : IsScalarTower α M M] :

SMulCommClass (ConjAct Mˣ) α M

Equations

ConjAct.unitsSMulCommClass' = ConjAct.unitsSMulCommClass'.proof_1

instance ConjAct.unitsMulSemiringAction {R : Type u_1} [inst : Semiring R] :

MulSemiringAction (ConjAct Rˣ) R

Equations

One or more equations did not get rendered due to their size.

theorem ConjAct.ofConjAct_zero {G₀ : Type u_1} [inst : GroupWithZero G₀] :

↑ConjAct.ofConjAct 0 = 0

theorem ConjAct.toConjAct_zero {G₀ : Type u_1} [inst : GroupWithZero G₀] :

↑ConjAct.toConjAct 0 = 0

instance ConjAct.mulAction₀ {G₀ : Type u_1} [inst : GroupWithZero G₀] :

MulAction (ConjAct G₀) G₀

Equations

ConjAct.mulAction₀ = MulAction.mk (_ : ∀ (b : G₀), 1 • b = b) (_ : ∀ (x y : ConjAct G₀) (b : G₀), (x * y) • b = x • y • b)

instance ConjAct.smulCommClass₀ (α : Type u_1) {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst : SMul α G₀] [inst : SMulCommClass α G₀ G₀] [inst : IsScalarTower α G₀ G₀] :

SMulCommClass α (ConjAct G₀) G₀

Equations

ConjAct.smulCommClass₀ = ConjAct.smulCommClass₀.proof_1

instance ConjAct.smulCommClass₀' (α : Type u_1) {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst : SMul α G₀] [inst : SMulCommClass G₀ α G₀] [inst : IsScalarTower α G₀ G₀] :

SMulCommClass (ConjAct G₀) α G₀

Equations

ConjAct.smulCommClass₀' = ConjAct.smulCommClass₀'.proof_1

instance ConjAct.distribMulAction₀ {K : Type u_1} [inst : DivisionRing K] :

DistribMulAction (ConjAct K) K

Equations

ConjAct.distribMulAction₀ = let src := ConjAct.mulAction₀; DistribMulAction.mk (_ : ∀ (a : ConjAct K), a • 0 = 0) (_ : ∀ (a : ConjAct K) (x y : K), a • (x + y) = a • x + a • y)

instance ConjAct.instMulDistribMulActionConjActToMonoidInstDivInvMonoidConjActToDivInvMonoid {G : Type u_1} [inst : Group G] :

MulDistribMulAction (ConjAct G) G

Equations

One or more equations did not get rendered due to their size.

instance ConjAct.instMulActionConjActToMonoidInstDivInvMonoidConjActToDivInvMonoid {G : Type u_1} [inst : Group G] :

MulAction (ConjAct G) G

Equations

ConjAct.instMulActionConjActToMonoidInstDivInvMonoidConjActToDivInvMonoid = MulDistribMulAction.toMulAction

instance ConjAct.smulCommClass (α : Type u_1) {G : Type u_2} [inst : Group G] [inst : SMul α G] [inst : SMulCommClass α G G] [inst : IsScalarTower α G G] :

SMulCommClass α (ConjAct G) G

Equations

ConjAct.smulCommClass = ConjAct.smulCommClass.proof_1

instance ConjAct.smulCommClass' (α : Type u_1) {G : Type u_2} [inst : Group G] [inst : SMul α G] [inst : SMulCommClass G α G] [inst : IsScalarTower α G G] :

SMulCommClass (ConjAct G) α G

Equations

ConjAct.smulCommClass' = ConjAct.smulCommClass'.proof_1

theorem ConjAct.smul_eq_mulAut_conj {G : Type u_1} [inst : Group G] (g : ConjAct G) (h : G) :

g • h = ↑(↑MulAut.conj (↑ConjAct.ofConjAct g)) h

theorem ConjAct.fixedPoints_eq_center {G : Type u_1} [inst : Group G] :

MulAction.fixedPoints (ConjAct G) G = ↑(Subgroup.center G)

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

theorem ConjAct.stabilizer_eq_centralizer {G : Type u_1} [inst : Group G] (g : G) :

MulAction.stabilizer (ConjAct G) g = Subgroup.centralizer (Subgroup.zpowers g)

instance ConjAct.Subgroup.conjAction {G : Type u_1} [inst : Group G] {H : Subgroup G} [hH : Subgroup.Normal H] :

SMul (ConjAct G) { x // x ∈ H }

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

Equations

ConjAct.Subgroup.conjAction = { smul := fun g h => { val := g • ↑h, property := (_ : ↑ConjAct.ofConjAct g * ↑h * (↑ConjAct.ofConjAct g)⁻¹ ∈ H) } }

theorem ConjAct.Subgroup.val_conj_smul {G : Type u_1} [inst : Group G] {H : Subgroup G} [inst : Subgroup.Normal H] (g : ConjAct G) (h : { x // x ∈ H }) :

↑(g • h) = g • ↑h

instance ConjAct.Subgroup.conjMulDistribMulAction {G : Type u_1} [inst : Group G] {H : Subgroup G} [inst : Subgroup.Normal H] :

MulDistribMulAction (ConjAct G) { x // x ∈ H }

Equations

One or more equations did not get rendered due to their size.

def MulAut.conjNormal {G : Type u_1} [inst : Group G] {H : Subgroup G} [inst : Subgroup.Normal H] :

G →* MulAut { x // x ∈ H }

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

Equations

MulAut.conjNormal = MonoidHom.comp (MulDistribMulAction.toMulAut (ConjAct G) { x // x ∈ H }) (MulEquiv.toMonoidHom ConjAct.toConjAct)

@[simp]

theorem MulAut.conjNormal_apply {G : Type u_1} [inst : Group G] {H : Subgroup G} [inst : Subgroup.Normal H] (g : G) (h : { x // x ∈ H }) :

↑(↑(↑MulAut.conjNormal g) h) = g * ↑h * g⁻¹

@[simp]

theorem MulAut.conjNormal_symm_apply {G : Type u_1} [inst : Group G] {H : Subgroup G} [inst : Subgroup.Normal H] (g : G) (h : { x // x ∈ H }) :

↑(↑(MulEquiv.symm (↑MulAut.conjNormal g)) h) = g⁻¹ * ↑h * g

@[simp]

theorem MulAut.conjNormal_inv_apply {G : Type u_1} [inst : Group G] {H : Subgroup G} [inst : Subgroup.Normal H] (g : G) (h : { x // x ∈ H }) :

↑(↑(↑MulAut.conjNormal g)⁻¹ h) = g⁻¹ * ↑h * g

theorem MulAut.conjNormal_val {G : Type u_1} [inst : Group G] {H : Subgroup G} [inst : Subgroup.Normal H] {h : { x // x ∈ H }} :

↑MulAut.conjNormal ↑h = ↑MulAut.conj h

instance ConjAct.normal_of_characteristic_of_normal {G : Type u_1} [inst : Group G] {H : Subgroup G} [hH : Subgroup.Normal H] {K : Subgroup { x // x ∈ H }} [h : Subgroup.Characteristic K] :

Subgroup.Normal (Subgroup.map (Subgroup.subtype H) K)

Equations

@ConjAct.normal_of_characteristic_of_normal = @ConjAct.normal_of_characteristic_of_normal.proof_1