NormResidueScalarObstruction.lean

1 import PaperX.NormResidueExactScalarCriterion
2 import Mathlib.Algebra.Group.Hom.Instances
3 
4 /-!
5 # Exact obstruction for scalar norm witnesses
6 
7 The scalar witness exists exactly when the restriction of the residue character
8 to scalar units does not become trivial after raising character values to the
9 field degree.  This identifies the precise exceptional scalar-character case;
10 degree--totient coprimality is only one sufficient way to rule it out.
11 -/
12 
13 set_option autoImplicit false
14 noncomputable section
15 
16 open scoped NumberField
17 
18 namespace PaperX.NormResidue
19 
20 variable (K : Type*) [Field K] [NumberField K]
21 
22 /-- The scalar norm-witness condition is equivalent to nontriviality of the
23 field-degree power of the restricted multiplicative character. -/
24 theorem scalar_power_witness_iff_restricted_pow_ne_one
25     (m : ℕ) (χ : ZMod m →*₀ ℂ) :
26     (∃ a : (ZMod m)ˣ,
27       χ ((a : ZMod m) ^ Module.finrank ℚ K) ≠ 1) ↔
28     (χ.toMonoidHom.comp (Units.coeHom (ZMod m))) ^ Module.finrank ℚ K ≠ 1 := by
29   let ψ : (ZMod m)ˣ →* ℂ := χ.toMonoidHom.comp (Units.coeHom (ZMod m))
30   constructor
31   · rintro ⟨a, ha⟩ htriv
32     apply ha
33     have h := DFunLike.congr_fun htriv a
34     simpa [ψ, MonoidHom.pow_apply] using h
35   · intro hnon
36     by_contra hnone
37     push Not at hnone
38     apply hnon
39     ext a
40     simpa [ψ, MonoidHom.pow_apply] using hnone a
41 
42 end PaperX.NormResidue

Back to source controls