SubgroupSpectrum.lean

1 import RealizationBoundaries.Procyclic
2 import Mathlib.Algebra.Group.Subgroup.Finite
3 import Mathlib.SetTheory.Cardinal.Continuum
4 
5 /-! # The actual subgroup lattice and intrinsic prime spectrum of D -/
6 set_option autoImplicit false
7 noncomputable section
8 open scoped BigOperators
9 namespace RealizationBoundaries
10 
11 /-- The subgroup of the actual direct sum whose support is contained in `B`. -/
12 def spectrumSubgroup (B : Set Prime) : AddSubgroup finiteSupport where
13   carrier := {x | support x.val ⊆ B}
14   zero_mem' := by simp [support]
15   add_mem' := by
16     intro x y hx hy p hp
17     by_contra hn
18     have hx0 : x.val p = 0 := by by_contra h; exact hn (hx h)
19     have hy0 : y.val p = 0 := by by_contra h; exact hn (hy h)
20     exact hp (by simp [hx0, hy0])
21   neg_mem' := by
22     intro x hx p hp
23     exact hx (by simpa using hp)
24 
25 @[simp] theorem mem_spectrumSubgroup (B : Set Prime) (x : finiteSupport) :
26     x ∈ spectrumSubgroup B ↔ support x.val ⊆ B := Iff.rfl
27 
28 /-- Prime factors are recorded using the actual standard seeds. -/
29 def subgroupSpectrum (H : AddSubgroup finiteSupport) : Set Prime :=
30   {p | primeSeed p ∈ H}
31 
32 @[simp] theorem primeSeed_mem_spectrumSubgroup (B : Set Prime) (p : Prime) :
33     primeSeed p ∈ spectrumSubgroup B ↔ p ∈ B := by
34   classical
35   constructor
36   · intro h
37     exact h (by simp [primeSeed, cut, support])
38   · intro hp q hq
39     have hqp : q = p := by
40       by_contra hn
41       exact hq (by simp [primeSeed, cut, hn])
42     simpa [hqp] using hp
43 
44 /-- CRT multiplication isolates and normalizes a nonzero coordinate inside any subgroup. -/
45 theorem primeSeed_mem_of_coordinate_ne_zero (H : AddSubgroup finiteSupport)
46     {x : finiteSupport} (hx : x ∈ H) (p : Prime) (hp : x.val p ≠ 0) :
47     primeSeed p ∈ H := by
48   classical
49   let J := (show (support x.val).Finite from x.property).toFinset
50   let c : Ambient := fun q => if q = p then (x.val q)⁻¹ else 0
51   obtain ⟨n, hn⟩ := finite_coordinate_interpolation J c
52   have he : n • x = primeSeed p := by
53     apply Subtype.ext
54     funext q
55     by_cases hq : q = p
56     · subst q
57       have hpm : p ∈ J := by simpa [J, support] using hp
58       change (n • x.val) p = (primeSeed p).val p
59       rw [coordinate_nsmul, hn p hpm]
60       simp [c, primeSeed, cut, hp]
61     · by_cases hqJ : q ∈ J
62       · change (n • x.val) q = (primeSeed p).val q
63         rw [coordinate_nsmul, hn q hqJ]
64         simp [c, hq, primeSeed, cut]
65       · have hxq : x.val q = 0 := by simpa [J, support] using hqJ
66         change (n • x.val) q = (primeSeed p).val q
67         rw [coordinate_nsmul]
68         simp [hxq, hq, primeSeed, cut]
69   exact he ▸ H.nsmul_mem hx n
70 
71 /-- Every direct-sum vector is the finite sum of its scalar prime coordinates. -/
72 theorem finiteSupport_primeSeed_decomposition (x : finiteSupport) :
73     x = ∑ p ∈ (show (support x.val).Finite from x.property).toFinset,
74       (x.val p).val • primeSeed p := by
75   classical
76   apply Subtype.ext
77   funext q
78   simp only [AddSubgroup.val_finsetSum, AddSubgroup.coe_nsmul, Finset.sum_apply]
79   by_cases hq : q ∈ (show (support x.val).Finite from x.property).toFinset
80   · rw [Finset.sum_eq_single q]
81     · simp [primeSeed, cut]
82     · intro p _ hpq
83       simp [primeSeed, cut, Ne.symm hpq]
84     · exact fun hn => (hn hq).elim
85   · have hxq : x.val q = 0 := by simpa [support] using hq
86     rw [hxq]
87     symm
88     apply Finset.sum_eq_zero
89     intro p hp
90     have hqp : q ≠ p := by intro h; subst p; exact hq hp
91     simp [primeSeed, cut, hqp]
92 
93 /-- No subgroup has coupled prime coordinates: it is exactly its support subgroup. -/
94 theorem spectrumSubgroup_subgroupSpectrum (H : AddSubgroup finiteSupport) :
95     spectrumSubgroup (subgroupSpectrum H) = H := by
96   classical
97   apply le_antisymm
98   · intro x hx
99     rw [finiteSupport_primeSeed_decomposition x]
100     apply H.sum_mem
101     intro p hp
102     exact H.nsmul_mem (hx (by simpa using hp)) _
103   · intro x hx p hp
104     exact primeSeed_mem_of_coordinate_ne_zero H hx p hp
105 
106 @[simp] theorem subgroupSpectrum_spectrumSubgroup (B : Set Prime) :
107     subgroupSpectrum (spectrumSubgroup B) = B := by
108   ext p
109   exact primeSeed_mem_spectrumSubgroup B p
110 
111 /-- The literal subgroup lattice of D is the powerset lattice of all primes. -/
112 def subgroupSpectrumOrderIso : Set Prime ≃o AddSubgroup finiteSupport where
113   toFun := spectrumSubgroup
114   invFun := subgroupSpectrum
115   left_inv := subgroupSpectrum_spectrumSubgroup
116   right_inv := spectrumSubgroup_subgroupSpectrum
117   map_rel_iff' := by
118     intro B C
119     constructor
120     · intro h p hp
121       exact (primeSeed_mem_spectrumSubgroup C p).mp
122         (h ((primeSeed_mem_spectrumSubgroup B p).mpr hp))
123     · intro h x hx p hp
124       exact h (hx hp)
125 
126 /-- Every actual subgroup of D is fully invariant under every actual endomorphism. -/
127 theorem finiteSupport_subgroup_fullyInvariant (H : AddSubgroup finiteSupport)
128     (f : AddMonoid.End finiteSupport) {x : finiteSupport} (hx : x ∈ H) : f x ∈ H := by
129   rw [← spectrumSubgroup_subgroupSpectrum H] at hx ⊢
130   intro p hp
131   apply hx
132   intro hx0
133   exact hp (finiteSupport_endomorphism_preserves_zero f x p hx0)
134 
135 /-- Intrinsic prime-order torsion, independent of an ambient-coordinate marking. -/
136 def HasPrimeTorsion (G : Type*) [AddGroup G] (p : Prime) : Prop :=
137   ∃ x : G, x ≠ 0 ∧ p.val • x = 0
138 
139 /-- The intrinsic prime spectrum of the support subgroup is its literal selector. -/
140 theorem spectrumSubgroup_hasPrimeTorsion_iff (B : Set Prime) (p : Prime) :
141     HasPrimeTorsion (spectrumSubgroup B) p ↔ p ∈ B := by
142   classical
143   constructor
144   · rintro ⟨x, hx, hpx⟩
145     have hxp : x.val.val p ≠ 0 := by
146       intro hp
147       apply hx
148       apply Subtype.ext
149       apply Subtype.ext
150       funext q
151       by_cases hqp : q = p
152       · subst q
153         exact hp
154       · have hn : ¬ q.val ∣ p.val := by
155           intro hd
156           exact hqp (Subtype.ext ((p.property.dvd_iff_eq q.property.ne_one).mp hd).symm)
157         apply coordinate_eq_zero_of_nsmul_eq_zero q hn
158         exact congrArg (fun y : spectrumSubgroup B => y.val.val q) hpx
159     exact x.property hxp
160   · intro hp
161     let e : spectrumSubgroup B := ⟨primeSeed p,
162       (primeSeed_mem_spectrumSubgroup B p).mpr hp⟩
163     refine ⟨e, ?_, ?_⟩
164     · intro he
165       have hh := congrArg (fun y : spectrumSubgroup B => y.val.val p) he
166       simp [e, primeSeed, cut] at hh
167     · apply Subtype.ext
168       apply Subtype.ext
169       funext q
170       by_cases hqp : q = p
171       · subst q
172         simp [e, primeSeed, cut]
173       · simp [e, primeSeed, cut, hqp]
174 
175 /-- Abstract additive isomorphisms preserve the intrinsic prime-order test. -/
176 theorem hasPrimeTorsion_equiv {G H : Type*} [AddGroup G] [AddGroup H]
177     (e : G ≃+ H) (p : Prime) : HasPrimeTorsion G p ↔ HasPrimeTorsion H p := by
178   constructor
179   · rintro ⟨x, hx, hpx⟩
180     refine ⟨e x, ?_, ?_⟩
181     · exact fun h => hx (e.injective (by simpa using h))
182     · rw [← map_nsmul, hpx, map_zero]
183   · rintro ⟨x, hx, hpx⟩
184     refine ⟨e.symm x, ?_, ?_⟩
185     · exact fun h => hx (e.symm.injective (by simpa using h))
186     · rw [← map_nsmul, hpx, map_zero]
187 
188 /-- The support groups are abstractly isomorphic exactly for identical prime spectra. -/
189 theorem spectrumSubgroup_isomorphic_iff (B C : Set Prime) :
190     Nonempty (spectrumSubgroup B ≃+ spectrumSubgroup C) ↔ B = C := by
191   constructor
192   · rintro ⟨e⟩
193     ext p
194     exact (spectrumSubgroup_hasPrimeTorsion_iff B p).symm.trans
195       ((hasPrimeTorsion_equiv e p).trans (spectrumSubgroup_hasPrimeTorsion_iff C p))
196   · rintro rfl
197     exact ⟨AddEquiv.refl _⟩
198 
199 /-- Joins and intersections agree literally with union and intersection. -/
200 theorem spectrumSubgroup_union (B C : Set Prime) :
201     spectrumSubgroup (B ∪ C) = spectrumSubgroup B ⊔ spectrumSubgroup C :=
202   subgroupSpectrumOrderIso.map_sup B C
203 
204 theorem spectrumSubgroup_inter (B C : Set Prime) :
205     spectrumSubgroup (B ∩ C) = spectrumSubgroup B ⊓ spectrumSubgroup C :=
206   subgroupSpectrumOrderIso.map_inf B C
207 
208 /-- The complementary support subgroups give an internal direct-sum decomposition. -/
209 theorem spectrumSubgroup_complement (B : Set Prime) :
210     IsCompl (spectrumSubgroup B) (spectrumSubgroup Bᶜ) :=
211   subgroupSpectrumOrderIso.isCompl_iff.mp isCompl_compl
212 
213 /-- All prime selectors consistent with a prescribed finite observation. -/
214 def SpectrumObservationFiber (F : Finset Prime) (B : Set Prime) :=
215   {C : Set Prime // ∀ p ∈ F, p ∈ C ↔ p ∈ B}
216 
217 /-- Independent choices along an infinite list of unobserved prime coordinates. -/
218 def spectrumObservationChoice (F : Finset Prime) (B : Set Prime)
219     (e : ℕ ↪ {p : Prime // p ∉ F}) (S : Set ℕ) : SpectrumObservationFiber F B := by
220   refine ⟨(B ∩ (F : Set Prime)) ∪ (fun n => (e n).val) '' S, ?_⟩
221   intro p hp
222   constructor
223   · rintro (h | ⟨n, _, hn⟩)
224     · exact h.1
225     · change (e n).val = p at hn
226       exact False.elim ((e n).property (by rw [hn]; exact hp))
227   · intro h
228     exact Or.inl ⟨h, hp⟩
229 
230 theorem spectrumObservationChoice_injective (F : Finset Prime) (B : Set Prime)
231     (e : ℕ ↪ {p : Prime // p ∉ F}) :
232     Function.Injective (spectrumObservationChoice F B e) := by
233   intro S T h
234   ext n
235   have hinj : Function.Injective (fun m => (e m).val) := by
236     intro i j hij
237     exact e.injective (Subtype.ext hij)
238   have hn : (e n).val ∉ F := (e n).property
239   have hh := congrArg (fun C : SpectrumObservationFiber F B => (e n).val ∈ C.val) h
240   change ((e n).val ∈ (B ∩ (F : Set Prime)) ∪ (fun m => (e m).val) '' S) =
241     ((e n).val ∈ (B ∩ (F : Set Prime)) ∪ (fun m => (e m).val) '' T) at hh
242   simpa [hn, Set.mem_image, hinj.eq_iff] using (Eq.to_iff hh)
243 
244 /-- Exactly continuum many selectors extend each finite observation, including the empty one. -/
245 theorem spectrumObservationFiber_card (F : Finset Prime) (B : Set Prime) :
246     Cardinal.mk (SpectrumObservationFiber F B) = Cardinal.continuum := by
247   classical
248   let e : ℕ ↪ {p : Prime // p ∉ F} :=
249     Set.Infinite.natEmbedding ((F : Set Prime)ᶜ) F.finite_toSet.infinite_compl
250   apply le_antisymm
251   · calc
252       Cardinal.mk (SpectrumObservationFiber F B) ≤ Cardinal.mk (Set Prime) :=
253         Cardinal.mk_subtype_le _
254       _ = Cardinal.continuum := by
255         rw [Cardinal.mk_set, Cardinal.mk_eq_aleph0, Cardinal.two_power_aleph0]
256   · calc
257       Cardinal.continuum = Cardinal.mk (Set ℕ) := by
258         rw [Cardinal.mk_set, Cardinal.mk_nat, Cardinal.two_power_aleph0]
259       _ ≤ Cardinal.mk (SpectrumObservationFiber F B) :=
260         Cardinal.mk_le_of_injective (spectrumObservationChoice_injective F B e)
261 
262 /-- Distinct finite-observation completions yield nonisomorphic actual subgroups. -/
263 theorem spectrumObservation_not_isomorphic (F : Finset Prime) (B : Set Prime)
264     (C D : SpectrumObservationFiber F B) (h : C ≠ D) :
265     ¬ Nonempty (spectrumSubgroup C.val ≃+ spectrumSubgroup D.val) := by
266   intro he
267   exact h (Subtype.ext ((spectrumSubgroup_isomorphic_iff C.val D.val).mp he))
268 
269 /-- Every coordinate observation taken together determines its selector uniquely. -/
270 theorem spectrum_determined_by_all_observations (B C : Set Prime)
271     (h : ∀ F : Finset Prime, ∀ p ∈ F, p ∈ B ↔ p ∈ C) : B = C := by
272   classical
273   ext p
274   exact h {p} p (Finset.mem_singleton_self p)
275 
276 end RealizationBoundaries

Back to source controls