Documentation

TauCeti.RingTheory.RootsOfUnity.ZMod

ℤ/k and the k-th roots of unity #

A primitive k-th root of unity generates the group of all k-th roots of unity, so Mathlib's IsPrimitiveRoot.zmodEquivZPowers, which identifies ℤ/k with the powers of a chosen primitive root, identifies it with the whole of μ_k.

Both halves are in Mathlib — IsPrimitiveRoot.zmodEquivZPowers and IsPrimitiveRoot.zpowers_eq — but not the composite, which is what a consumer phrased in terms of μ_k rather than a chosen generator needs.

Independently of any primitive root, μ_k of any commutative monoid is killed by k, so written additively it is a ZMod k-module.

Conversely, ℤ/n written multiplicatively is itself a group of n-th roots of unity: ofAdd 1 is a primitive n-th root of unity, and the group is cyclic, so Multiplicative (ZMod n) has enough n-th roots of unity in the sense of Mathlib's duality theory for finite abelian groups. This is what lets that theory serve the groups killed by n, whose characters with values in ℤ/n are their additive homomorphisms to ZMod n.

Main results #

Provenance #

IsPrimitiveRoot.zmodEquivRootsOfUnity is ported from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) @ a302aeacd86053f9d5f991fbbf664e1cc1051d08, source file projects/HasseWeil/HasseWeil/HasseBound/WeilPairing/RootsOfUnity.lean, declaration rootsOfUnity_addEquiv_zmod. Three changes: the direction is reversed to start from ZMod k, so that it reads like IsPrimitiveRoot.zmodEquivZPowers which it extends; the base is a domain rather than a field, which is all zpowers_eq asks for; and the four characterising lemmas below — the equivalence and its inverse, each at an integer and at a natural exponent — are added, none of which the source has. The remaining declarations of this file — the ZMod k-module structure on μ_k written additively and the roots of unity of Multiplicative (ZMod n) — have no counterpart in that source.

source
@[simp]
theorem TauCeti.nsmul_additive_rootsOfUnity_eq_zero {M : Type u_1} [CommMonoid M] (k : ℕ) (x : Additive ↥(rootsOfUnity k M)) :
k • x = 0

μ_k is killed by k: written additively, ζ ^ k = 1 reads k • ζ = 0.

source
@[instance_reducible]
instance TauCeti.instModuleZModAdditiveRootsOfUnity {M : Type u_1} [CommMonoid M] (k : ℕ) :
Module (ZMod k) (Additive ↥(rootsOfUnity k M))

μ_k, written additively, is a ZMod k-module, being killed by k.

Equations
source
theorem TauCeti.ZMod.isPrimitiveRoot_ofAdd_one (n : ℕ) :
IsPrimitiveRoot (Multiplicative.ofAdd 1) n

ofAdd 1 is a primitive n-th root of unity in ℤ/n written multiplicatively: its order is the additive order of 1 : ZMod n, which is n.

source
instance TauCeti.instHasEnoughRootsOfUnityMultiplicativeZMod (n : ℕ) :
HasEnoughRootsOfUnity (Multiplicative (ZMod n)) n

ℤ/n written multiplicatively has enough n-th roots of unity: ofAdd 1 is a primitive one, and its roots of unity form a cyclic group, being a subgroup of the cyclic group of units of Multiplicative (ZMod n).

source
theorem TauCeti.hasEnoughRootsOfUnity_multiplicative_zmod_exponent {n : ℕ} [NeZero n] {M : Type u_2} [AddMonoid M] (hM : ∀ (x : M), n • x = 0) :
HasEnoughRootsOfUnity (Multiplicative (ZMod n)) (Monoid.exponent (Multiplicative M))

ℤ/n written multiplicatively has enough roots of unity for every monoid killed by n: the exponent of such a monoid divides n. This is the hypothesis of Mathlib's duality theory for finite abelian groups, CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity and CommGroup.card_monoidHom_of_hasEnoughRootsOfUnity, with the target Multiplicative (ZMod n).

source
noncomputable def IsPrimitiveRoot.zmodEquivRootsOfUnity {R : Type u_1} [CommRing R] [IsDomain R] {k : ℕ} [NeZero k] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) :
ZMod k ≃+ Additive ↥(rootsOfUnity k R)

ℤ/k is the group of k-th roots of unity, written additively, once a primitive k-th root of unity is chosen: that root generates μ_k, so zmodEquivZPowers already lands on all of it.

Equations
Instances For
    source
    @[simp]
    theorem IsPrimitiveRoot.coe_zmodEquivRootsOfUnity_apply_intCast {R : Type u_1} [CommRing R] [IsDomain R] {k : ℕ} [NeZero k] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℤ) :
    ↑(Additive.toMul (h.zmodEquivRootsOfUnity ↑i)) = ζ ^ i

    The equivalence sends the class of an integer i to ζ ^ i, which determines it on all of ZMod k since every class is the class of an integer.

    source
    @[simp]
    theorem IsPrimitiveRoot.coe_zmodEquivRootsOfUnity_apply_natCast {R : Type u_1} [CommRing R] [IsDomain R] {k : ℕ} [NeZero k] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℕ) :
    ↑(Additive.toMul (h.zmodEquivRootsOfUnity ↑i)) = ζ ^ i

    The equivalence sends the class of a natural number i to ζ ^ i, the natural-exponent reading of coe_zmodEquivRootsOfUnity_apply_intCast.

    source
    @[simp]
    theorem IsPrimitiveRoot.zmodEquivRootsOfUnity_symm_apply_zpow {R : Type u_1} [CommRing R] [IsDomain R] {k : ℕ} [NeZero k] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℤ) (hi : ζ ^ i ∈ rootsOfUnity k R) :
    h.zmodEquivRootsOfUnity.symm (Additive.ofMul ⟨ζ ^ i, hi⟩) = ↑i

    The inverse sends ζ ^ i back to the class of i, for an integer exponent.

    source
    @[simp]
    theorem IsPrimitiveRoot.zmodEquivRootsOfUnity_symm_apply_pow {R : Type u_1} [CommRing R] [IsDomain R] {k : ℕ} [NeZero k] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℕ) (hi : ζ ^ i ∈ rootsOfUnity k R) :
    h.zmodEquivRootsOfUnity.symm (Additive.ofMul ⟨ζ ^ i, hi⟩) = ↑i

    The inverse sends ζ ^ i back to the class of i, for a natural exponent.