Continuous outer automorphisms acting on conjugacy classes

A continuous automorphism sends a conjugacy class to the class of its image. Inner automorphisms fix every conjugacy class, so this action factors through the continuous outer automorphism group. These actions are the basic interface for transporting conjugacy-invariant data along outer actions of extensions.

The actions are algebraic: they require a topology on G to specify continuous automorphisms, but no topology on ContinuousAut G or ContinuousOut G.

@[instance_reducible]

instance TauCeti.ContinuousAut.instMulActionConjClasses {G : Type u_1} [TopologicalSpace G] [Monoid G] : MulAction (ContinuousAut G) (ConjClasses G)

A continuous automorphism acts on conjugacy classes by its underlying monoid automorphism.

@[simp]

theorem TauCeti.ContinuousAut.smul_conjClasses_mk {G : Type u_1} [TopologicalSpace G] [Monoid G] (φ : ContinuousAut G) (x : G) : φ • ConjClasses.mk x = ConjClasses.mk (φ x)

The action of a continuous automorphism on a conjugacy class is computed on a representative.

@[simp]

theorem TauCeti.ContinuousAut.smul_conjClasses_pow {G : Type u_1} [TopologicalSpace G] [Monoid G] (φ : ContinuousAut G) (c : ConjClasses G) (n : ℕ) : φ • c ^ n = (φ • c) ^ n

Continuous automorphisms commute with powering conjugacy classes.

@[simp]

theorem TauCeti.ContinuousAut.smul_conjClasses_inv {G : Type u_1} [TopologicalSpace G] [Group G] (φ : ContinuousAut G) (c : ConjClasses G) : φ • c⁻¹ = (φ • c)⁻¹

Continuous automorphisms commute with inversion of conjugacy classes.

@[simp]

theorem TauCeti.ContinuousAut.conj_smul_conjClasses {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (g : G) (c : ConjClasses G) : conj g • c = c

Inner automorphisms fix every conjugacy class.

@[instance_reducible]

instance TauCeti.ContinuousOut.instMulActionConjClasses {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] : MulAction (ContinuousOut G) (ConjClasses G)

The action of continuous automorphisms on conjugacy classes factors through continuous outer automorphisms.

@[simp]

theorem TauCeti.ContinuousOut.mk_smul_conjClasses {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (φ : ContinuousAut G) (c : ConjClasses G) : ↑φ • c = φ • c

The outer action is computed using any representative continuous automorphism.

theorem TauCeti.ContinuousOut.mk_smul_mk {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (φ : ContinuousAut G) (x : G) : ↑φ • ConjClasses.mk x = ConjClasses.mk (φ x)

On the class of an element, the outer action sends it to the class of its image.

@[simp]

theorem TauCeti.ContinuousOut.smul_conjClasses_pow {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (φ : ContinuousOut G) (c : ConjClasses G) (n : ℕ) : φ • c ^ n = (φ • c) ^ n

Continuous outer automorphisms commute with powering conjugacy classes.

@[simp]

theorem TauCeti.ContinuousOut.smul_conjClasses_inv {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (φ : ContinuousOut G) (c : ConjClasses G) : φ • c⁻¹ = (φ • c)⁻¹

Continuous outer automorphisms commute with inversion of conjugacy classes.