The cyclotomic character #
Let L
be an integral domain and let n : ℕ+
be a positive integer. If μₙ
is the
group of n
th 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 n
th roots
of 1
in L
.
modularCyclotomicCharacter L n hn : (L ≃+* L) →* (ZMod n)ˣ
sendsg
to the uniquej
such thatg(ζ)=ζ^j
for allζ : rootsOfUnity n L
. Herehn
is a proof that there aren
n
th roots of unity inL
.cyclotomicCharacter L p : (L ≃+* L) →* ℤ_[p]ˣ
sendsg
to the uniquej
such thatg(ζ) = ζ ^ (j mod pⁱ)
for allpⁱ
'th roots of unityζ
.Note: This is defined to be the trivial character if
L
has 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
n
th
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 n
th roots of unity in L
.
TODO #
- Prove the compatibility of
modularCyclotomicCharacter n
andmodularCyclotomicCharacter m
ifn ∣ 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 n
th 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 n
th 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
n
th 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 n
th 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 n
th 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 n
th 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
n
th 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 n
th 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
.