Automorphisms of characteristic quotients

A continuous automorphism of a group with a topology induces an abstract automorphism of each quotient by a topologically characteristic normal subgroup. These quotient automorphisms are the coordinates used in the congruence topology on ContinuousAut G. Two automorphisms share a coordinate exactly when they agree modulo the subgroup at every point, and the formula on quotient classes also shows that inner automorphisms descend to inner automorphisms.

See Ribes–Zalesskii, Profinite Groups, §4.4.

def TauCeti.ContinuousAut.mapQuotient {G : Type u_1} [Group G] [TopologicalSpace G] {N : Subgroup G} (hN : IsTopCharacteristic G N) [N.Normal] : ContinuousAut G →* MulAut (G ⧸ N)

The abstract automorphism of a characteristic quotient induced by a continuous automorphism. For an open normal subgroup this is a coordinate of the congruence topology.

Equations

• TauCeti.ContinuousAut.mapQuotient hN = { toFun := fun (φ : TauCeti.ContinuousAut G) => QuotientGroup.congr N N φ.toMulEquiv ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.ContinuousAut.mapQuotient_mk {G : Type u_1} [Group G] [TopologicalSpace G] {N : Subgroup G} (hN : IsTopCharacteristic G N) [N.Normal] (φ : ContinuousAut G) (x : G) : ((mapQuotient hN) φ) ↑x = ↑(φ x)

The quotient automorphism sends the class of x to the class of φ x.

@[simp]

theorem TauCeti.ContinuousAut.mapQuotient_eq_iff {G : Type u_1} [Group G] [TopologicalSpace G] {N : Subgroup G} (hN : IsTopCharacteristic G N) [N.Normal] {φ ψ : ContinuousAut G} : (mapQuotient hN) φ = (mapQuotient hN) ψ ↔ ∀ (x : G), ↑(φ x) = ↑(ψ x)

Two continuous automorphisms induce the same automorphism of a characteristic quotient exactly when they agree modulo the subgroup at every point.

theorem TauCeti.ContinuousAut.mapOfLE_mapQuotient {G : Type u_1} [Group G] [TopologicalSpace G] {N : Subgroup G} (hN : IsTopCharacteristic G N) {M : Subgroup G} [N.Normal] [M.Normal] (hM : IsTopCharacteristic G M) (hle : N ≤ M) (φ : ContinuousAut G) (q : G ⧸ N) : (QuotientGroup.mapOfLE hle) (((mapQuotient hN) φ) q) = ((mapQuotient hM) φ) ((QuotientGroup.mapOfLE hle) q)

The quotient automorphisms induced by one continuous automorphism on two characteristic quotients G ⧸ N and G ⧸ M, N ≤ M, are compatible with the quotient map G ⧸ N → G ⧸ M.

@[simp]

theorem TauCeti.ContinuousAut.mapQuotient_conj {G : Type u_1} [Group G] [TopologicalSpace G] {N : Subgroup G} (hN : IsTopCharacteristic G N) [SeparatelyContinuousMul G] (g : G) : (mapQuotient hN) (conj g) = MulAut.conj ↑g

The quotient coordinate carries conjugation by g to conjugation by its class.