The cyclotomic character

Let L be an integral domain and let n : ℕ+ be a positive integer. If μₙ is the group of nth roots of unity in L then any field automorphism g of L induces an automorphism of μₙ which, being a cyclic group, must be of the form ζ ↦ ζ^j for some integer j = j(g), well-defined in ZMod d, with d the cardinality of μₙ. The function j is a group homomorphism (L ≃+* L) →* ZMod d.

Future work: If L is separably closed (e.g. algebraically closed) and p is a prime number such that p ≠ 0 in L, then applying the above construction with n = p^i (noting that the size of μₙ is p^i) gives a compatible collection of group homomorphisms (L ≃+* L) →* ZMod (p^i) which glue to give a group homomorphism (L ≃+* L) →* ℤₚ; this is the p-adic cyclotomic character.

Important definitions

Let L be an integral domain, g : L ≃+* L and n : ℕ+. Let d be the number of nth roots of 1 in L.

• ModularCyclotomicCharacter L n hn : (L ≃+* L) →* (ZMod n)ˣ sends g to the unique j such that g(ζ)=ζ^j for all ζ : rootsOfUnity n L. Here hn is a proof that there are n nth roots of unity in L.

Implementation note

In theory this could be set up as some theory about monoids, being a character on monoid isomorphisms, but under the hypotheses that the n'th roots of unity are cyclic. The advantage of sticking to integral domains is that finite subgroups are guaranteed to be cyclic, so the weaker assumption that there are n nth roots of unity is enough. All the applications I'm aware of are when L is a field anyway.

Although I don't know whether it's of any use, ModularCyclotomicCharacter' is the general case for integral domains, with target in (ZMod d)ˣ where d is the number of nth roots of unity in L.

Todo

• Prove the compatibility of ModularCyclotomicCharacter n and ModularCyclotomicCharacter m if n ∣ m.

• Define the cyclotomic character.

• Prove that it's continuous.

Tags

cyclotomic character

theorem rootsOfUnity.integer_power_of_ringEquiv {L : Type u} [CommRing L] [IsDomain L] (n : ℕ+) (g : L ≃+* L) : ∃ (m : ℤ), ∀ (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ m)

theorem rootsOfUnity.integer_power_of_ringEquiv' {L : Type u} [CommRing L] [IsDomain L] (n : ℕ+) (g : L ≃+* L) : ∃ (m : ℤ), ∀ t ∈ rootsOfUnity n L, g ↑t = ↑(t ^ m)

noncomputable def ModularCyclotomicCharacter_aux {L : Type u} [CommRing L] [IsDomain L] (g : L ≃+* L) (n : ℕ+) : ℤ

ModularCyclotomicCharacter_aux g n is a non-canonical auxiliary integer j, only well-defined modulo the number of n'th roots of unity in L, such that g(ζ)=ζ^j for all n'th roots of unity ζ in L.

Equations

• ModularCyclotomicCharacter_aux g n = Exists.choose ⋯

theorem ModularCyclotomicCharacter_aux_spec {L : Type u} [CommRing L] [IsDomain L] (g : L ≃+* L) (n : ℕ+) (t : ↥(rootsOfUnity n L)) : g ↑↑t = ↑(↑t ^ ModularCyclotomicCharacter_aux g n)

noncomputable def ModularCyclotomicCharacter.toFun {L : Type u} [CommRing L] [IsDomain L] (n : ℕ+) (g : L ≃+* L) : ZMod (Fintype.card ↥(rootsOfUnity n L))

If g is a ring automorphism of L, and n : ℕ+, then ModularCyclotomicCharacter.toFun n g is the j : ZMod d such that g(ζ)=ζ^j for all n'th roots of unity. Here d is the number of nth roots of unity in L.

Equations

• ModularCyclotomicCharacter.toFun n g = ↑(ModularCyclotomicCharacter_aux g n)

theorem ModularCyclotomicCharacter.toFun_spec {L : Type u} [CommRing L] [IsDomain L] (g : L ≃+* L) {n : ℕ+} (t : ↥(rootsOfUnity n L)) : g ↑↑t = ↑(↑t ^ ZMod.val (ModularCyclotomicCharacter.toFun n g))

The formula which characterises the output of ModularCyclotomicCharacter g n.

theorem ModularCyclotomicCharacter.toFun_spec' {L : Type u} [CommRing L] [IsDomain L] (g : L ≃+* L) {n : ℕ+} {t : Lˣ} (ht : t ∈ rootsOfUnity n L) : g ↑t = ↑t ^ ZMod.val (ModularCyclotomicCharacter.toFun n g)

theorem ModularCyclotomicCharacter.toFun_spec'' {L : Type u} [CommRing L] [IsDomain L] (g : L ≃+* L) {n : ℕ+} {t : L} (ht : IsPrimitiveRoot t ↑n) : g t = t ^ ZMod.val (ModularCyclotomicCharacter.toFun n g)

theorem ModularCyclotomicCharacter.toFun_unique {L : Type u} [CommRing L] [IsDomain L] (n : ℕ+) (g : L ≃+* L) (c : ZMod (Fintype.card ↥(rootsOfUnity n L))) (hc : ∀ (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ ZMod.val c)) : c = ModularCyclotomicCharacter.toFun n g

If g(t)=t^c for all roots of unity, then c=χ(g).

theorem ModularCyclotomicCharacter.toFun_unique' {L : Type u} [CommRing L] [IsDomain L] (n : ℕ+) (g : L ≃+* L) (c : ZMod (Fintype.card ↥(rootsOfUnity n L))) (hc : ∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ ZMod.val c) : c = ModularCyclotomicCharacter.toFun n g

theorem ModularCyclotomicCharacter.id {L : Type u} [CommRing L] [IsDomain L] (n : ℕ+) : ModularCyclotomicCharacter.toFun n (RingEquiv.refl L) = 1

theorem ModularCyclotomicCharacter.comp {L : Type u} [CommRing L] [IsDomain L] (n : ℕ+) (g : L ≃+* L) (h : L ≃+* L) : ModularCyclotomicCharacter.toFun n (g * h) = ModularCyclotomicCharacter.toFun n g * ModularCyclotomicCharacter.toFun n h

noncomputable def ModularCyclotomicCharacter' (L : Type u) [CommRing L] [IsDomain L] (n : ℕ+) : (L ≃+* L) →* (ZMod (Fintype.card ↥(rootsOfUnity n L)))ˣ

Given a positive integer n, ModularCyclotomicCharacter' n is a multiplicative homomorphism from the automorphisms of a field L to (ℤ/dℤ)ˣ, where d is the number of n'th roots of unity in L. It is uniquely characterised by the property that g(ζ)=ζ^(ModularCyclotomicCharacter n g) for g an automorphism of L and ζ an nth root of unity.

Equations

• ModularCyclotomicCharacter' L n = MonoidHom.toHomUnits { toOneHom := { toFun := ModularCyclotomicCharacter.toFun n, map_one' := ⋯ }, map_mul' := ⋯ }

theorem spec' (L : Type u) [CommRing L] [IsDomain L] (n : ℕ+) (g : L ≃+* L) {t : Lˣ} (ht : t ∈ rootsOfUnity n L) : g ↑t = ↑t ^ ZMod.val ↑((ModularCyclotomicCharacter' L n) g)

theorem unique' (L : Type u) [CommRing L] [IsDomain L] (n : ℕ+) (g : L ≃+* L) {c : ZMod (Fintype.card ↥(rootsOfUnity n L))} (hc : ∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ ZMod.val c) : c = ↑((ModularCyclotomicCharacter' L n) g)

noncomputable def ModularCyclotomicCharacter (L : Type u) [CommRing L] [IsDomain L] {n : ℕ+} (hn : Fintype.card ↥(rootsOfUnity n L) = ↑n) : (L ≃+* L) →* (ZMod ↑n)ˣ

Given a positive integer n and a field L containing n nth roots of unity, ModularCyclotomicCharacter n is a multiplicative homomorphism from the automorphisms of L to (ℤ/nℤ)ˣ. It is uniquely characterised by the property that g(ζ)=ζ^(ModularCyclotomicCharacter n g) for g an automorphism of L and ζ any nth root of unity.

Equations

• ModularCyclotomicCharacter L hn = MonoidHom.comp (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (ZMod.ringEquivCongr hn)))) (ModularCyclotomicCharacter' L n)

theorem ModularCyclotomicCharacter.spec (L : Type u) [CommRing L] [IsDomain L] {n : ℕ+} (hn : Fintype.card ↥(rootsOfUnity n L) = ↑n) (g : L ≃+* L) {t : Lˣ} (ht : t ∈ rootsOfUnity n L) : g ↑t = ↑t ^ ZMod.val ↑((ModularCyclotomicCharacter L hn) g)

theorem ModularCyclotomicCharacter.unique (L : Type u) [CommRing L] [IsDomain L] {n : ℕ+} (hn : Fintype.card ↥(rootsOfUnity n L) = ↑n) (g : L ≃+* L) {c : ZMod ↑n} (hc : ∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ ZMod.val c) : c = ↑((ModularCyclotomicCharacter L hn) g)

theorem IsPrimitiveRoot.autToPow_eq_ModularCyclotomicCharacter {L : Type u} [CommRing L] [IsDomain L] (n : ℕ+) (R : Type u_1) [CommRing R] [Algebra R L] {μ : L} (hμ : IsPrimitiveRoot μ ↑n) (g : L ≃ₐ[R] L) : (IsPrimitiveRoot.autToPow R hμ) g = (ModularCyclotomicCharacter L ⋯) ↑g

The relationship between IsPrimitiveRoot.autToPow and ModularCyclotomicCharacter. Note that IsPrimitiveRoot.autToPow needs an explicit root of unity, and also an auxiliary "base ring" R.