NormResidueScalarPower.lean

1 import PaperX.NormResidueScalarWitness
2 
3 /-!
4 # Scalar power witnesses for residue-norm characters
5 
6 Scalar units in the residue algebra have determinant norm equal to the
7 `[K : ℚ]`-th power of the corresponding scalar residue.  If that power map is
8 bijective on `(ZMod m)ˣ`, every nontrivial character on scalar units therefore
9 produces the unit witness required by the norm-residue cancellation theorem.
10 -/
11 
12 set_option autoImplicit false
13 noncomputable section
14 
15 open scoped NumberField
16 
17 namespace PaperX.NormResidue
18 
19 variable (K : Type*) [Field K] [NumberField K]
20 
21 /-- A nontrivial multiplicative character on scalar units has a concrete
22 scalar witness. -/
23 theorem exists_scalar_character_witness (m : ℕ) (χ : ZMod m →*₀ ℂ)
24     (hχ : χ.toMonoidHom.comp (Units.coeHom (ZMod m)) ≠ 1) :
25     ∃ b : (ZMod m)ˣ, χ (b : ZMod m) ≠ 1 := by
26   by_contra h
27   push Not at h
28   apply hχ
29   ext b
30   simpa using h b
31 
32 /-- If the degree is coprime to the order of the scalar unit group, the degree
33 power map on scalar units is surjective.  Hence every nontrivial scalar-unit
34 character supplies an actual unit of `𝓞 K / m 𝓞 K` on which the determinant
35 norm character is nontrivial. -/
36 theorem exists_scalarResidueUnit_witness_of_card_coprime
37     (m : ℕ) (hm : m ≠ 0) (χ : ZMod m →*₀ ℂ)
38     (hχ : χ.toMonoidHom.comp (Units.coeHom (ZMod m)) ≠ 1)
39     (hdeg : (Nat.card ((ZMod m)ˣ)).Coprime (Module.finrank ℚ K)) :
40     ∃ u : (𝓞 K ⧸ modulusIdeal (𝓞 K) m)ˣ,
41       χ (integerQuotientNorm K m (u : 𝓞 K ⧸ modulusIdeal (𝓞 K) m)) ≠ 1 := by
42   let _ : NeZero m := ⟨hm⟩
43   obtain ⟨b, hb⟩ := exists_scalar_character_witness m χ hχ
44   let d : ℕ := Module.finrank ℚ K
45   let a : (ZMod m)ˣ := b ^ ((d⁻¹ : ZMod (Nat.card ((ZMod m)ˣ))).val)
46   have ha : a ^ d = b := by
47     dsimp [a, d]
48     exact pow_zmod_val_inv_pow hdeg.gcd_eq_one b
49   refine ⟨scalarResidueUnit K m hm a, ?_⟩
50   rw [integerQuotientNorm_scalarResidueUnit]
51   have ha' : (a : ZMod m) ^ Module.finrank ℚ K = (b : ZMod m) := by
52     simpa [d] using congrArg (fun u : (ZMod m)ˣ => (u : ZMod m)) ha
53   rw [ha']
54   exact hb
55 
56 end PaperX.NormResidue

Back to source controls