English
For a fixed n and domain L, there is a multiplicative homomorphism χ₀ n from the automorphism group of L to (Z/nZ)ˣ characterized by g(ζ) = ζ^{χ₀(n,g)} for every n-th root of unity ζ.
Русский
Для данного n и области L существует мультипликативный гомоморфизм χ₀ n: Aut(L) → (Z/nZ)ˣ, такой что g(ζ)=ζ^{χ₀(n,g)} для каждого ζ — n-й корень единства.
LaTeX
$$$\\chi_{0}:\\mathrm{Aut}(L) \\to (\\mathbb{Z}/n\\mathbb{Z})^{\\times},\\; g(\\zeta)=\\zeta^{\\chi_{0}(n,g)}\\;\\text{для всех }\\zeta\\in \\mathrm{rootsOfUnity}_n(L)$$$
Lean4
/-- 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. -/
noncomputable def modularCyclotomicCharacter {n : ℕ} [NeZero n] (hn : Fintype.card { x // x ∈ rootsOfUnity n L } = n) :
(L ≃+* L) →* (ZMod n)ˣ :=
(Units.mapEquiv <| (ZMod.ringEquivCongr hn).toMulEquiv).toMonoidHom.comp (modularCyclotomicCharacter' L n)
