QuadraticGaloisPackets.lean

1 import PaperX.QuadraticGalois
2 import PaperX.QuadraticCharacters
3 import PaperX.QuadraticPacketBoundary
4 
5 /-! A natural arithmetic interpretation of the quadratic coordinate ring.
6 The characters are actual absolute-Galois-group homomorphisms, specified by
7 triviality on the kernel of the quotient defined by a square root of minus one. -/
8 set_option autoImplicit false
9 noncomputable section
10 open scoped Classical
11 namespace PaperX.QuadraticGaloisPackets
12 
13 open PaperX.QuadraticAlgebra PaperX.QuadraticGalois
14 open PaperX.CompletionExamples PaperX.ArithmeticCertificateExample
15 
16 variable {B C : Type*} [CommRing B] [CommRing C]
17 
18 def rootPacketEquiv : Root B ≃ Packet B :=
19   QuadraticCharacters.characterEquiv.trans descentEquiv.symm
20 
21 def ofRoot (x : Root B) : Packet B := rootPacketEquiv x
22 
23 def rootOf (χ : Packet B) : Root B := rootPacketEquiv.symm χ
24 
25 @[simp] theorem ofRoot_rootOf (χ : Packet B) : ofRoot (rootOf χ) = χ :=
26   rootPacketEquiv.apply_symm_apply χ
27 
28 @[simp] theorem rootOf_ofRoot (x : Root B) : rootOf (ofRoot x) = x :=
29   rootPacketEquiv.symm_apply_apply x
30 
31 @[simp] theorem ofRoot_val (x : Root B) :
32     (ofRoot x).val = (QuadraticCharacters.ofRoot x).comp quotientMap := rfl
33 
34 theorem ofRoot_apply_val (x : Root B) (σ : Field.absoluteGaloisGroup ℚ) :
35     ((ofRoot x).val σ : B) = if quotientMap σ = 1 then 1 else x.val :=
36   QuadraticCharacters.ofRoot_apply_val x (quotientMap σ)
37 
38 theorem ofRoot_injective : Function.Injective (ofRoot (B := B)) :=
39   rootPacketEquiv.injective
40 
41 /-- Coefficient change of the arithmetic character is the actual point reduction. -/
42 theorem ofRoot_natural (f : B →+* C) (x : Root B) :
43     mapPacket f (ofRoot x) = ofRoot (mapRoot f x) := by
44   apply Subtype.ext
45   apply MonoidHom.ext
46   intro σ
47   exact congrArg (fun ψ : C2 →* Cˣ => ψ (quotientMap σ))
48     (QuadraticCharacters.map_ofRoot f x)
49 
50 theorem rootOf_natural (f : B →+* C) (χ : Packet B) :
51     rootOf (mapPacket f χ) = mapRoot f (rootOf χ) := by
52   apply ofRoot_injective
53   rw [ofRoot_rootOf, ← ofRoot_natural, ofRoot_rootOf]
54 
55 variable (R : Type*) [CommRing R] [Algebra R B]
56 
57 /-- This equivalence identifies actual arithmetic objects, not free-standing labels. -/
58 def pointPacketEquiv : (CoordinateRing R →ₐ[R] B) ≃ Packet B :=
59   (pointEquiv R).trans rootPacketEquiv
60 
61 @[simp] theorem pointPacketEquiv_apply (p : CoordinateRing R →ₐ[R] B) :
62     pointPacketEquiv R p = ofRoot (pointEquiv R p) := rfl
63 
64 variable [Algebra R C]
65 
66 theorem pointPacketEquiv_natural (f : B →ₐ[R] C)
67     (p : CoordinateRing R →ₐ[R] B) :
68     pointPacketEquiv R (f.comp p) = mapPacket f.toRingHom (pointPacketEquiv R p) :=
69   (ofRoot_natural f.toRingHom (pointEquiv R p)).symm
70 
71 variable (B)
72 
73 def oneRoot : Root B := ⟨1, by simp⟩
74 
75 def negativeRoot : Root B := ⟨-1, by simp⟩
76 
77 variable {B}
78 
79 theorem oneRoot_character : (ofRoot (oneRoot B)).val = 1 := by
80   apply MonoidHom.ext
81   intro σ
82   apply Units.ext
83   change ((ofRoot (oneRoot B)).val σ : B) = 1
84   rw [ofRoot_apply_val]
85   simp [oneRoot]
86 
87 theorem negativeRoot_character (σ : Field.absoluteGaloisGroup ℚ) :
88     ((ofRoot (negativeRoot B)).val σ : B) =
89       if (show GQ from σ) imaginary = imaginary then 1 else -1 := by
90   rw [ofRoot_apply_val]
91   by_cases h : quotientMap σ = 1
92   · have hs := (quotientMap_eq_one_iff σ).mp h
93     simp [h, hs]
94   · have hs : ¬ (show GQ from σ) imaginary = imaginary := by
95       intro hs
96       exact h ((quotientMap_eq_one_iff σ).mpr hs)
97     simp [h, hs, negativeRoot]
98 
99 /-- The entire integral arithmetic packet has exactly the trivial and sign members. -/
100 theorem dyadic_packet_classification (χ : Packet ℤ_[2]) :
101     χ = ofRoot (oneRoot ℤ_[2]) ∨ χ = ofRoot (negativeRoot ℤ_[2]) := by
102   rcases (QuadraticPacketBoundary.dyadic_roots (rootOf χ).val).mp (rootOf χ).property with h | h
103   · left
104     rw [← ofRoot_rootOf χ]
105     exact congrArg ofRoot (Subtype.ext h)
106   · right
107     rw [← ofRoot_rootOf χ]
108     exact congrArg ofRoot (Subtype.ext h)
109 
110 theorem dyadic_packets_distinct :
111     ofRoot (oneRoot ℤ_[2]) ≠ ofRoot (negativeRoot ℤ_[2]) := by
112   intro h
113   exact QuadraticPacketBoundary.dyadic_signs_distinct
114     (congrArg Subtype.val (ofRoot_injective h))
115 
116 theorem dyadic_packets_same_residual :
117     mapPacket (PadicInt.toZMod : ℤ_[2] →+* ZMod 2) (ofRoot (oneRoot ℤ_[2])) =
118       mapPacket (PadicInt.toZMod : ℤ_[2] →+* ZMod 2) (ofRoot (negativeRoot ℤ_[2])) := by
119   rw [ofRoot_natural, ofRoot_natural]
120   apply congrArg ofRoot
121   exact Subtype.ext QuadraticPacketBoundary.signs_same_mod_two
122 
123 theorem dyadic_packets_separated_mod_four :
124     mapPacket (PadicInt.toZModPow 2 : ℤ_[2] →+* ZMod 4) (ofRoot (oneRoot ℤ_[2])) ≠
125       mapPacket (PadicInt.toZModPow 2 : ℤ_[2] →+* ZMod 4)
126         (ofRoot (negativeRoot ℤ_[2])) := by
127   rw [ofRoot_natural, ofRoot_natural]
128   intro h
129   exact QuadraticPacketBoundary.signs_distinct_mod_four
130     (congrArg Subtype.val (ofRoot_injective h))
131 
132 /-- The nonlifting scalar is an actual character of G_Q at finite precision. -/
133 def threePacket : Packet (ZMod 8) :=
134   ofRoot ⟨3, QuadraticPacketBoundary.three_root_mod_eight⟩
135 
136 theorem threePacket_no_lift :
137     ¬ ∃ χ : Packet (ZMod 16),
138       mapPacket QuadraticPacketBoundary.reduceSixteen χ = threePacket := by
139   rintro ⟨χ, hχ⟩
140   apply QuadraticPacketBoundary.three_no_root_lift_mod_sixteen
141   refine ⟨(rootOf χ).val, (rootOf χ).property, ?_⟩
142   have h := congrArg rootOf hχ
143   rw [rootOf_natural] at h
144   change mapRoot QuadraticPacketBoundary.reduceSixteen (rootOf χ) =
145     rootOf (ofRoot ⟨3, QuadraticPacketBoundary.three_root_mod_eight⟩) at h
146   rw [rootOf_ofRoot] at h
147   exact congrArg Subtype.val h
148 
149 end PaperX.QuadraticGaloisPackets

Back to source controls