Automorphisms of a quotient by a characteristic subgroup

Every automorphism of a group G maps a characteristic subgroup N onto itself, so it induces an automorphism of the quotient G ⧸ N. This gives the homomorphism MulAut.mapQuotient N : MulAut G →* MulAut (G ⧸ N), the quotient counterpart of Mathlib's MulAut.characteristic N : MulAut G →* MulAut N. Its kernel consists of the automorphisms acting trivially on G ⧸ N. For the Frattini subgroup of a finite p-group this kernel is a p-group, see TauCeti/GroupTheory/Frattini.lean.

Main definitions

• MulAut.mapQuotient N: the automorphism of G ⧸ N induced by an automorphism of G, for a characteristic subgroup N.

Main statements

• MulAut.mapQuotient_mk: the induced automorphism sends the class of x to the class of φ x.
• MulAut.mem_ker_mapQuotient_iff: an automorphism induces the identity on G ⧸ N exactly when it fixes every class modulo N.

def MulAut.mapQuotient {G : Type u_1} [Group G] (N : Subgroup G) [N.Characteristic] : MulAut G →* MulAut (G ⧸ N)

The automorphism of the quotient G ⧸ N by a characteristic subgroup N induced by an automorphism of G.

@[simp]

theorem MulAut.mapQuotient_mk {G : Type u_1} [Group G] (N : Subgroup G) [N.Characteristic] (φ : MulAut G) (x : G) : ((mapQuotient N) φ) ↑x = ↑(φ x)

The automorphism induced on G ⧸ N sends the class of x to the class of φ x.

theorem MulAut.mem_ker_mapQuotient_iff {G : Type u_1} [Group G] (N : Subgroup G) [N.Characteristic] {φ : MulAut G} : φ ∈ (mapQuotient N).ker ↔ ∀ (x : G), ↑(φ x) = ↑x

An automorphism of G induces the identity on G ⧸ N exactly when it fixes every class modulo N.