Documentation

TauCeti.Algebra.Module.ZMod.MulAut

Automorphisms of a group whose additive copy is a ℤ/nℤ-module #

Let Q be a commutative group whose additive copy Additive Q is a ZMod n-module, for instance an elementary abelian p-group viewed as an 𝔽_p-vector space through AddCommGroup.zmodModule. Every additive endomorphism of a ZMod n-module is ZMod n-linear (ZMod.map_smul), so the group automorphisms of Q are exactly the ZMod n-linear automorphisms of Additive Q. This file records that identification as an isomorphism of groups; composed with a basis it presents the automorphism group of a finite elementary abelian p-group as a general linear group over 𝔽_p.

Main definitions #

source
def TauCeti.mulAutEquivZModLinearEquiv (n : ℕ) (Q : Type u_1) [CommGroup Q] [Module (ZMod n) (Additive Q)] :
MulAut Q ≃* Additive Q ≃ₗ[ZMod n] Additive Q

Group automorphisms are linear automorphisms. For a commutative group Q whose additive copy is a ZMod n-module, an automorphism of Q, read additively, is a ZMod n-linear automorphism of Additive Q, and every linear automorphism arises this way.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.mulAutEquivZModLinearEquiv_apply {n : ℕ} {Q : Type u_1} [CommGroup Q] [Module (ZMod n) (Additive Q)] (σ : MulAut Q) (x : Additive Q) :
    ((mulAutEquivZModLinearEquiv n Q) σ) x = Additive.ofMul (σ (Additive.toMul x))

    The linear automorphism attached to σ acts on Additive Q as σ acts on Q.

    source
    @[simp]
    theorem TauCeti.mulAutEquivZModLinearEquiv_symm_apply {n : ℕ} {Q : Type u_1} [CommGroup Q] [Module (ZMod n) (Additive Q)] (e : Additive Q ≃ₗ[ZMod n] Additive Q) (x : Q) :
    ((mulAutEquivZModLinearEquiv n Q).symm e) x = Additive.toMul (e (Additive.ofMul x))

    The group automorphism attached to a linear automorphism e acts on Q as e acts on Additive Q.