ScalarWitnessAttempt.lean

1 import PaperX.NormResidueCharacter
2 import Mathlib.Data.ZMod.Units
3 import Mathlib.GroupTheory.OrderOfElement
4 
5 set_option autoImplicit false
6 noncomputable section
7 open scoped NumberField
8 namespace PaperX.NormResidue
9 
10 variable (K : Type*) [Field K] [NumberField K]
11 
12 theorem integerQuotient_mk_nat_eq_of_zmod_eq (m a b : ℕ)
13     (h : (a : ZMod m) = (b : ZMod m)) :
14     Ideal.Quotient.mk (modulusIdeal (𝓞 K) m) (a : 𝓞 K) =
15       Ideal.Quotient.mk (modulusIdeal (𝓞 K) m) (b : 𝓞 K) := by
16   apply (Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _).2
17   change (a : 𝓞 K) - (b : 𝓞 K) ∈ Ideal.span {(m : 𝓞 K)}
18   rw [Ideal.mem_span_singleton]
19   have hz : (m : ℤ) ∣ (a : ℤ) - (b : ℤ) :=
20     (ZMod.natCast_eq_natCast_iff a b m).mp h |>.symm.dvd
21   rcases hz with ⟨z, hz⟩
22   refine ⟨(z : 𝓞 K), ?_⟩
23   exact_mod_cast hz
24 
25 theorem integerQuotientNorm_natCast (m a : ℕ) :
26     integerQuotientNorm K m
27       (Ideal.Quotient.mk (modulusIdeal (𝓞 K) m) (a : 𝓞 K)) =
28       (a : ZMod m) ^ Module.finrank ℚ K := by
29   rw [integerQuotientNorm_mk, Algebra.norm_natCast]
30   simp [NumberField.RingOfIntegers.rank]
31 
32 noncomputable def scalarResidueUnit (m : ℕ) (hm : m ≠ 0) (a : (ZMod m)ˣ) :
33     (𝓞 K ⧸ modulusIdeal (𝓞 K) m)ˣ := by
34   let _ : NeZero m := ⟨hm⟩
35   let av : ℕ := (a : ZMod m).val
36   let bv : ℕ := a.inv.val
37   refine ⟨Ideal.Quotient.mk (modulusIdeal (𝓞 K) m) (av : 𝓞 K),
38     Ideal.Quotient.mk (modulusIdeal (𝓞 K) m) (bv : 𝓞 K), ?_, ?_⟩
39   · have hz : ((av * bv : ℕ) : ZMod m) = (1 : ZMod m) := by
40       dsimp [av, bv]
41       rw [Nat.cast_mul, ZMod.natCast_zmod_val, ZMod.natCast_zmod_val]
42       exact a.val_inv
43     simpa only [map_mul, Nat.cast_mul, map_one, Nat.cast_one] using
44       integerQuotient_mk_nat_eq_of_zmod_eq K m (av * bv) 1 (by simpa using hz)
45   · have hz : ((bv * av : ℕ) : ZMod m) = (1 : ZMod m) := by
46       dsimp [av, bv]
47       rw [Nat.cast_mul, ZMod.natCast_zmod_val, ZMod.natCast_zmod_val]
48       exact a.inv_val
49     simpa only [map_mul, Nat.cast_mul, map_one, Nat.cast_one] using
50       integerQuotient_mk_nat_eq_of_zmod_eq K m (bv * av) 1 (by simpa using hz)
51 
52 theorem integerQuotientNorm_scalarResidueUnit (m : ℕ) (hm : m ≠ 0)
53     (a : (ZMod m)ˣ) :
54     integerQuotientNorm K m
55       (scalarResidueUnit K m hm a : 𝓞 K ⧸ modulusIdeal (𝓞 K) m) =
56       (a : ZMod m) ^ Module.finrank ℚ K := by
57   let _ : NeZero m := ⟨hm⟩
58   change integerQuotientNorm K m
59       (Ideal.Quotient.mk (modulusIdeal (𝓞 K) m) ((a : ZMod m).val : 𝓞 K)) = _
60   rw [integerQuotientNorm_natCast]
61   rw [ZMod.natCast_zmod_val]
62 
63 end PaperX.NormResidue
64 
65 namespace PaperX.NormResidue
66 
67 variable (K : Type*) [Field K] [NumberField K]
68 
69 theorem exists_scalarResidueUnit_witness_of_restricted_nontrivial
70     (m : ℕ) (hm : m ≠ 0) (χ : ZMod m →*₀ ℂ)
71     (hχ : χ.toMonoidHom.comp (Units.coeHom (ZMod m)) ≠ 1)
72     (hdeg : (Module.finrank ℚ K).Coprime m.totient) :
73     ∃ u : (𝓞 K ⧸ modulusIdeal (𝓞 K) m)ˣ,
74       χ (integerQuotientNorm K m (u : 𝓞 K ⧸ modulusIdeal (𝓞 K) m)) ≠ 1 := by
75   let _ : NeZero m := ⟨hm⟩
76   have hbex : ∃ b : (ZMod m)ˣ, χ (b : ZMod m) ≠ 1 := by
77     by_contra h
78     push Not at h
79     apply hχ
80     ext b
81     simpa using h b
82   obtain ⟨b, hb⟩ := hbex
83   have hcard : (Nat.card ((ZMod m)ˣ)).Coprime (Module.finrank ℚ K) := by
84     rw [Nat.card_eq_fintype_card, ZMod.card_units_eq_totient]
85     exact hdeg.symm
86   obtain ⟨a, ha⟩ := (Nat.Coprime.pow_left_bijective hcard).2 b
87   refine ⟨scalarResidueUnit K m hm a, ?_⟩
88   rw [integerQuotientNorm_scalarResidueUnit]
89   have ha' : (a : ZMod m) ^ Module.finrank ℚ K = (b : ZMod m) := by
90     simpa using congrArg (fun u : (ZMod m)ˣ => (u : ZMod m)) ha
91   rw [ha']
92   exact hb
93 
94 end PaperX.NormResidue

Back to source controls