NormResidueIdealFilter.lean

1 import PaperX.NormResidueArithmetic
2 
3 /-!
4 # Finite residue filters for actual ideal norms
5 
6 For `I * J = (x)`, the norm of `I` is recovered from the residue of `x`
7 after fixing its norm sign and assuming the norm of `J` is a unit modulo `m`.
8 The residue target may be empty; no surjectivity of the norm is asserted.
9 -/
10 
11 set_option backward.isDefEq.respectTransparency.types false
12 noncomputable section
13 
14 open scoped NumberField
15 
16 namespace PaperX.NormResidue
17 
18 variable (K : Type*) [Field K] [NumberField K]
19 
20 /-- Signed residue norm, with `true` selecting the nonnegative sign. -/
21 def signedResidue (m : ℕ) (positive : Bool)
22     (q : 𝓞 K ⧸ modulusIdeal (𝓞 K) m) : ZMod m :=
23   if positive then integerQuotientNorm K m q else -integerQuotientNorm K m q
24 
25 /-- The sign condition needed to identify a signed norm with its absolute value. -/
26 def normSign (positive : Bool) (x : 𝓞 K) : Prop :=
27   if positive then 0 ≤ Algebra.norm ℤ x else Algebra.norm ℤ x ≤ 0
28 
29 theorem signedResidue_mk (m : ℕ) (positive : Bool) {x : 𝓞 K}
30     (hx : normSign K positive x) :
31     signedResidue K m positive (Ideal.Quotient.mk (modulusIdeal (𝓞 K) m) x) =
32       (Ideal.absNorm (Ideal.span {x}) : ZMod m) := by
33   cases positive with
34   | false => exact (principal_absNorm_residue_nonpos K m hx).symm
35   | true => exact (principal_absNorm_residue_nonneg K m hx).symm
36 
37 theorem ideal_product_norm_residue (m : ℕ) (I J : Ideal (𝓞 K)) {x : 𝓞 K}
38     (hIJ : I * J = Ideal.span {x}) :
39     (Ideal.absNorm I : ZMod m) * (Ideal.absNorm J : ZMod m) =
40       (Ideal.absNorm (Ideal.span {x}) : ZMod m) := by
41   rw [← Nat.cast_mul, ← map_mul, hIJ]
42 
43 theorem signedResidue_eq_ideal_product (m : ℕ) (positive : Bool)
44     (I J : Ideal (𝓞 K)) {x : 𝓞 K}
45     (hIJ : I * J = Ideal.span {x}) (hx : normSign K positive x) :
46     signedResidue K m positive (Ideal.Quotient.mk (modulusIdeal (𝓞 K) m) x) =
47       (Ideal.absNorm I : ZMod m) * (Ideal.absNorm J : ZMod m) := by
48   rw [signedResidue_mk K m positive hx, ideal_product_norm_residue K m I J hIJ]
49 
50 /-- The actual finite residue classes which encode one prescribed ideal norm residue. -/
51 def idealResidueTarget (m : ℕ) (positive : Bool) (J : Ideal (𝓞 K)) (c : ZMod m) :
52     Set (𝓞 K ⧸ modulusIdeal (𝓞 K) m) :=
53   {q | signedResidue K m positive q = c * (Ideal.absNorm J : ZMod m)}
54 
55 theorem idealResidueTarget_finite (m : ℕ) (hm : m ≠ 0) (positive : Bool)
56     (J : Ideal (𝓞 K)) (c : ZMod m) : (idealResidueTarget K m positive J c).Finite := by
57   let := integer_quotient_finite K m hm
58   exact Set.toFinite _
59 
60 theorem ideal_norm_residue_iff (m : ℕ) (positive : Bool)
61     (I J : Ideal (𝓞 K)) {x : 𝓞 K} (c : ZMod m)
62     (hIJ : I * J = Ideal.span {x}) (hx : normSign K positive x)
63     (hJ : IsUnit (Ideal.absNorm J : ZMod m)) :
64     (Ideal.absNorm I : ZMod m) = c ↔
65       Ideal.Quotient.mk (modulusIdeal (𝓞 K) m) x ∈ idealResidueTarget K m positive J c := by
66   change _ ↔ signedResidue K m positive _ = _
67   rw [signedResidue_eq_ideal_product K m positive I J hIJ hx]
68   exact hJ.mul_left_inj.symm
69 
70 theorem ideal_norm_residue_iff_of_coprime (m : ℕ) (positive : Bool)
71     (I J : Ideal (𝓞 K)) {x : 𝓞 K} (c : ZMod m)
72     (hIJ : I * J = Ideal.span {x}) (hx : normSign K positive x)
73     (hJ : (Ideal.absNorm J).Coprime m) :
74     (Ideal.absNorm I : ZMod m) = c ↔
75       Ideal.Quotient.mk (modulusIdeal (𝓞 K) m) x ∈ idealResidueTarget K m positive J c :=
76   ideal_norm_residue_iff K m positive I J c hIJ hx ((ZMod.isUnit_iff_coprime _ _).mpr hJ)
77 
78 end PaperX.NormResidue

Back to source controls