Continuous automorphisms and continuous outer automorphisms

For a topological magma G, the continuous multiplicative self-isomorphisms G ≃ₜ* G form a group under composition, ContinuousAut G. Its multiplication is (φ * ψ) x = φ (ψ x), matching Mathlib's MulAut, and forgetting continuity is an injective homomorphism ContinuousAut.toMulAut : ContinuousAut G →* MulAut G.

The group ContinuousAut G acts faithfully on G by evaluation. This is a MulDistribMulAction, and each individual automorphism acts continuously.

When G is a group whose multiplication is separately continuous, every inner automorphism x ↦ g * x * g⁻¹ is continuous, which gives the homomorphism ContinuousAut.conj : G →* ContinuousAut G, lifting MulAut.conj. Its kernel is the centre of G and its range is normal, so the quotient ContinuousOut G is the group of continuous outer automorphisms. An automorphism that is inner as an abstract automorphism is the continuous inner automorphism by the same element, so its class in ContinuousOut G is trivial.

More generally, conjugation by g restricts to a continuous automorphism of every normal subgroup N, which gives ContinuousAut.conjNormal : G →* ContinuousAut N, lifting MulAut.conjNormal, with kernel the centralizer of N.

For a profinite group an abstract automorphism need not be continuous, so ContinuousAut G can be a proper subgroup of MulAut G. It is the group on which the congruence topology of a profinite group is placed, and ContinuousOut G is the target of outer actions such as the outer Galois action on a profinite fundamental group.

Main definitions

• TauCeti.ContinuousAut G: the group G ≃ₜ* G of continuous automorphisms.
• TauCeti.ContinuousAut.toMulAut: the forgetful homomorphism ContinuousAut G →* MulAut G.
• TauCeti.ContinuousAut.smul_def: the action of a continuous automorphism is evaluation.
• TauCeti.ContinuousAut.conj: the inner automorphisms, conj g x = g * x * g⁻¹.
• TauCeti.ContinuousAut.conjNormal: conjugation on a normal subgroup, conjNormal g n = g * n * g⁻¹.
• TauCeti.ContinuousOut G: the quotient of ContinuousAut G by the inner automorphisms, with quotient map TauCeti.ContinuousOut.mk.
• TauCeti.ContinuousOut.mulEquivOfIsMulCommutative: for commutative G, the outer automorphism group is the automorphism group.

Main results

• TauCeti.ContinuousAut.toMulAut_injective: a continuous automorphism is determined by its underlying abstract automorphism.
• TauCeti.ContinuousAut.ker_conj: the kernel of conj is the centre of G, so conj is injective exactly when the centre is trivial (conj_injective_iff) and trivial exactly when G is commutative (range_conj_eq_bot_iff).
• TauCeti.ContinuousAut.ker_conjNormal: the kernel of conjugation on a normal subgroup N is the centralizer of N.
• TauCeti.ContinuousAut.conjNormal_coe: conjugation by an element of N is the inner automorphism of N by that element.
• TauCeti.ContinuousAut.mul_conj_mul_inv: φ * conj g * φ⁻¹ = conj (φ g), so the range of conj is normal.
• TauCeti.ContinuousAut.eq_conj_of_toMulAut_eq_conj: an automorphism that is inner as an abstract automorphism is the continuous inner automorphism.
• TauCeti.ContinuousOut.mk_eq_one_iff: the class of φ in ContinuousOut G is trivial exactly when the underlying abstract automorphism is inner.

References

• L. Ribes, P. Zalesskii, Profinite Groups, 2nd ed., §4.4.

@[reducible, inline]

abbrev TauCeti.ContinuousAut (G : Type u_1) [Mul G] [TopologicalSpace G] : Type u_1

The group of continuous automorphisms of a topological magma G: the continuous multiplicative isomorphisms G ≃ₜ* G, under composition.

Equations

• TauCeti.ContinuousAut G = (G ≃ₜ* G)

@[instance_reducible]

instance TauCeti.ContinuousAut.instGroup (G : Type u_1) [Mul G] [TopologicalSpace G] : Group (ContinuousAut G)

Continuous automorphisms form a group under composition: φ * ψ = ψ.trans φ, so that (φ * ψ) x = φ (ψ x) as for MulAut.

Equations

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

@[simp]

theorem TauCeti.ContinuousAut.coe_mul {G : Type u_1} [Mul G] [TopologicalSpace G] (φ ψ : ContinuousAut G) : ⇑(φ * ψ) = ⇑φ ∘ ⇑ψ

@[simp]

theorem TauCeti.ContinuousAut.coe_one {G : Type u_1} [Mul G] [TopologicalSpace G] : ⇑1 = id

@[simp]

theorem TauCeti.ContinuousAut.coe_inv {G : Type u_1} [Mul G] [TopologicalSpace G] (φ : ContinuousAut G) : ⇑φ⁻¹ = ⇑(ContinuousMulEquiv.symm φ)

theorem TauCeti.ContinuousAut.mul_def {G : Type u_1} [Mul G] [TopologicalSpace G] (φ ψ : ContinuousAut G) : φ * ψ = ContinuousMulEquiv.trans ψ φ

theorem TauCeti.ContinuousAut.one_def {G : Type u_1} [Mul G] [TopologicalSpace G] : 1 = ContinuousMulEquiv.refl G

theorem TauCeti.ContinuousAut.inv_def {G : Type u_1} [Mul G] [TopologicalSpace G] (φ : ContinuousAut G) : φ⁻¹ = ContinuousMulEquiv.symm φ

@[simp]

theorem TauCeti.ContinuousAut.mul_apply {G : Type u_1} [Mul G] [TopologicalSpace G] (φ ψ : ContinuousAut G) (x : G) : (φ * ψ) x = φ (ψ x)

@[simp]

theorem TauCeti.ContinuousAut.one_apply {G : Type u_1} [Mul G] [TopologicalSpace G] (x : G) : 1 x = x

@[simp]

theorem TauCeti.ContinuousAut.inv_apply {G : Type u_1} [Mul G] [TopologicalSpace G] (φ : ContinuousAut G) (x : G) : φ⁻¹ x = (ContinuousMulEquiv.symm φ) x

def TauCeti.ContinuousAut.toMulAut {G : Type u_1} [Mul G] [TopologicalSpace G] : ContinuousAut G →* MulAut G

The forgetful homomorphism from continuous automorphisms to abstract automorphisms.

Equations

• TauCeti.ContinuousAut.toMulAut = { toFun := fun (φ : TauCeti.ContinuousAut G) => φ.toMulEquiv, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.ContinuousAut.coe_toMulAut {G : Type u_1} [Mul G] [TopologicalSpace G] (φ : ContinuousAut G) : ⇑(toMulAut φ) = ⇑φ

theorem TauCeti.ContinuousAut.toMulAut_injective {G : Type u_1} [Mul G] [TopologicalSpace G] : Function.Injective ⇑toMulAut

A continuous automorphism is determined by its underlying abstract automorphism.

@[instance_reducible]

instance TauCeti.ContinuousAut.instMulDistribMulAction (G : Type u_1) [Monoid G] [TopologicalSpace G] : MulDistribMulAction (ContinuousAut G) G

Continuous automorphisms act on their underlying monoid by evaluation.

Equations

• TauCeti.ContinuousAut.instMulDistribMulAction G = MulDistribMulAction.compHom G TauCeti.ContinuousAut.toMulAut

@[simp]

theorem TauCeti.ContinuousAut.smul_def (G : Type u_1) [Monoid G] [TopologicalSpace G] (φ : ContinuousAut G) (x : G) : φ • x = φ x

The action of a continuous automorphism is its evaluation.

instance TauCeti.ContinuousAut.instFaithfulSMul (G : Type u_1) [Monoid G] [TopologicalSpace G] : FaithfulSMul (ContinuousAut G) G

The evaluation action of continuous automorphisms is faithful.

instance TauCeti.ContinuousAut.instContinuousConstSMul (G : Type u_1) [Monoid G] [TopologicalSpace G] : ContinuousConstSMul (ContinuousAut G) G

Each continuous automorphism acts continuously on its underlying monoid.

def TauCeti.ContinuousAut.conj {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] : G →* ContinuousAut G

The inner automorphisms of a group with separately continuous multiplication: conj g x = g * x * g⁻¹. This lifts MulAut.conj along toMulAut (toMulAut_conj).

Equations

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

@[simp]

theorem TauCeti.ContinuousAut.conj_apply {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (g x : G) : (conj g) x = g * x * g⁻¹

@[simp]

theorem TauCeti.ContinuousAut.conj_symm_apply {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (g x : G) : (ContinuousMulEquiv.symm (conj g)) x = g⁻¹ * x * g

theorem TauCeti.ContinuousAut.conj_inv_apply {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (g x : G) : (conj g)⁻¹ x = g⁻¹ * x * g

@[simp]

theorem TauCeti.ContinuousAut.toMulAut_conj {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (g : G) : toMulAut (conj g) = MulAut.conj g

theorem TauCeti.ContinuousAut.ker_conj {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] : conj.ker = Subgroup.center G

The kernel of the inner-automorphism homomorphism is the centre.

theorem TauCeti.ContinuousAut.conj_injective_iff {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] : Function.Injective ⇑conj ↔ Subgroup.center G = ⊥

Conjugation is injective exactly when the centre is trivial.

theorem TauCeti.ContinuousAut.range_conj_eq_bot_iff {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] : conj.range = ⊥ ↔ IsMulCommutative G

Every inner automorphism is trivial exactly when G is commutative.

theorem TauCeti.ContinuousAut.mul_conj_mul_inv {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (φ : ContinuousAut G) (g : G) : φ * conj g * φ⁻¹ = conj (φ g)

Conjugating an inner automorphism by a continuous automorphism φ gives the inner automorphism by the image under φ.

instance TauCeti.ContinuousAut.normal_range_conj {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] : conj.range.Normal

The inner automorphisms form a normal subgroup of the continuous automorphisms.

theorem TauCeti.ContinuousAut.eq_conj_of_toMulAut_eq_conj {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {φ : ContinuousAut G} {g : G} (h : toMulAut φ = MulAut.conj g) : φ = conj g

A continuous automorphism that is inner as an abstract automorphism is the continuous inner automorphism by the same element.

theorem TauCeti.ContinuousAut.toMulAut_mem_range_conj_iff {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {φ : ContinuousAut G} : toMulAut φ ∈ MulAut.conj.range ↔ φ ∈ conj.range

A continuous automorphism is inner exactly when its underlying abstract automorphism is.

def TauCeti.ContinuousAut.conjNormal {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {N : Subgroup G} [N.Normal] : G →* ContinuousAut ↥N

Conjugation of G on a normal subgroup N, as continuous automorphisms of N with the subspace topology: conjNormal g n = g * n * g⁻¹. This lifts MulAut.conjNormal along toMulAut (toMulAut_conjNormal).

Equations

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

@[simp]

theorem TauCeti.ContinuousAut.conjNormal_apply {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {N : Subgroup G} [N.Normal] (g : G) (n : ↥N) : ↑((conjNormal g) n) = g * ↑n * g⁻¹

@[simp]

theorem TauCeti.ContinuousAut.conjNormal_symm_apply {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {N : Subgroup G} [N.Normal] (g : G) (n : ↥N) : ↑((ContinuousMulEquiv.symm (conjNormal g)) n) = g⁻¹ * ↑n * g

theorem TauCeti.ContinuousAut.conjNormal_inv_apply {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {N : Subgroup G} [N.Normal] (g : G) (n : ↥N) : ↑((conjNormal g)⁻¹ n) = g⁻¹ * ↑n * g

@[simp]

theorem TauCeti.ContinuousAut.toMulAut_conjNormal {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {N : Subgroup G} [N.Normal] (g : G) : toMulAut (conjNormal g) = MulAut.conjNormal g

@[simp]

theorem TauCeti.ContinuousAut.conjNormal_coe {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {N : Subgroup G} [N.Normal] (n : ↥N) : conjNormal ↑n = conj n

Conjugation by an element of N is the inner automorphism of N by that element.

theorem TauCeti.ContinuousAut.ker_conjNormal {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {N : Subgroup G} [N.Normal] : conjNormal.ker = Subgroup.centralizer ↑N

The kernel of conjugation on a normal subgroup N is the centralizer of N.

@[reducible, inline]

abbrev TauCeti.ContinuousOut (G : Type u_1) [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] : Type u_1

The group of continuous outer automorphisms of G: continuous automorphisms modulo the inner ones.

Equations

• TauCeti.ContinuousOut G = (TauCeti.ContinuousAut G ⧸ TauCeti.ContinuousAut.conj.range)

@[reducible, inline]

abbrev TauCeti.ContinuousOut.mk {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] : ContinuousAut G →* ContinuousOut G

The quotient map from continuous automorphisms to continuous outer automorphisms.

Equations

• TauCeti.ContinuousOut.mk = QuotientGroup.mk' TauCeti.ContinuousAut.conj.range

@[simp]

theorem TauCeti.ContinuousOut.mk_conj {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (g : G) : ↑(ContinuousAut.conj g) = 1

Inner automorphisms have trivial outer class.

theorem TauCeti.ContinuousOut.mk_eq_one_iff {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {φ : ContinuousAut G} : mk φ = 1 ↔ ContinuousAut.toMulAut φ ∈ MulAut.conj.range

The class of a continuous automorphism in ContinuousOut G is trivial exactly when its underlying abstract automorphism is inner.

def TauCeti.ContinuousOut.mulEquivOfIsMulCommutative {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] [IsMulCommutative G] : ContinuousOut G ≃* ContinuousAut G

For commutative G every inner automorphism is trivial, so the continuous outer automorphism group is the continuous automorphism group.

Equations

• TauCeti.ContinuousOut.mulEquivOfIsMulCommutative = (QuotientGroup.quotientMulEquivOfEq ⋯).trans QuotientGroup.quotientBot

@[simp]

theorem TauCeti.ContinuousOut.mulEquivOfIsMulCommutative_mk {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] [IsMulCommutative G] (φ : ContinuousAut G) : mulEquivOfIsMulCommutative ↑φ = φ

@[simp]

theorem TauCeti.ContinuousOut.mulEquivOfIsMulCommutative_symm_apply {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] [IsMulCommutative G] (φ : ContinuousAut G) : mulEquivOfIsMulCommutative.symm φ = ↑φ