NormResidueArithmetic.lean

1 import PaperX.NormResidueAlgebra
2 import Mathlib.NumberTheory.NumberField.Norm
3 
4 /-!
5 # Arithmetic residue norms and the sign of principal ideal norms
6 
7 The finite residue norm is attached to the ring of integers itself. Absolute
8 ideal norms agree with signed element norms only after choosing a norm sign.
9 -/
10 
11 set_option backward.isDefEq.respectTransparency.types false
12 
13 noncomputable section
14 
15 open scoped NumberField
16 
17 namespace PaperX.NormResidue
18 
19 variable (K : Type*) [Field K] [NumberField K]
20 
21 /-- The canonical norm map on the actual quotient of the ring of integers. -/
22 def integerQuotientNorm (m : ℕ) :
23     𝓞 K ⧸ modulusIdeal (𝓞 K) m →* ZMod m :=
24   quotientNorm (Module.Free.chooseBasis ℤ (𝓞 K)) m
25 
26 theorem integerQuotientNorm_mk (m : ℕ) (x : 𝓞 K) :
27     integerQuotientNorm K m (Ideal.Quotient.mk (modulusIdeal (𝓞 K) m) x) =
28       (Algebra.norm ℤ x : ZMod m) :=
29   quotientNorm_mk _ _ _
30 
31 theorem integer_norm_congr (m : ℕ) {x y : 𝓞 K}
32     (h : x - y ∈ modulusIdeal (𝓞 K) m) :
33     (Algebra.norm ℤ x : ZMod m) = (Algebra.norm ℤ y : ZMod m) :=
34   norm_congr_of_sub_mem (Module.Free.chooseBasis ℤ (𝓞 K)) m h
35 
36 theorem integer_quotient_finite (m : ℕ) (hm : m ≠ 0) :
37     Finite (𝓞 K ⧸ modulusIdeal (𝓞 K) m) := by
38   apply Ideal.finiteQuotientOfFreeOfNeBot
39   change Ideal.span {(m : 𝓞 K)} ≠ ⊥
40   intro h
41   exact (Nat.cast_ne_zero.mpr hm) (Ideal.span_singleton_eq_bot.mp h)
42 
43 theorem integer_quotient_card (m : ℕ) :
44     Nat.card (𝓞 K ⧸ modulusIdeal (𝓞 K) m) = m ^ Module.finrank ℚ K := by
45   rw [← Submodule.cardQuot_apply, ← Ideal.absNorm_apply]
46   simp [modulusIdeal, Ideal.absNorm_span_singleton, Algebra.norm_natCast,
47     NumberField.RingOfIntegers.rank]
48 
49 theorem principal_absNorm_residue_nonneg (m : ℕ) {x : 𝓞 K}
50     (hx : 0 ≤ Algebra.norm ℤ x) :
51     (Ideal.absNorm (Ideal.span {x}) : ZMod m) =
52       integerQuotientNorm K m (Ideal.Quotient.mk (modulusIdeal (𝓞 K) m) x) := by
53   rw [integerQuotientNorm_mk, Ideal.absNorm_span_singleton]
54   have h : ((Algebra.norm ℤ x).natAbs : ℤ) = Algebra.norm ℤ x := by
55     rw [Int.natCast_natAbs, abs_of_nonneg hx]
56   simpa only [Int.cast_natCast, Int.cast_neg] using congrArg (fun z : ℤ => (z : ZMod m)) h
57 
58 theorem principal_absNorm_residue_nonpos (m : ℕ) {x : 𝓞 K}
59     (hx : Algebra.norm ℤ x ≤ 0) :
60     (Ideal.absNorm (Ideal.span {x}) : ZMod m) =
61       -integerQuotientNorm K m (Ideal.Quotient.mk (modulusIdeal (𝓞 K) m) x) := by
62   rw [integerQuotientNorm_mk, Ideal.absNorm_span_singleton]
63   have h : ((Algebra.norm ℤ x).natAbs : ℤ) = -Algebra.norm ℤ x := by
64     rw [Int.natCast_natAbs, abs_of_nonpos hx]
65   simpa only [Int.cast_natCast, Int.cast_neg] using congrArg (fun z : ℤ => (z : ZMod m)) h
66 
67 theorem principal_absNorm_congr_nonneg (m : ℕ) {x y : 𝓞 K}
68     (h : x - y ∈ modulusIdeal (𝓞 K) m)
69     (hx : 0 ≤ Algebra.norm ℤ x) (hy : 0 ≤ Algebra.norm ℤ y) :
70     (Ideal.absNorm (Ideal.span {x}) : ZMod m) =
71       (Ideal.absNorm (Ideal.span {y}) : ZMod m) := by
72   rw [principal_absNorm_residue_nonneg K m hx, principal_absNorm_residue_nonneg K m hy,
73     integerQuotientNorm_mk, integerQuotientNorm_mk]
74   exact integer_norm_congr K m h
75 
76 theorem principal_absNorm_congr_nonpos (m : ℕ) {x y : 𝓞 K}
77     (h : x - y ∈ modulusIdeal (𝓞 K) m)
78     (hx : Algebra.norm ℤ x ≤ 0) (hy : Algebra.norm ℤ y ≤ 0) :
79     (Ideal.absNorm (Ideal.span {x}) : ZMod m) =
80       (Ideal.absNorm (Ideal.span {y}) : ZMod m) := by
81   rw [principal_absNorm_residue_nonpos K m hx, principal_absNorm_residue_nonpos K m hy,
82     integerQuotientNorm_mk, integerQuotientNorm_mk]
83   exact congrArg Neg.neg (integer_norm_congr K m h)
84 
85 end PaperX.NormResidue

Back to source controls