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 : ) [NeZero 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 : ) [NeZero 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 : ) [NeZero 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 : ) [NeZero n] (t : (rootsOfUnity n L)) :
    g t = ↑(t ^ aux g n)
    theorem modularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_pow {L : Type u} [CommRing L] [IsDomain L] (g : L ≃+* L) (p : ) [Fact (Nat.Prime p)] [∀ (i : ), HasEnoughRootsOfUnity L (p ^ i)] {i k : } (hi : k i) :
    p ^ k aux g (p ^ i) - aux g (p ^ k)
    noncomputable def modularCyclotomicCharacter.toFun {L : Type u} [CommRing L] [IsDomain L] (n : ) [NeZero 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 : } [NeZero n] (t : (rootsOfUnity n L)) :
      g t = ↑(t ^ (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 : } [NeZero n] {t : Lˣ} (ht : t rootsOfUnity n L) :
      g t = t ^ (toFun n g).val
      theorem modularCyclotomicCharacter.toFun_spec'' {L : Type u} [CommRing L] [IsDomain L] (g : L ≃+* L) {n : } [NeZero n] {t : L} (ht : IsPrimitiveRoot t n) :
      g t = t ^ (toFun n g).val
      theorem modularCyclotomicCharacter.toFun_unique {L : Type u} [CommRing L] [IsDomain L] (n : ) [NeZero n] (g : L ≃+* L) (c : ZMod (Fintype.card (rootsOfUnity n L))) (hc : ∀ (t : (rootsOfUnity n L)), g t = ↑(t ^ c.val)) :
      c = 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 : ) [NeZero n] (g : L ≃+* L) (c : ZMod (Fintype.card (rootsOfUnity n L))) (hc : trootsOfUnity n L, g t = t ^ c.val) :
      c = toFun n g
      theorem modularCyclotomicCharacter.comp {L : Type u} [CommRing L] [IsDomain L] (n : ) [NeZero n] (g h : L ≃+* L) :
      toFun n (g * h) = toFun n g * toFun n h
      noncomputable def modularCyclotomicCharacter' (L : Type u) [CommRing L] [IsDomain L] (n : ) [NeZero 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 modularCyclotomicCharacter'.spec' (L : Type u) [CommRing L] [IsDomain L] (n : ) [NeZero n] (g : L ≃+* L) {t : Lˣ} (ht : t rootsOfUnity n L) :
        g t = t ^ (↑((modularCyclotomicCharacter' L n) g)).val
        theorem modularCyclotomicCharacter'.unique' (L : Type u) [CommRing L] [IsDomain L] (n : ) [NeZero 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 : } [NeZero 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 : } [NeZero 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 : } [NeZero 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 : ) [NeZero n] (R : Type u_1) [CommRing R] [Algebra R L] {μ : L} ( : IsPrimitiveRoot μ n) (g : L ≃ₐ[R] L) :
          (autToPow R ) 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.

          noncomputable def cyclotomicCharacter.toFun {L : Type u} [CommRing L] [IsDomain L] (p : ) [Fact (Nat.Prime p)] (g : L ≃+* L) :

          The underlying function of the cyclotomic character. See cyclotomicCharacter.

          Equations
          Instances For
            theorem cyclotomicCharacter.toFun_apply {L : Type u} [CommRing L] [IsDomain L] (p : ) [Fact (Nat.Prime p)] (g : L ≃+* L) [∀ (i : ), HasEnoughRootsOfUnity L (p ^ i)] :
            theorem cyclotomicCharacter.toZModPow_toFun {L : Type u} [CommRing L] [IsDomain L] (p : ) [Fact (Nat.Prime p)] (g : L ≃+* L) [∀ (i : ), HasEnoughRootsOfUnity L (p ^ i)] (n : ) :
            theorem cyclotomicCharacter.toFun_spec {L : Type u} [CommRing L] [IsDomain L] (p : ) [Fact (Nat.Prime p)] [∀ (i : ), HasEnoughRootsOfUnity L (p ^ i)] (g : L ≃+* L) {n : } (t : (rootsOfUnity (p ^ n) L)) :
            g t = t ^ ((PadicInt.toZModPow n) (toFun p g)).val
            noncomputable def cyclotomicCharacter (L : Type u) [CommRing L] [IsDomain L] (p : ) [Fact (Nat.Prime p)] :

            Suppose L is a domain containing all pⁱ-th primitive roots with p a (rational) prime. If g is a ring automorphism of L, then cyclotomicCharacter L p g is the unique j : ℤₚ such that g(ζ) = ζ ^ (j mod pⁱ) for all pⁱ'th roots of unity ζ.

            Note: This is the trivial character when L does not contain all pⁱ-th primitive roots.

            Equations
            Instances For
              theorem cyclotomicCharacter.spec {L : Type u} [CommRing L] [IsDomain L] (p : ) [Fact (Nat.Prime p)] {n : } [∀ (i : ), HasEnoughRootsOfUnity L (p ^ i)] (g : L ≃+* L) (t : L) (ht : t ^ p ^ n = 1) :
              g t = t ^ ((PadicInt.toZModPow n) ((cyclotomicCharacter L p) g)).val
              theorem cyclotomicCharacter.toZModPow {L : Type u} [CommRing L] [IsDomain L] (p : ) [Fact (Nat.Prime p)] {n : } [∀ (i : ), HasEnoughRootsOfUnity L (p ^ i)] (g : L ≃+* L) :
              @[deprecated modularCyclotomicCharacter.aux (since := "2025-05-02")]
              def ModularCyclotomicCharacter.aux {L : Type u} [CommRing L] [IsDomain L] (g : L ≃+* L) (n : ) [NeZero n] :

              Alias of modularCyclotomicCharacter.aux.


              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
                @[deprecated modularCyclotomicCharacter.aux_spec (since := "2025-05-02")]
                theorem ModularCyclotomicCharacter.aux_spec {L : Type u} [CommRing L] [IsDomain L] (g : L ≃+* L) (n : ) [NeZero n] (t : (rootsOfUnity n L)) :
                g t = ↑(t ^ modularCyclotomicCharacter.aux g n)

                Alias of modularCyclotomicCharacter.aux_spec.

                @[deprecated modularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_pow (since := "2025-05-02")]
                theorem ModularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_pow {L : Type u} [CommRing L] [IsDomain L] (g : L ≃+* L) (p : ) [Fact (Nat.Prime p)] [∀ (i : ), HasEnoughRootsOfUnity L (p ^ i)] {i k : } (hi : k i) :

                Alias of modularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_pow.

                @[deprecated modularCyclotomicCharacter.toFun (since := "2025-05-02")]

                Alias of modularCyclotomicCharacter.toFun.


                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
                  @[deprecated modularCyclotomicCharacter.toFun_spec (since := "2025-05-02")]
                  theorem ModularCyclotomicCharacter.toFun_spec {L : Type u} [CommRing L] [IsDomain L] (g : L ≃+* L) {n : } [NeZero n] (t : (rootsOfUnity n L)) :
                  g t = ↑(t ^ (modularCyclotomicCharacter.toFun n g).val)

                  Alias of modularCyclotomicCharacter.toFun_spec.


                  The formula which characterises the output of modularCyclotomicCharacter g n.

                  @[deprecated modularCyclotomicCharacter.toFun_spec' (since := "2025-05-02")]
                  theorem ModularCyclotomicCharacter.toFun_spec' {L : Type u} [CommRing L] [IsDomain L] (g : L ≃+* L) {n : } [NeZero n] {t : Lˣ} (ht : t rootsOfUnity n L) :

                  Alias of modularCyclotomicCharacter.toFun_spec'.

                  @[deprecated modularCyclotomicCharacter.toFun_spec'' (since := "2025-05-02")]
                  theorem ModularCyclotomicCharacter.toFun_spec'' {L : Type u} [CommRing L] [IsDomain L] (g : L ≃+* L) {n : } [NeZero n] {t : L} (ht : IsPrimitiveRoot t n) :

                  Alias of modularCyclotomicCharacter.toFun_spec''.

                  @[deprecated modularCyclotomicCharacter.toFun_unique (since := "2025-05-02")]
                  theorem ModularCyclotomicCharacter.toFun_unique {L : Type u} [CommRing L] [IsDomain L] (n : ) [NeZero n] (g : L ≃+* L) (c : ZMod (Fintype.card (rootsOfUnity n L))) (hc : ∀ (t : (rootsOfUnity n L)), g t = ↑(t ^ c.val)) :

                  Alias of modularCyclotomicCharacter.toFun_unique.


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

                  @[deprecated modularCyclotomicCharacter.toFun_unique' (since := "2025-05-02")]
                  theorem ModularCyclotomicCharacter.toFun_unique' {L : Type u} [CommRing L] [IsDomain L] (n : ) [NeZero n] (g : L ≃+* L) (c : ZMod (Fintype.card (rootsOfUnity n L))) (hc : trootsOfUnity n L, g t = t ^ c.val) :

                  Alias of modularCyclotomicCharacter.toFun_unique'.

                  @[deprecated modularCyclotomicCharacter.id (since := "2025-05-02")]

                  Alias of modularCyclotomicCharacter.id.

                  @[deprecated modularCyclotomicCharacter.comp (since := "2025-05-02")]

                  Alias of modularCyclotomicCharacter.comp.

                  @[deprecated modularCyclotomicCharacter' (since := "2025-05-02")]

                  Alias of modularCyclotomicCharacter'.


                  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
                    @[deprecated modularCyclotomicCharacter'.spec' (since := "2025-05-02")]
                    theorem ModularCyclotomicCharacter'.spec' (L : Type u) [CommRing L] [IsDomain L] (n : ) [NeZero n] (g : L ≃+* L) {t : Lˣ} (ht : t rootsOfUnity n L) :
                    g t = t ^ (↑((modularCyclotomicCharacter' L n) g)).val

                    Alias of modularCyclotomicCharacter'.spec'.

                    @[deprecated modularCyclotomicCharacter'.unique' (since := "2025-05-02")]
                    theorem ModularCyclotomicCharacter'.unique' (L : Type u) [CommRing L] [IsDomain L] (n : ) [NeZero n] (g : L ≃+* L) {c : ZMod (Fintype.card (rootsOfUnity n L))} (hc : trootsOfUnity n L, g t = t ^ c.val) :

                    Alias of modularCyclotomicCharacter'.unique'.

                    @[deprecated modularCyclotomicCharacter (since := "2025-05-02")]
                    def ModularCyclotomicCharacter (L : Type u) [CommRing L] [IsDomain L] {n : } [NeZero n] (hn : Fintype.card (rootsOfUnity n L) = n) :
                    (L ≃+* L) →* (ZMod n)ˣ

                    Alias of modularCyclotomicCharacter.


                    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
                      @[deprecated modularCyclotomicCharacter.spec (since := "2025-05-02")]
                      theorem ModularCyclotomicCharacter.spec (L : Type u) [CommRing L] [IsDomain L] {n : } [NeZero 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

                      Alias of modularCyclotomicCharacter.spec.

                      @[deprecated modularCyclotomicCharacter.unique (since := "2025-05-02")]
                      theorem ModularCyclotomicCharacter.unique (L : Type u) [CommRing L] [IsDomain L] {n : } [NeZero n] (hn : Fintype.card (rootsOfUnity n L) = n) (g : L ≃+* L) {c : ZMod n} (hc : trootsOfUnity n L, g t = t ^ c.val) :

                      Alias of modularCyclotomicCharacter.unique.

                      @[deprecated IsPrimitiveRoot.autToPow_eq_modularCyclotomicCharacter (since := "2025-05-02")]
                      theorem IsPrimitiveRoot.autToPow_eq_ModularCyclotomicCharacter {L : Type u} [CommRing L] [IsDomain L] (n : ) [NeZero n] (R : Type u_1) [CommRing R] [Algebra R L] {μ : L} ( : IsPrimitiveRoot μ n) (g : L ≃ₐ[R] L) :
                      (autToPow R ) g = (modularCyclotomicCharacter L ) g

                      Alias of IsPrimitiveRoot.autToPow_eq_modularCyclotomicCharacter.


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

                      @[deprecated cyclotomicCharacter.toFun (since := "2025-05-02")]
                      def CyclotomicCharacter.toFun {L : Type u} [CommRing L] [IsDomain L] (p : ) [Fact (Nat.Prime p)] (g : L ≃+* L) :

                      Alias of cyclotomicCharacter.toFun.


                      The underlying function of the cyclotomic character. See cyclotomicCharacter.

                      Equations
                      Instances For
                        @[deprecated cyclotomicCharacter.toFun_apply (since := "2025-05-02")]

                        Alias of cyclotomicCharacter.toFun_apply.

                        @[deprecated cyclotomicCharacter.toZModPow_toFun (since := "2025-05-02")]

                        Alias of cyclotomicCharacter.toZModPow_toFun.

                        @[deprecated cyclotomicCharacter.toFun_spec (since := "2025-05-02")]
                        theorem CyclotomicCharacter.toFun_spec {L : Type u} [CommRing L] [IsDomain L] (p : ) [Fact (Nat.Prime p)] [∀ (i : ), HasEnoughRootsOfUnity L (p ^ i)] (g : L ≃+* L) {n : } (t : (rootsOfUnity (p ^ n) L)) :
                        g t = t ^ ((PadicInt.toZModPow n) (cyclotomicCharacter.toFun p g)).val

                        Alias of cyclotomicCharacter.toFun_spec.

                        @[deprecated cyclotomicCharacter (since := "2025-05-02")]
                        def CyclotomicCharacter (L : Type u) [CommRing L] [IsDomain L] (p : ) [Fact (Nat.Prime p)] :

                        Alias of cyclotomicCharacter.


                        Suppose L is a domain containing all pⁱ-th primitive roots with p a (rational) prime. If g is a ring automorphism of L, then cyclotomicCharacter L p g is the unique j : ℤₚ such that g(ζ) = ζ ^ (j mod pⁱ) for all pⁱ'th roots of unity ζ.

                        Note: This is the trivial character when L does not contain all pⁱ-th primitive roots.

                        Equations
                        Instances For
                          @[deprecated cyclotomicCharacter.spec (since := "2025-05-02")]
                          theorem CyclotomicCharacter.spec {L : Type u} [CommRing L] [IsDomain L] (p : ) [Fact (Nat.Prime p)] {n : } [∀ (i : ), HasEnoughRootsOfUnity L (p ^ i)] (g : L ≃+* L) (t : L) (ht : t ^ p ^ n = 1) :
                          g t = t ^ ((PadicInt.toZModPow n) ((cyclotomicCharacter L p) g)).val

                          Alias of cyclotomicCharacter.spec.

                          @[deprecated cyclotomicCharacter.toZModPow (since := "2025-05-02")]
                          theorem CyclotomicCharacter.toZModPow {L : Type u} [CommRing L] [IsDomain L] (p : ) [Fact (Nat.Prime p)] {n : } [∀ (i : ), HasEnoughRootsOfUnity L (p ^ i)] (g : L ≃+* L) :

                          Alias of cyclotomicCharacter.toZModPow.

                          @[deprecated cyclotomicCharacter.continuous (since := "2025-05-02")]

                          Alias of cyclotomicCharacter.continuous.