A faithful seed Galois realization contains a full-order character value
ProvedHorizontalPadicL.SeedCyclotomicGaloisCharacterDataV2.exists_fullOrder_valuecyclotomic-fieldsdirichlet-charactersgalois-representationsnumber-theory
A faithful seed/cyclotomic Galois realization contains a unit residue class a such that eta(a) has the full order of eta.
Preamble
import Definitions.Def_KN_SeedCyclotomicGaloisCharactersV2 set_option autoImplicit false noncomputable section
Formal statement
namespace HorizontalPadicL
/-- A faithful seed/cyclotomic Galois realization supplies a residue class on
which the seed Dirichlet character has its full order. -/
theorem SeedCyclotomicGaloisCharacterDataV2.exists_fullOrder_value
{N p m : ℕ} [Fact p.Prime]
(η : DirichletCharacterWithLevel)
(C : SeedCyclotomicGaloisCharacterDataV2 N p m η) :
∃ a : (ZMod η.1.1)ˣ,
orderOf (η.2 (a : ZMod η.1.1)) = orderOf η.2 := by sorry
end HorizontalPadicLSource
Immediate from the distinguished full-order seed generator and the exact description of the seed-character image.