DyadicProjectors.lean

1 import Mathlib.Algebra.MonoidAlgebra.Basic
2 import Mathlib.NumberTheory.Padics.PadicIntegers
3 import Mathlib.Tactic
4 
5 set_option autoImplicit false
6 
7 /-! Paper XII, Proposition 11.1: actual dyadic sign projectors. -/
8 namespace PaperXII.DyadicProjectors
9 
10 abbrev G := Multiplicative (ZMod 2)
11 
12 def g : G := Multiplicative.ofAdd 1
13 
14 theorem g_ne_one : g ≠ 1 := by decide
15 
16 theorem g_mul_g : g * g = 1 := by decide
17 
18 theorem group_cases (h : G) : h = 1 ∨ h = g := by
19   change h.toAdd = 0 ∨ h.toAdd = 1
20   exact (by decide : ∀ a : ZMod 2, a = 0 ∨ a = 1) h.toAdd
21 
22 section Field
23 variable {K : Type*} [Field K]
24 
25 /-- The actual group-ring basis element corresponding to the nonidentity element. -/
26 noncomputable def generator : MonoidAlgebra K G := MonoidAlgebra.single g 1
27 
28 /-- Every group algebra element has exactly its two actual group coefficients. -/
29 theorem two_coefficients (x : MonoidAlgebra K G) :
30     x = MonoidAlgebra.single 1 (x.coeff 1) + MonoidAlgebra.single g (x.coeff g) := by
31   ext h
32   rcases group_cases h with rfl | rfl <;> simp [g_ne_one, Ne.symm g_ne_one]
33 
34 /-- The positive sign idempotent, with coefficient 1/2 at each group element. -/
35 noncomputable def ePlus : MonoidAlgebra K G :=
36   MonoidAlgebra.single 1 (1 / 2) + MonoidAlgebra.single g (1 / 2)
37 
38 /-- The negative sign idempotent. -/
39 noncomputable def eMinus : MonoidAlgebra K G :=
40   MonoidAlgebra.single 1 (1 / 2) + MonoidAlgebra.single g (-(1 / 2))
41 
42 theorem ePlus_formula : ePlus (K := K) = (1 / 2 : K) • (1 + generator) := by
43   simp [ePlus, generator, smul_add, MonoidAlgebra.smul_single, MonoidAlgebra.one_def]
44 
45 theorem eMinus_formula : eMinus (K := K) = (1 / 2 : K) • (1 - generator) := by
46   simp [eMinus, generator, MonoidAlgebra.smul_single, MonoidAlgebra.one_def,
47     ← MonoidAlgebra.single_neg, sub_eq_add_neg]
48 
49 /-- Evaluation at the two characters of the actual cyclic group of order two. -/
50 noncomputable def characterMap : MonoidAlgebra K G →+* K × K where
51   toFun x := (x.coeff 1 + x.coeff g, x.coeff 1 - x.coeff g)
52   map_one' := by simp [MonoidAlgebra.one_def, g_ne_one]
53   map_zero' := by simp
54   map_add' x y := by ext <;> simp <;> ring
55   map_mul' x y := by
56     rw [two_coefficients x, two_coefficients y]
57     ext <;> simp [add_mul, mul_add, MonoidAlgebra.single_mul_single,
58       g_mul_g, g_ne_one, Ne.symm g_ne_one] <;> ring
59 
60 variable [CharZero K]
61 
62 /-- The inverse two-character transform. -/
63 noncomputable def inverseCharacters (z : K × K) : MonoidAlgebra K G :=
64   MonoidAlgebra.single 1 ((z.1 + z.2) / 2) +
65     MonoidAlgebra.single g ((z.1 - z.2) / 2)
66 
67 theorem characterMap_inverse (z : K × K) : characterMap (inverseCharacters z) = z := by
68   ext <;> simp [characterMap, inverseCharacters, g_ne_one, Ne.symm g_ne_one] <;> ring
69 
70 theorem inverse_characterMap (x : MonoidAlgebra K G) : inverseCharacters (characterMap x) = x := by
71   rw [two_coefficients x]
72   simp [characterMap, inverseCharacters, g_ne_one, Ne.symm g_ne_one]
73 
74 /-- The two-character decomposition over any field of characteristic zero. -/
75 noncomputable def characterEquiv : MonoidAlgebra K G ≃+* K × K :=
76   RingEquiv.ofBijective characterMap
77     ⟨Function.HasLeftInverse.injective ⟨inverseCharacters, inverse_characterMap⟩,
78       Function.HasRightInverse.surjective ⟨inverseCharacters, characterMap_inverse⟩⟩
79 
80 theorem characters_ePlus : characterMap (ePlus (K := K)) = (1, 0) := by
81   ext <;> simp [characterMap, ePlus, g_ne_one, Ne.symm g_ne_one]; ring
82 
83 theorem characters_eMinus : characterMap (eMinus (K := K)) = (0, 1) := by
84   ext <;> simp [characterMap, eMinus, g_ne_one, Ne.symm g_ne_one]; ring
85 
86 /-- These are complementary, orthogonal idempotents in the actual group algebra. -/
87 theorem sign_projector_relations :
88     ePlus (K := K) * ePlus = ePlus ∧ eMinus (K := K) * eMinus = eMinus ∧
89     ePlus (K := K) * eMinus = 0 ∧ ePlus (K := K) + eMinus = 1 := by
90   have inj := (characterEquiv (K := K)).injective
91   change Function.Injective (characterMap (K := K)) at inj
92   refine ⟨inj ?_, inj ?_, inj ?_, inj ?_⟩ <;>
93     simp only [map_mul, map_add, map_zero, map_one, characters_ePlus, characters_eMinus] <;>
94     ext <;> simp
95 
96 /-- There are no other idempotents besides 0, 1 and the two sign projectors. -/
97 theorem idempotent_classification (x : MonoidAlgebra K G) :
98     x * x = x ↔ x = 0 ∨ x = 1 ∨ x = ePlus ∨ x = eMinus := by
99   constructor
100   · intro hx
101     have hfield (a : K) (ha : a * a = a) : a = 0 ∨ a = 1 := by
102       have hz : a * (a - 1) = 0 := by rw [mul_sub, mul_one, ha, sub_self]
103       exact (mul_eq_zero.mp hz).imp_right sub_eq_zero.mp
104     have hy := congrArg characterMap hx
105     rw [map_mul] at hy
106     have h₁ := hfield (characterMap x).1 (congrArg Prod.fst hy)
107     have h₂ := hfield (characterMap x).2 (congrArg Prod.snd hy)
108     have inj := (characterEquiv (K := K)).injective
109     change Function.Injective (characterMap (K := K)) at inj
110     rcases h₁ with h₁ | h₁ <;> rcases h₂ with h₂ | h₂
111     · left; apply inj; ext <;> simp [h₁, h₂]
112     · right; right; right; apply inj; rw [characters_eMinus]; exact Prod.ext h₁ h₂
113     · right; right; left; apply inj; rw [characters_ePlus]; exact Prod.ext h₁ h₂
114     · right; left; apply inj; ext <;> simp [h₁, h₂]
115   · rintro (rfl | rfl | rfl | rfl)
116     · simp
117     · simp
118     · exact sign_projector_relations.1
119     · exact sign_projector_relations.2.1
120 
121 /-- The two nontrivial idempotents are nonzero. -/
122 theorem sign_projectors_nonzero : ePlus (K := K) ≠ 0 ∧ eMinus (K := K) ≠ 0 := by
123   constructor
124   · intro h
125     have hh := congrArg characterMap h
126     rw [characters_ePlus, map_zero] at hh
127     have := congrArg Prod.fst hh
128     exact one_ne_zero this
129   · intro h
130     have hh := congrArg characterMap h
131     rw [characters_eMinus, map_zero] at hh
132     have := congrArg Prod.snd hh
133     exact one_ne_zero this
134 
135 /-- Each sign projector is primitive: it has no proper nonzero idempotent below it. -/
136 theorem sign_projectors_primitive :
137     (∀ e : MonoidAlgebra K G, e * e = e → e * ePlus = e → e = 0 ∨ e = ePlus) ∧
138     (∀ e : MonoidAlgebra K G, e * e = e → e * eMinus = e → e = 0 ∨ e = eMinus) := by
139   have rel := sign_projector_relations (K := K)
140   constructor
141   · intro e he hb
142     rcases (idempotent_classification e).mp he with rfl | rfl | rfl | rfl
143     · exact Or.inl rfl
144     · exact Or.inr (by simpa using hb.symm)
145     · exact Or.inr rfl
146     · left
147       rw [mul_comm, rel.2.2.1] at hb
148       exact hb.symm
149   · intro e he hb
150     rcases (idempotent_classification e).mp he with rfl | rfl | rfl | rfl
151     · exact Or.inl rfl
152     · exact Or.inr (by simpa using hb.symm)
153     · left
154       rw [rel.2.2.1] at hb
155       exact hb.symm
156     · exact Or.inr rfl
157 
158 end Field
159 
160 /-- The canonical coefficient embedding of the actual dyadic integral group algebra. -/
161 noncomputable def integralMap : MonoidAlgebra ℤ_[2] G →+* MonoidAlgebra ℚ_[2] G :=
162   MonoidAlgebra.mapRingHom G PadicInt.Coe.ringHom
163 
164 theorem half_norm : ‖(1 / 2 : ℚ_[2])‖ = 2 := by
165   have hp : ‖(2 : ℚ_[2])‖ = (2 : ℝ)⁻¹ := by
166     exact_mod_cast (Padic.norm_p (p := 2))
167   rw [norm_div, norm_one, hp]
168   norm_num
169 
170 /-- The scalar obstruction is actual dyadic integrality, not a formal denominator rule. -/
171 theorem half_not_integral (a : ℤ_[2]) : (a : ℚ_[2]) ≠ 1 / 2 := by
172   intro ha
173   have h := a.2
174   rw [ha, half_norm] at h
175   norm_num at h
176 
177 /-- Neither actual dyadic character projector belongs to the integral coefficient image. -/
178 theorem sign_projectors_not_integral :
179     ePlus (K := ℚ_[2]) ∉ Set.range integralMap ∧
180       eMinus (K := ℚ_[2]) ∉ Set.range integralMap := by
181   constructor <;> rintro ⟨a, ha⟩
182   · have hc := congrArg (fun x : MonoidAlgebra ℚ_[2] G => x.coeff 1) ha
183     have hcoeff : (a.coeff 1 : ℚ_[2]) = 1 / 2 := by
184       simp only [integralMap, MonoidAlgebra.coeff_mapRingHom] at hc
185       change (a.coeff 1 : ℚ_[2]) = _ at hc
186       simpa [ePlus, g_ne_one] using hc
187     exact half_not_integral _ hcoeff
188   · have hc := congrArg (fun x : MonoidAlgebra ℚ_[2] G => x.coeff 1) ha
189     have hcoeff : (a.coeff 1 : ℚ_[2]) = 1 / 2 := by
190       simp only [integralMap, MonoidAlgebra.coeff_mapRingHom] at hc
191       change (a.coeff 1 : ℚ_[2]) = _ at hc
192       simpa [eMinus, g_ne_one] using hc
193     exact half_not_integral _ hcoeff
194 
195 end PaperXII.DyadicProjectors

Back to source controls