English
Given a primitive root μ of order n and an algebra hom g, the evaluation of g on μ matches the power μ^{(modular cyclotomic character)} via a canonical isomorphism.
Русский
Пусть имеется примитивный корень μ порядка n и алгебраический гомоморфизм g; значение g(μ) равно μ^{χ'(g)} через каноническое изоморфирование.
LaTeX
$$$g(\\mu) = \\mu^{(\\text{modularCyclotomicCharacter}'(L,n,g))}$ для соответствующего нормирования$$
Lean4
/-- 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. -/
noncomputable def modularCyclotomicCharacter' (n : ℕ) [NeZero n] :
(L ≃+* L) →* (ZMod (Fintype.card { x // x ∈ rootsOfUnity n L }))ˣ :=
MonoidHom.toHomUnits
{ toFun := modularCyclotomicCharacter.toFun n
map_one' := modularCyclotomicCharacter.id n
map_mul' := modularCyclotomicCharacter.comp n }
