Documentation

TauCeti.GroupTheory.Abelianization.Conjugation

Conjugation on the abelianization of a normal subgroup #

Let N be a normal subgroup of a group G. Conjugation by g ∈ G is an automorphism of N, so it induces an automorphism of the abelianization N^{ab}. Conjugation by an element of N itself is inner, hence invisible in N^{ab}, so the action factors through G ⧸ N: this file makes N^{ab} a G ⧸ N-module, with (g : G ⧸ N) • [n] = [g n g⁻¹] (Abelianization.mk_smul_of).

For N = G' the commutator subgroup, the acting group is G ⧸ G' = G^{ab}, and G' ⧸ G'' is the G^{ab}-module whose extension class is that of G ⧸ G''; this is the coefficient module in which the transfer G → G' ⧸ G'' takes its values. The instance for Abelianization G is recorded separately, because Abelianization G is not reducibly G ⧸ commutator G.

Main definitions #

Main results #

source
noncomputable def Abelianization.conjAut {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] :
G ⧸ N →* MulAut (Abelianization ↥N)

Conjugation by G ⧸ N on N^{ab}: conjugation by g ∈ G on N, carried to N^{ab}, which depends only on the class of g because elements of N act by inner automorphisms.

Instances For
    source
    theorem Abelianization.conjAut_mk_of {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (g : G) (n : ↥N) :
    ((conjAut N) ↑g) (of n) = of ((MulAut.conjNormal g) n)

    conjAut N sends the class of g to conjugation by g on classes.

    source
    @[instance_reducible]
    noncomputable instance Abelianization.instMulDistribMulActionQuotient {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] :
    MulDistribMulAction (G ⧸ N) (Abelianization ↥N)

    The conjugation action of G ⧸ N on N^{ab}, given by conjAut N.

    source
    @[simp]
    theorem Abelianization.conjAut_apply {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (q : G ⧸ N) (x : Abelianization ↥N) :
    ((conjAut N) q) x = q • x

    Applying the automorphism conjAut N q is the action of q.

    source
    @[simp]
    theorem Abelianization.mk_smul_of {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (g : G) (n : ↥N) :
    ↑g • of n = of ((MulAut.conjNormal g) n)

    The defining equation of the action of G ⧸ N on N^{ab}: the class of g sends the class of n to the class of g * n * g⁻¹.

    source
    @[instance_reducible]
    noncomputable instance Abelianization.instMulDistribMulActionCommutator {G : Type u_1} [Group G] :
    MulDistribMulAction (Abelianization G) (Abelianization ↥(commutator G))

    The conjugation action of G^{ab} on G' ⧸ G''.

    source
    @[simp]
    theorem Abelianization.of_smul_of {G : Type u_1} [Group G] (g : G) (n : ↥(commutator G)) :
    of g • of n = of ((MulAut.conjNormal g) n)

    The class of g in G^{ab} acts on G' ⧸ G'' as conjugation by g.