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_3) : Type u_3

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

Equations

• ConjAct G = G

instance ConjAct.instGroup {G : Type u_3} [Group G] : Group (ConjAct G)

Equations

• ConjAct.instGroup = inst

instance ConjAct.instDivInvMonoid {G : Type u_3} [DivInvMonoid G] : DivInvMonoid (ConjAct G)

Equations

• ConjAct.instDivInvMonoid = inst

instance ConjAct.instGroupWithZero {G : Type u_3} [GroupWithZero G] : GroupWithZero (ConjAct G)

Equations

• ConjAct.instGroupWithZero = inst

instance ConjAct.instFintype {G : Type u_3} [Fintype G] : Fintype (ConjAct G)

Equations

• ConjAct.instFintype = inst

@[simp]

theorem ConjAct.card {G : Type u_3} [Fintype G] : Fintype.card (ConjAct G) = Fintype.card G

instance ConjAct.instInhabited {G : Type u_3} [DivInvMonoid G] : Inhabited (ConjAct G)

Equations

• ConjAct.instInhabited = { default := 1 }

def ConjAct.ofConjAct {G : Type u_3} [DivInvMonoid G] : ConjAct G ≃* G

Reinterpret g : ConjAct G as an element of G.

Equations

• ConjAct.ofConjAct = { toFun := id, invFun := id, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

def ConjAct.toConjAct {G : Type u_3} [DivInvMonoid G] : G ≃* ConjAct G

Reinterpret g : G as an element of ConjAct G.

Equations

• ConjAct.toConjAct = ConjAct.ofConjAct.symm

def ConjAct.rec {G : Type u_3} [DivInvMonoid G] {C : ConjAct G → Sort u_7} (h : (g : G) → C (ConjAct.toConjAct g)) (g : ConjAct G) : C g

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

Equations

• ConjAct.rec h = h

@[simp]

theorem ConjAct.forall {G : Type u_3} [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_3} [DivInvMonoid G] : ConjAct.ofConjAct.symm = ConjAct.toConjAct

@[simp]

theorem ConjAct.to_mul_symm_eq {G : Type u_3} [DivInvMonoid G] : ConjAct.toConjAct.symm = ConjAct.ofConjAct

@[simp]

theorem ConjAct.toConjAct_ofConjAct {G : Type u_3} [DivInvMonoid G] (x : ConjAct G) : ConjAct.toConjAct (ConjAct.ofConjAct x) = x

@[simp]

theorem ConjAct.ofConjAct_toConjAct {G : Type u_3} [DivInvMonoid G] (x : G) : ConjAct.ofConjAct (ConjAct.toConjAct x) = x

theorem ConjAct.ofConjAct_one {G : Type u_3} [DivInvMonoid G] : ConjAct.ofConjAct 1 = 1

theorem ConjAct.toConjAct_one {G : Type u_3} [DivInvMonoid G] : ConjAct.toConjAct 1 = 1

@[simp]

theorem ConjAct.ofConjAct_inv {G : Type u_3} [DivInvMonoid G] (x : ConjAct G) : ConjAct.ofConjAct x⁻¹ = (ConjAct.ofConjAct x)⁻¹

@[simp]

theorem ConjAct.toConjAct_inv {G : Type u_3} [DivInvMonoid G] (x : G) : ConjAct.toConjAct x⁻¹ = (ConjAct.toConjAct x)⁻¹

theorem ConjAct.ofConjAct_mul {G : Type u_3} [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_3} [DivInvMonoid G] (x : G) (y : G) : ConjAct.toConjAct (x * y) = ConjAct.toConjAct x * ConjAct.toConjAct y

instance ConjAct.instSMul {G : Type u_3} [DivInvMonoid G] : SMul (ConjAct G) G

Equations

• ConjAct.instSMul = { smul := fun (g : ConjAct G) (h : G) => ConjAct.ofConjAct g * h * (ConjAct.ofConjAct g)⁻¹ }

theorem ConjAct.smul_def {G : Type u_3} [DivInvMonoid G] (g : ConjAct G) (h : G) : g • h = ConjAct.ofConjAct g * h * (ConjAct.ofConjAct g)⁻¹

theorem ConjAct.toConjAct_smul {G : Type u_3} [DivInvMonoid G] (g : G) (h : G) : ConjAct.toConjAct g • h = g * h * g⁻¹

instance ConjAct.unitsScalar {M : Type u_2} [Monoid M] : SMul (ConjAct Mˣ) M

Equations

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

theorem ConjAct.units_smul_def {M : Type u_2} [Monoid M] (g : ConjAct Mˣ) (h : M) : g • h = ↑(ConjAct.ofConjAct g) * h * ↑(ConjAct.ofConjAct g)⁻¹

instance ConjAct.unitsMulDistribMulAction {M : Type u_2} [Monoid M] : MulDistribMulAction (ConjAct Mˣ) M

Equations

• ConjAct.unitsMulDistribMulAction = MulDistribMulAction.mk ⋯ ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance ConjAct.unitsMulSemiringAction {R : Type u_5} [Semiring R] : MulSemiringAction (ConjAct Rˣ) R

Equations

• ConjAct.unitsMulSemiringAction = MulSemiringAction.mk ⋯ ⋯

theorem ConjAct.ofConjAct_zero {G₀ : Type u_4} [GroupWithZero G₀] : ConjAct.ofConjAct 0 = 0

theorem ConjAct.toConjAct_zero {G₀ : Type u_4} [GroupWithZero G₀] : ConjAct.toConjAct 0 = 0

instance ConjAct.mulAction₀ {G₀ : Type u_4} [GroupWithZero G₀] : MulAction (ConjAct G₀) G₀

Equations

• ConjAct.mulAction₀ = MulAction.mk ⋯ ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance ConjAct.distribMulAction₀ {K : Type u_6} [DivisionRing K] : DistribMulAction (ConjAct K) K

Equations

• ConjAct.distribMulAction₀ = DistribMulAction.mk ⋯ ⋯

instance ConjAct.instMulDistribMulAction {G : Type u_3} [Group G] : MulDistribMulAction (ConjAct G) G

Equations

• ConjAct.instMulDistribMulAction = MulDistribMulAction.mk ⋯ ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem ConjAct.smul_eq_mulAut_conj {G : Type u_3} [Group G] (g : ConjAct G) (h : G) : g • h = (MulAut.conj (ConjAct.ofConjAct g)) h

theorem ConjAct.fixedPoints_eq_center {G : Type u_3} [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.

@[simp]

theorem ConjAct.mem_orbit_conjAct {G : Type u_3} [Group G] {g : G} {h : G} : g ∈ MulAction.orbit (ConjAct G) h ↔ IsConj g h

theorem ConjAct.orbitRel_conjAct {G : Type u_3} [Group G] : ⇑(MulAction.orbitRel (ConjAct G) G) = IsConj

theorem ConjAct.orbit_eq_carrier_conjClasses {G : Type u_3} [Group G] (g : G) : MulAction.orbit (ConjAct G) g = (ConjClasses.mk g).carrier

theorem ConjAct.stabilizer_eq_centralizer {G : Type u_3} [Group G] (g : G) : MulAction.stabilizer (ConjAct G) g = Subgroup.centralizer ↑(Subgroup.zpowers (ConjAct.toConjAct g))

theorem Subgroup.centralizer_eq_comap_stabilizer {G : Type u_3} [Group G] (g : G) : Subgroup.centralizer {g} = Subgroup.comap ConjAct.toConjAct.toMonoidHom (MulAction.stabilizer (ConjAct G) g)

instance ConjAct.Subgroup.conjAction {G : Type u_3} [Group G] {H : Subgroup G} [hH : H.Normal] : SMul (ConjAct G) ↥H

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

Equations

• ConjAct.Subgroup.conjAction = { smul := fun (g : ConjAct G) (h : ↥H) => ⟨g • ↑h, ⋯⟩ }

theorem ConjAct.Subgroup.val_conj_smul {G : Type u_3} [Group G] {H : Subgroup G} [H.Normal] (g : ConjAct G) (h : ↥H) : ↑(g • h) = g • ↑h

instance ConjAct.Subgroup.conjMulDistribMulAction {G : Type u_3} [Group G] {H : Subgroup G} [H.Normal] : MulDistribMulAction (ConjAct G) ↥H

Equations

• ConjAct.Subgroup.conjMulDistribMulAction = Function.Injective.mulDistribMulAction H.subtype ⋯ ⋯

def MulAut.conjNormal {G : Type u_3} [Group G] {H : Subgroup G} [H.Normal] : G →* MulAut ↥H

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

Equations

• MulAut.conjNormal = (MulDistribMulAction.toMulAut (ConjAct G) ↥H).comp ConjAct.toConjAct.toMonoidHom

@[simp]

theorem MulAut.conjNormal_apply {G : Type u_3} [Group G] {H : Subgroup G} [H.Normal] (g : G) (h : ↥H) : ↑((MulAut.conjNormal g) h) = g * ↑h * g⁻¹

@[simp]

theorem MulAut.conjNormal_symm_apply {G : Type u_3} [Group G] {H : Subgroup G} [H.Normal] (g : G) (h : ↥H) : ↑((MulEquiv.symm (MulAut.conjNormal g)) h) = g⁻¹ * ↑h * g

@[simp]

theorem MulAut.conjNormal_inv_apply {G : Type u_3} [Group G] {H : Subgroup G} [H.Normal] (g : G) (h : ↥H) : ↑((MulAut.conjNormal g)⁻¹ h) = g⁻¹ * ↑h * g

theorem MulAut.conjNormal_val {G : Type u_3} [Group G] {H : Subgroup G} [H.Normal] {h : ↥H} : MulAut.conjNormal ↑h = MulAut.conj h

instance ConjAct.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

Equations

• ⋯ = ⋯

def unitsCentralizerEquiv (M : Type u_2) [Monoid M] (x : Mˣ) : (↥(Submonoid.centralizer {↑x}))ˣ ≃* ↥(MulAction.stabilizer (ConjAct Mˣ) x)

The stabilizer of Mˣ acting on itself by conjugation at x : Mˣ is exactly the units of the centralizer of x : M.

Equations

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

@[simp]

theorem val_unitsCentralizerEquiv_symm_apply_coe (M : Type u_2) [Monoid M] (x : Mˣ) : ∀ (a : ↥(MulAction.stabilizer (ConjAct Mˣ) x)), ↑↑((unitsCentralizerEquiv M x).symm a) = ↑(ConjAct.ofConjAct ↑a)

@[simp]

theorem val_unitsCentralizerEquiv_apply_coe (M : Type u_2) [Monoid M] (x : Mˣ) : ∀ (a : (↥(Submonoid.centralizer {↑x}))ˣ), ↑↑((unitsCentralizerEquiv M x) a) = ↑↑a