# 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)ˣ`

sends`g`

to the unique`j`

such that`g(ζ)=ζ^j`

for all`ζ : rootsOfUnity n L`

. Here`hn`

is a proof that there are`n`

`n`

th 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`

`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`

and`ModularCyclotomicCharacter m`

if`n ∣ m`

.Define the cyclotomic character.

Prove that it's continuous.

## 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

- ModularCyclotomicCharacter_aux g n = ⋯.choose

## 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

- ModularCyclotomicCharacter L hn = (Units.mapEquiv (ZMod.ringEquivCongr hn).toMulEquiv).toMonoidHom.comp (ModularCyclotomicCharacter' L n)

## 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`

.