cyclotomicCharacter — Mathlib

English

For t ∈ rootsOfUnity, the equality holds for g restricted to units: g t = t^{χ' (n,g)}.

Русский

Для t ∈ rootsOfUnity верно g t = t^{χ' (n,g)}.

LaTeX

$$$g t = t^{ (\\,modularCyclotomicCharacter' L n g) : ZMod (...) }.val$$$

Lean4

/-- 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.
-/
noncomputable def cyclotomicCharacter (p : ℕ) [Fact p.Prime] : (L ≃+* L) →* ℤ_[p]ˣ :=
  .toHomUnits
    { toFun g := cyclotomicCharacter.toFun p g
      map_one' := by
        by_cases H : ∀ (i : ℕ), ∃ ζ : L, IsPrimitiveRoot ζ (p ^ i)
        · haveI _ (i) : HasEnoughRootsOfUnity L (p ^ i) := ⟨H i, rootsOfUnity.isCyclic _ _⟩
          refine PadicInt.ext_of_toZModPow.mp fun n ↦ ?_
          simp [cyclotomicCharacter.toZModPow_toFun]
        · simp [cyclotomicCharacter.toFun, dif_neg H]
      map_mul' f
        g := by
        by_cases H : ∀ (i : ℕ), ∃ ζ : L, IsPrimitiveRoot ζ (p ^ i)
        · haveI _ (i) : HasEnoughRootsOfUnity L (p ^ i) := ⟨H i, rootsOfUnity.isCyclic _ _⟩
          refine PadicInt.ext_of_toZModPow.mp fun n ↦ ?_
          simp [cyclotomicCharacter.toZModPow_toFun]
        · simp [cyclotomicCharacter.toFun, dif_neg H] }

Похожие утверждения