A seed Galois realization contains a full-order character value

Proved

HorizontalPadicL.SeedCyclotomicGaloisCharacterData.exists_fullOrder_value

by davidloeffler · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

dirichlet-charactersgalois-representationsnumber-theory

The seed/cyclotomic Galois realization contains a unit residue class $a$ such that the order of $\eta(a)$ is the order of the seed Dirichlet character $\eta$ .

Retired. This helper uses the retired Galois package. Use HorizontalPadicL.SeedCyclotomicGaloisCharacterDataV2.exists_fullOrder_value.

Preamble

import Definitions.Def_KN_SeedCyclotomicGaloisCharacters

set_option autoImplicit false
noncomputable section

namespace HorizontalPadicL

Formal statement

/-- A seed/cyclotomic Galois realization supplies a residue class on which
the seed Dirichlet character has its full order. -/
theorem SeedCyclotomicGaloisCharacterData.exists_fullOrder_value
    {N p m : ℕ} [Fact p.Prime]
    (η : DirichletCharacterWithLevel)
    (C : SeedCyclotomicGaloisCharacterData N p m η) :
    ∃ a : (ZMod η.1.1)ˣ,
      orderOf (η.2 (a : ZMod η.1.1)) = orderOf η.2 := by sorry

end HorizontalPadicL

Source

Immediate from the full-order seed generator and the assertion that every Galois-character value is a value of the Dirichlet character.

View graph