IdealResidueUnitAction.lean

1 import PaperX.NormResidueLatticeMap
2 
3 /-! Multiplication by a residue-ring unit permutes the actual ideal residue set.
4 No surjectivity from ideal residues to the ambient residue ring is used. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperX.IdealResidueUnitAction
8 open Ideal NumberField
9 open PaperX.IdealClassQuantitative PaperX.ResidueLattice PaperX.NormResidue
10 open PaperX.NormResidueLattice
11 open scoped nonZeroDivisors
12 
13 variable (K : Type*) [Field K] [NumberField K]
14 
15 /-- Every ideal-lattice residue has a representative in the actual integral ideal. -/
16 theorem residue_mk_surjective (M J : (Ideal (𝓞 K))⁰) :
17     Function.Surjective (fun x : (J : Ideal (𝓞 K)) =>
18       (Submodule.Quotient.mk (idealPointEquiv K J x) : IdealResidues K M J)) := by
19   intro c
20   induction c using Quotient.inductionOn with
21   | h x =>
22     refine ⟨(idealPointEquiv K J).symm x, ?_⟩
23     simp only [Equiv.apply_symm_apply]
24     rfl
25 
26 /-- Multiplication by an algebraic integer descends to the actual ideal residues. -/
27 def mulResidue (M J : (Ideal (𝓞 K))⁰) (a : 𝓞 K) :
28     IdealResidues K M J → IdealResidues K M J :=
29   Quotient.lift (fun x : idealEuclideanLattice K J =>
30     Submodule.Quotient.mk (idealPointEquiv K J
31       ⟨a * integerRepresentative K J x,
32         (J : Ideal (𝓞 K)).mul_mem_left a ((idealPointEquiv K J).symm x).property⟩)) (by
33     intro x y hxy
34     apply (idealPoint_residue_eq_iff K M J _ _).mpr
35     have hrep : integerRepresentative K J x - integerRepresentative K J y ∈
36         (M : Ideal (𝓞 K)) := by
37       rw [← integerPoint_mem_iff K M, integerPoint_sub,
38         integerRepresentative_point, integerRepresentative_point]
39       exact (Submodule.Quotient.eq
40         ((idealEuclideanLattice K M).comap (idealEuclideanLattice K J).subtype)).mp
41           (Quotient.sound hxy)
42     change a * integerRepresentative K J x - a * integerRepresentative K J y ∈ _
43     rw [← mul_sub]
44     exact (M : Ideal (𝓞 K)).mul_mem_left a hrep)
45 
46 theorem mulResidue_mk (M J : (Ideal (𝓞 K))⁰) (a : 𝓞 K)
47     (x : (J : Ideal (𝓞 K))) :
48     mulResidue K M J a (Submodule.Quotient.mk (idealPointEquiv K J x)) =
49       Submodule.Quotient.mk (idealPointEquiv K J
50         ⟨a * x.1, (J : Ideal (𝓞 K)).mul_mem_left a x.2⟩) := by
51   change Submodule.Quotient.mk (idealPointEquiv K J
52     ⟨a * integerRepresentative K J (idealPointEquiv K J x), _⟩) = _
53   simp only [integerRepresentative_equiv]
54 
55 /-- An inverse modulo m acts as a genuine inverse on ideal residues when mJ≤M. -/
56 theorem mulResidue_inverse (M J : (Ideal (𝓞 K))⁰) (m : ℕ)
57     (hprod : modulusIdeal (𝓞 K) m * (J : Ideal (𝓞 K)) ≤ M)
58     (a b : 𝓞 K) (hab : a * b - 1 ∈ modulusIdeal (𝓞 K) m)
59     (c : IdealResidues K M J) :
60     mulResidue K M J a (mulResidue K M J b c) = c := by
61   obtain ⟨x, rfl⟩ := residue_mk_surjective K M J c
62   rw [mulResidue_mk, mulResidue_mk]
63   apply (idealPoint_residue_eq_iff K M J _ _).mpr
64   change a * (b * x.1) - x.1 ∈ (M : Ideal (𝓞 K))
65   have h := hprod (Ideal.mul_mem_mul hab x.2)
66   convert h using 1
67   ring
68 
69 /-- The actual permutation induced by a unit of the ring-of-integers residue ring. -/
70 def unitPerm (M J : (Ideal (𝓞 K))⁰) (m : ℕ)
71     (hprod : modulusIdeal (𝓞 K) m * (J : Ideal (𝓞 K)) ≤ M)
72     (u : (𝓞 K ⧸ modulusIdeal (𝓞 K) m)ˣ) :
73     Equiv.Perm (IdealResidues K M J) where
74   toFun := mulResidue K M J (Quotient.out (u : 𝓞 K ⧸ modulusIdeal (𝓞 K) m))
75   invFun := mulResidue K M J (Quotient.out ((u⁻¹ :
76     (𝓞 K ⧸ modulusIdeal (𝓞 K) m)ˣ) : 𝓞 K ⧸ modulusIdeal (𝓞 K) m))
77   left_inv := by
78     apply mulResidue_inverse K M J m hprod
79     apply Ideal.Quotient.eq.mp
80     simp [map_mul, Ideal.Quotient.mk_out]
81   right_inv := by
82     apply mulResidue_inverse K M J m hprod
83     apply Ideal.Quotient.eq.mp
84     simp [map_mul, Ideal.Quotient.mk_out]
85 
86 /-- Multiplication has the expected effect on the actual residue norm. -/
87 theorem residueNorm_mulResidue (M J : (Ideal (𝓞 K))⁰) (m : ℕ)
88     (hM : (M : Ideal (𝓞 K)) ≤ modulusIdeal (𝓞 K) m) (a : 𝓞 K)
89     (c : IdealResidues K M J) :
90     residueNorm K M J m hM (mulResidue K M J a c) =
91       (Algebra.norm ℤ a : ZMod m) * residueNorm K M J m hM c := by
92   obtain ⟨x, rfl⟩ := residue_mk_surjective K M J c
93   rw [mulResidue_mk, residueNorm_mk, residueNorm_mk, map_mul, Int.cast_mul]
94 
95 /-- The permutation scales the norm by the actual norm of the residue-ring unit. -/
96 theorem residueNorm_unitPerm (M J : (Ideal (𝓞 K))⁰) (m : ℕ)
97     (hprod : modulusIdeal (𝓞 K) m * (J : Ideal (𝓞 K)) ≤ M)
98     (hM : (M : Ideal (𝓞 K)) ≤ modulusIdeal (𝓞 K) m)
99     (u : (𝓞 K ⧸ modulusIdeal (𝓞 K) m)ˣ) (c : IdealResidues K M J) :
100     residueNorm K M J m hM (unitPerm K M J m hprod u c) =
101       integerQuotientNorm K m (u : 𝓞 K ⧸ modulusIdeal (𝓞 K) m) *
102         residueNorm K M J m hM c := by
103   change residueNorm K M J m hM (mulResidue K M J _ c) = _
104   rw [residueNorm_mulResidue, ← integerQuotientNorm_mk, Ideal.Quotient.mk_out]
105 
106 end PaperX.IdealResidueUnitAction

Back to source controls