The kernel of an action on a cyclic group

Let a group G act by additive automorphisms on a cyclic group A. The action factors through the automorphism group of A, which Mathlib identifies with the units of ZMod (Nat.card A) (IsCyclic.mulAutMulEquiv, read additively through MulAutMultiplicative). Consequently the kernel of the action has index dividing φ (Nat.card A) (index_ker_toPermHom_dvd_totient) and the quotient of G by it is commutative (isMulCommutative_quotient_ker_toPermHom).

For the roots of unity μₙ of a field this says that adjoining μₙ to a field is an abelian extension of degree dividing φ n, the input used to make a finite Galois layer contain μₙ without changing the primes dividing its degree, beyond those dividing φ n.

theorem TauCeti.index_ker_toPermHom_dvd_totient (G : Type u_1) [Group G] (A : Type u_2) [AddGroup A] [DistribMulAction G A] [IsAddCyclic A] : (MulAction.toPermHom G A).ker.index ∣ (Nat.card A).totient

The kernel of an action on a cyclic group has index dividing φ (Nat.card A): the action factors through the automorphism group of A, which has φ (Nat.card A) elements. For an infinite cyclic A the statement is empty, φ 0 = 0.

theorem TauCeti.isMulCommutative_quotient_ker_toPermHom (G : Type u_1) [Group G] (A : Type u_2) [AddGroup A] [DistribMulAction G A] [IsAddCyclic A] : IsMulCommutative (G ⧸ (MulAction.toPermHom G A).ker)

The quotient by the kernel of an action on a cyclic group is commutative: it embeds into the automorphism group of A, the units of ZMod (Nat.card A).