Documentation

Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

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.

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 #

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 : ), trootsOfUnity 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
Instances For
    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) :

    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
    Instances For
      theorem ModularCyclotomicCharacter.toFun_spec {L : Type u} [CommRing L] [IsDomain L] (g : L ≃+* L) {n : ℕ+} (t : (rootsOfUnity n L)) :
      g t = (t ^ (ModularCyclotomicCharacter.toFun n g).val)

      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 ^ (ModularCyclotomicCharacter.toFun n g).val
      theorem ModularCyclotomicCharacter.toFun_spec'' {L : Type u} [CommRing L] [IsDomain L] (g : L ≃+* L) {n : ℕ+} {t : L} (ht : IsPrimitiveRoot t n) :
      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 ^ c.val)) :

      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 : trootsOfUnity n L, g t = t ^ c.val) :
      noncomputable def ModularCyclotomicCharacter' (L : Type u) [CommRing L] [IsDomain L] (n : ℕ+) :

      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
      Instances For
        theorem spec' (L : Type u) [CommRing L] [IsDomain L] (n : ℕ+) (g : L ≃+* L) {t : Lˣ} (ht : t rootsOfUnity n L) :
        g t = t ^ (((ModularCyclotomicCharacter' L n) g)).val
        theorem unique' (L : Type u) [CommRing L] [IsDomain L] (n : ℕ+) (g : L ≃+* L) {c : ZMod (Fintype.card (rootsOfUnity n L))} (hc : trootsOfUnity n L, g t = t ^ c.val) :
        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
        Instances For
          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 ^ (((ModularCyclotomicCharacter L hn) g)).val
          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 : trootsOfUnity n L, g t = t ^ c.val) :
          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) :

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