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)ˣsendsgto the uniquejsuch thatg(ζ)=ζ^jfor allζ : rootsOfUnity n L. Herehnis a proof that there arennth roots of unity inL.cyclotomicCharacter L p : (L ≃+* L) →* ℤ_[p]ˣsendsgto the uniquejsuch thatg(ζ) = ζ ^ (j mod pⁱ)for allpⁱ-th roots of unityζ.Note: This is defined to be the trivial character if
Lhas no enough roots of unity.
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 nandmodularCyclotomicCharacter mifn ∣ m.
Tags #
cyclotomic character
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
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
The formula which characterises the output of modularCyclotomicCharacter g n.
If g(t)=t^c for all roots of unity, then c=χ(g).
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 = { toFun := modularCyclotomicCharacter.toFun n, map_one' := ⋯, map_mul' := ⋯ }.toHomUnits
Instances For
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
The relationship between IsPrimitiveRoot.autToPow and
modularCyclotomicCharacter. Note that IsPrimitiveRoot.autToPow
needs an explicit root of unity, and also an auxiliary "base ring" R.
The underlying function of the cyclotomic character. See cyclotomicCharacter.
Equations
- cyclotomicCharacter.toFun p g = if H : ∀ (i : ℕ), ∃ (ζ : L), IsPrimitiveRoot ζ (p ^ i) then PadicInt.ofIntSeq (fun (x : ℕ) => modularCyclotomicCharacter.aux g (p ^ x)) ⋯ else 1
Instances For
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
- cyclotomicCharacter L p = { toFun := fun (g : L ≃+* L) => cyclotomicCharacter.toFun p g, map_one' := ⋯, map_mul' := ⋯ }.toHomUnits
Instances For
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.
Instances For
Alias of modularCyclotomicCharacter.aux_spec.
Alias of modularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_pow.
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.
Instances For
Alias of modularCyclotomicCharacter.toFun_spec.
The formula which characterises the output of modularCyclotomicCharacter g n.
Alias of modularCyclotomicCharacter.toFun_spec'.
Alias of modularCyclotomicCharacter.toFun_spec''.
Alias of modularCyclotomicCharacter.toFun_unique.
If g(t)=t^c for all roots of unity, then c=χ(g).
Alias of modularCyclotomicCharacter.toFun_unique'.
Alias of modularCyclotomicCharacter.id.
Alias of modularCyclotomicCharacter.comp.
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.
Instances For
Alias of modularCyclotomicCharacter'.spec'.
Alias of modularCyclotomicCharacter'.unique'.
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.
Instances For
Alias of modularCyclotomicCharacter.spec.
Alias of modularCyclotomicCharacter.unique.
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.
Alias of cyclotomicCharacter.toFun.
The underlying function of the cyclotomic character. See cyclotomicCharacter.
Equations
Instances For
Alias of cyclotomicCharacter.toFun_apply.
Alias of cyclotomicCharacter.toZModPow_toFun.
Alias of cyclotomicCharacter.toFun_spec.
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
Alias of cyclotomicCharacter.toZModPow.
Alias of cyclotomicCharacter.continuous.