StructuralClosure.lean

1 import RealizationBoundaries.Countability
2 import RealizationBoundaries.RationalFG
3 import RealizationBoundaries.CyclicFiniteTargets
4 import Mathlib.GroupTheory.FiniteAbelian.Basic
5 import Mathlib.LinearAlgebra.Basis.Defs
6 import Mathlib.Data.Finsupp.Encodable
7 import Mathlib.LinearAlgebra.Dimension.Free
8 import Mathlib.LinearAlgebra.Basis.VectorSpace
9 import Mathlib.LinearAlgebra.Dimension.Finite
10 import Mathlib.Data.Rat.Lemmas
11 import Mathlib.Tactic.FieldSimp
12 import Mathlib.Tactic.NormNum
13 import Mathlib.Tactic.Ring
14 
15 /-! # Structural closure of the ambient-preimage and cocycle statements -/
16 set_option autoImplicit false
17 noncomputable section
18 namespace RealizationBoundaries
19 
20 /-- A rational vector space is countable exactly when an actual basis is countable.
21 The reverse implication uses the finite-support coefficient representation. -/
22 theorem rational_countable_iff_basis_countable {ι : Type} (W : Submodule ℚ TailSpace)
23     (b : Module.Basis ι ℚ W) : Countable W ↔ Countable ι := by
24   constructor
25   · intro h
26     let := h
27     exact b.injective.countable
28   · intro h
29     let := h
30     exact Countable.of_equiv (ι →₀ ℚ) b.repr.toEquiv.symm
31 
32 /-- Monograph 4.6: countability of the original preimage is equivalent to countable
33 rational dimension, expressed through any chosen basis of its actual quotient. -/
34 theorem preimage_countable_iff_basis_countable {ι : Type} (W : Submodule ℚ TailSpace)
35     (b : Module.Basis ι ℚ W) : Countable (preimage W) ↔ Countable ι :=
36   (preimage_countable_iff W).trans (rational_countable_iff_basis_countable W b)
37 
38 /-- The dimension formulation in the printed structural proposition. -/
39 theorem preimage_countable_iff_rational_rank (W : Submodule ℚ TailSpace) :
40     Countable (preimage W) ↔ Module.rank ℚ W ≤ Cardinal.aleph0 := by
41   rw [Module.Free.rank_eq_card_chooseBasisIndex]
42   exact (preimage_countable_iff_basis_countable W
43     (Module.Free.chooseBasis ℚ W)).trans Cardinal.mk_le_aleph0_iff.symm
44 
45 /-- Finite or countably infinite rational dimension, including the zero subspace. -/
46 theorem preimage_countable_iff_dimension_finite_or_countably_infinite
47     (W : Submodule ℚ TailSpace) :
48     Countable (preimage W) ↔
49       Module.rank ℚ W < Cardinal.aleph0 ∨ Module.rank ℚ W = Cardinal.aleph0 := by
50   rw [preimage_countable_iff_rational_rank, le_iff_lt_or_eq]
51 
52 /-- Reduction does not cancel a prime denominator when the numerator is coprime. -/
53 theorem rational_prime_fraction_den (p : Prime) (a : ℕ) (ha : Nat.Coprime a p.val) :
54     ((a : ℚ) / (p.val : ℚ)).den = p.val := by
55   have h := Rat.den_div_eq_of_coprime (a := (a : ℤ)) (b := (p.val : ℤ))
56     (by exact_mod_cast p.property.pos) (by simpa using ha)
57   change ((((a : ℚ) / (p.val : ℚ)).den : ℤ)) = (p.val : ℤ) at h
58   exact Int.ofNat_inj.mp h
59 
60 /-- At a prime denominator, a reduced fraction has the section's specified zero value. -/
61 theorem rationalSection_prime_fraction_zero (S : Set Prime) (p : Prime) (a : ℕ)
62     (ha : Nat.Coprime a p.val) :
63     rationalSection S ((a : ℚ) / (p.val : ℚ)) p = 0 := by
64   apply rationalSection_denominator_zero
65   rw [rational_prime_fraction_den p a ha]
66 
67 /-- Monograph 5.4: the negative selected indicator at one prime.
68 The equality is in the actual finite-support subgroup of the unrestricted product. -/
69 theorem cocycle_reads_coordinate (S : Set Prime) (p : Prime) :
70     cocycle S ((1 : ℚ) / (p.val : ℚ)) (((p.val - 1 : ℕ) : ℚ) / (p.val : ℚ)) =
71       -(⟨cut {p} (indicator S), cut_mem_finiteSupport {p} (indicator S)⟩ : finiteSupport) := by
72   classical
73   have hc : Nat.Coprime (p.val - 1) p.val :=
74     (Nat.coprime_self_sub_left (m := 1) p.property.one_lt.le).mpr
75       (Nat.coprime_one_left p.val)
76   have hs : (1 : ℚ) / (p.val : ℚ) + ((p.val - 1 : ℕ) : ℚ) / (p.val : ℚ) = 1 := by
77     rw [Nat.cast_sub p.property.one_lt.le]
78     have hp : (p.val : ℚ) ≠ 0 := Nat.cast_ne_zero.mpr p.property.ne_zero
79     field_simp
80     ring
81   apply Subtype.ext
82   funext q
83   by_cases hqp : q = p
84   · subst q
85     change rationalSection S ((1 : ℚ) / (p.val : ℚ)) p +
86       rationalSection S (((p.val - 1 : ℕ) : ℚ) / (p.val : ℚ)) p -
87       rationalSection S (_ + _) p = _
88     have h1 : rationalSection S ((1 : ℚ) / (p.val : ℚ)) p = 0 := by
89       simpa only [Nat.cast_one] using
90         rationalSection_prime_fraction_zero S p 1 (Nat.coprime_one_left p.val)
91     have h2 := rationalSection_prime_fraction_zero S p (p.val - 1) hc
92     rw [hs, h1, h2]
93     change 0 + 0 - rationalSection S 1 p = -(cut {p} (indicator S) p)
94     simp [cut]
95   · have hz : sectionDefect S ((1 : ℚ) / (p.val : ℚ))
96         (((p.val - 1 : ℕ) : ℚ) / (p.val : ℚ)) q = 0 := by
97       by_contra hn
98       have hd := sectionDefect_support S ((1 : ℚ) / (p.val : ℚ))
99         (((p.val - 1 : ℕ) : ℚ) / (p.val : ℚ)) hn
100       change q.val ∣ _ at hd
101       rw [show (1 : ℚ) / (p.val : ℚ) = ((1 : ℕ) : ℚ) / (p.val : ℚ) from rfl,
102         rational_prime_fraction_den p 1 (Nat.coprime_one_left p.val),
103         rational_prime_fraction_den p (p.val - 1) hc] at hd
104       have hdiv : q.val ∣ p.val := (q.property.dvd_mul.mp hd).elim id id
105       exact hqp (Subtype.ext ((p.property.dvd_iff_eq q.property.ne_one).mp hdiv).symm)
106     change sectionDefect S _ _ q = _
107     change sectionDefect S _ _ q = -(cut {p} (indicator S) q)
108     rw [hz]
109     simp [cut, hqp]
110 
111 /-- The single cocycle value recovers whether the prime was selected. -/
112 theorem cocycle_coordinate_nonzero_iff (S : Set Prime) (p : Prime) :
113     (cocycle S ((1 : ℚ) / (p.val : ℚ))
114       (((p.val - 1 : ℕ) : ℚ) / (p.val : ℚ))).val p ≠ 0 ↔ p ∈ S := by
115   classical
116   rw [cocycle_reads_coordinate]
117   change -(cut {p} (indicator S) p) ≠ 0 ↔ p ∈ S
118   by_cases h : p ∈ S <;> simp [cut, indicator, h]
119 
120 /-- A finite subgroup of an original preimage embeds into its actual order-torsion kernel. -/
121 def finiteSubgroupKernelEmbedding (W : Submodule ℚ TailSpace)
122     (H : AddSubgroup (preimage W)) [Finite H] : H →+ rootKernel W (Nat.card H) where
123   toFun x := ⟨x.val, by
124     change Nat.card H • x.val = 0
125     exact congrArg (fun z : H => z.val) (card_nsmul_eq_zero' (x := x))⟩
126   map_zero' := rfl
127   map_add' _ _ := rfl
128 
129 theorem finiteSubgroupKernelEmbedding_injective (W : Submodule ℚ TailSpace)
130     (H : AddSubgroup (preimage W)) [Finite H] :
131     Function.Injective (finiteSubgroupKernelEmbedding W H) := by
132   intro x y h
133   exact Subtype.ext (congrArg (fun z : rootKernel W (Nat.card H) => z.val) h)
134 
135 /-- Every actual finite subgroup is cyclic, not merely abstractly bounded in cardinality. -/
136 theorem finite_preimage_subgroup_cyclic (W : Submodule ℚ TailSpace)
137     (H : AddSubgroup (preimage W)) [Finite H] : IsAddCyclic H := by
138   let e : rootKernel W (Nat.card H) ≃+ ZMod (primeRadical (Nat.card H)) :=
139     (rootKernelEquiv W Nat.card_pos).trans (divisorCrtEquiv Nat.card_pos).toAddEquiv.symm
140   exact isAddCyclic_of_injective (e.toAddMonoidHom.comp (finiteSubgroupKernelEmbedding W H))
141     (e.injective.comp (finiteSubgroupKernelEmbedding_injective W H))
142 
143 /-- The order of any finite subgroup is squarefree, including the trivial subgroup of order one. -/
144 theorem finite_preimage_subgroup_squarefree (W : Submodule ℚ TailSpace)
145     (H : AddSubgroup (preimage W)) [Finite H] : Squarefree (Nat.card H) := by
146   let : Finite (rootKernel W (Nat.card H)) := rootKernel_finite W Nat.card_pos
147   have hc : primeRadical (Nat.card H) = Nat.card H := by
148     apply Nat.le_antisymm (Nat.le_of_dvd Nat.card_pos (primeRadical_dvd _))
149     have hi := Nat.card_le_card_of_injective (finiteSubgroupKernelEmbedding W H)
150       (finiteSubgroupKernelEmbedding_injective W H)
151     rwa [rootKernel_card W Nat.card_pos] at hi
152   rw [← hc]
153   exact primeRadical_squarefree _
154 
155 /-- Complete finite branch of the local subgroup classification. -/
156 theorem finite_preimage_subgroup_classification (W : Submodule ℚ TailSpace)
157     (H : AddSubgroup (preimage W)) [Finite H] :
158     ∃ m : ℕ, 0 < m ∧ Squarefree m ∧ Nonempty (H ≃+ ZMod m) := by
159   exact ⟨Nat.card H, Nat.card_pos, finite_preimage_subgroup_squarefree W H,
160     ⟨(zmodAddCyclicAddEquiv (finite_preimage_subgroup_cyclic W H)).symm⟩⟩
161 
162 /-- The rational coordinate map on the actual nonsplit selector extension. -/
163 def selectorRational {S : Set Prime} (hS : S.Infinite) : selectorGroup S →+ ℚ where
164   toFun x := ((NormalForm.realizationEquiv hS).symm x).rational
165   map_zero' := by
166     simp only [map_zero]
167     rfl
168   map_add' x y := by simp
169 
170 /-- The coordinate map vanishes exactly on the actual torsion kernel. -/
171 theorem selectorRational_eq_zero_iff {S : Set Prime} (hS : S.Infinite)
172     (x : selectorGroup S) : selectorRational hS x = 0 ↔ x.val ∈ finiteSupport := by
173   let z := (NormalForm.realizationEquiv hS).symm x
174   have hz : x.val = rationalSection S z.rational + z.finite.val := by
175     have h := NormalForm.realizationEquiv_coe hS z
176     simpa only [z, AddEquiv.apply_symm_apply] using h
177   constructor
178   · intro h
179     change z.rational = 0 at h
180     rw [hz, h, rationalSection_zero, zero_add]
181     exact z.finite.property
182   · intro h
183     have hn := normalForm_unique hS z.rational 0 z.finite ⟨x.val, h⟩
184       (by simpa using hz.symm)
185     exact hn.1
186 
187 /-- The direct product map associated to one lift of an integer quotient generator. -/
188 def integerSplitMap {L : Type} [AddCommGroup L] (f : L →+ ℤ) (x : L)
189     (_hx : f x = 1) : ℤ × f.ker →+ L where
190   toFun z := z.1 • x + z.2.val
191   map_zero' := by simp
192   map_add' z w := by simp only [Prod.fst_add, Prod.snd_add, add_zsmul,
193     AddSubgroup.coe_add]; abel
194 
195 theorem integerSplitMap_bijective {L : Type} [AddCommGroup L] (f : L →+ ℤ) (x : L)
196     (hx : f x = 1) : Function.Bijective (integerSplitMap f x hx) := by
197   constructor
198   · intro z w h
199     have hf := congrArg f h
200     have hn : z.1 = w.1 := by
201       simpa [integerSplitMap, hx, AddMonoidHom.mem_ker.mp z.2.property,
202         AddMonoidHom.mem_ker.mp w.2.property] using hf
203     apply Prod.ext hn
204     apply Subtype.ext
205     change z.1 • x + z.2.val = w.1 • x + w.2.val at h
206     rw [hn] at h
207     exact add_left_cancel h
208   · intro z
209     refine ⟨(f z, ⟨z - (f z) • x, ?_⟩), ?_⟩
210     · change f (z - (f z) • x) = 0
211       simp [hx]
212     · change (f z) • x + (z - (f z) • x) = z
213       abel
214 
215 /-- A supplied actual lift gives the full split equivalence over an integer quotient. -/
216 def integerSplitEquiv {L : Type} [AddCommGroup L] (f : L →+ ℤ) (x : L)
217     (hx : f x = 1) : L ≃+ ℤ × f.ker :=
218   (AddEquiv.ofBijective (integerSplitMap f x hx) (integerSplitMap_bijective f x hx)).symm
219 
220 /-- A split integer quotient of a finitely generated group has finitely generated kernel. -/
221 theorem integerSplitKernel_fg {L : Type} [AddCommGroup L] [AddGroup.FG L]
222     (f : L →+ ℤ) (x : L) (hx : f x = 1) : AddGroup.FG f.ker := by
223   let e := integerSplitEquiv f x hx
224   let g : L →+ f.ker := (AddMonoidHom.snd ℤ f.ker).comp e.toAddMonoidHom
225   apply AddGroup.fg_of_surjective (f := g)
226   intro k
227   exact ⟨e.symm (0, k), by simp [g]⟩
228 
229 /-- The finite subgroup classification also applies through a supplied faithful embedding. -/
230 theorem finite_embedded_preimage_classification (W : Submodule ℚ TailSpace)
231     (F : Type) [AddCommGroup F] [Finite F] (f : F →+ preimage W)
232     (hf : Function.Injective f) :
233     ∃ m : ℕ, 0 < m ∧ Squarefree m ∧ Nonempty (F ≃+ ZMod m) := by
234   let e : F ≃+ f.range := AddMonoidHom.ofInjective hf
235   let : Finite f.range := Finite.of_equiv F e.toEquiv
236   obtain ⟨m, hm, hs, ⟨g⟩⟩ := finite_preimage_subgroup_classification W f.range
237   exact ⟨m, hm, hs, ⟨e.trans g⟩⟩
238 
239 /-- The kernel of an integer quotient is finite when it is exactly torsion in the ambient group. -/
240 theorem fg_selector_integer_kernel_finite {S : Set Prime} (hS : S.Infinite)
241     (L : AddSubgroup (selectorGroup S)) [AddGroup.FG L]
242     (f : L →+ ℤ) (hf : Function.Surjective f)
243     (hker : ∀ x : L, f x = 0 → selectorRational hS x.val = 0) : Finite f.ker := by
244   obtain ⟨x, hx⟩ := hf 1
245   let : AddGroup.FG f.ker := integerSplitKernel_fg f x hx
246   apply AddCommGroup.finite_of_fg_isAddTorsion
247   intro k
248   have hfinite : k.val.val.val ∈ finiteSupport :=
249     (selectorRational_eq_zero_iff hS k.val.val).mp (hker k.val k.property)
250   obtain ⟨m, hm, hzero⟩ := (preimage_torsion_iff (selectorLine S) k.val.val).mpr hfinite
251   apply isOfFinAddOrder_iff_nsmul_eq_zero.mpr
252   exact ⟨m, hm, Subtype.ext (Subtype.ext hzero)⟩
253 
254 /-- The infinite branch, once a generator of the rational image has been chosen. -/
255 theorem fg_selector_subgroup_integer_classification {S : Set Prime} (hS : S.Infinite)
256     (L : AddSubgroup (selectorGroup S)) [AddGroup.FG L]
257     (f : L →+ ℤ) (hf : Function.Surjective f)
258     (hker : ∀ x : L, f x = 0 → selectorRational hS x.val = 0) :
259     ∃ m : ℕ, 0 < m ∧ Squarefree m ∧ Nonempty (L ≃+ ℤ × ZMod m) := by
260   let : Finite f.ker := fg_selector_integer_kernel_finite hS L f hf hker
261   let j : f.ker →+ preimage (selectorLine S) := L.subtype.comp f.ker.subtype
262   have hj : Function.Injective j := Subtype.val_injective.comp Subtype.val_injective
263   obtain ⟨m, hm, hs, ⟨g⟩⟩ := finite_embedded_preimage_classification (selectorLine S) f.ker j hj
264   obtain ⟨x, hx⟩ := hf 1
265   exact ⟨m, hm, hs, ⟨(integerSplitEquiv f x hx).trans ((AddEquiv.refl ℤ).prodCongr g)⟩⟩
266 
267 /-- Zero rational image forces a finitely generated selector subgroup to be finite. -/
268 theorem fg_selector_subgroup_finite_of_rational_zero {S : Set Prime} (hS : S.Infinite)
269     (L : AddSubgroup (selectorGroup S)) [AddGroup.FG L]
270     (hzero : ∀ x : L, selectorRational hS x.val = 0) : Finite L := by
271   apply AddCommGroup.finite_of_fg_isAddTorsion
272   intro x
273   have hfinite : x.val.val ∈ finiteSupport :=
274     (selectorRational_eq_zero_iff hS x.val).mp (hzero x)
275   obtain ⟨m, hm, hz⟩ := (preimage_torsion_iff (selectorLine S) x.val).mpr hfinite
276   exact isOfFinAddOrder_iff_nsmul_eq_zero.mpr ⟨m, hm, Subtype.ext hz⟩
277 
278 /-- Full local subgroup structure for every actual infinite selector extension. -/
279 theorem fg_selector_subgroup_classification {S : Set Prime} (hS : S.Infinite)
280     (L : AddSubgroup (selectorGroup S)) [AddGroup.FG L] :
281     ∃ m : ℕ, 0 < m ∧ Squarefree m ∧
282       (Nonempty (L ≃+ ZMod m) ∨ Nonempty (L ≃+ ℤ × ZMod m)) := by
283   let f : L →+ ℚ := (selectorRational hS).comp L.subtype
284   by_cases hzero : f.range = ⊥
285   · have hz : ∀ x : L, selectorRational hS x.val = 0 := by
286       intro x
287       have hx : f x ∈ f.range := ⟨x, rfl⟩
288       rw [hzero] at hx
289       exact hx
290     let : Finite L := fg_selector_subgroup_finite_of_rational_zero hS L hz
291     obtain ⟨m, hm, hs, he⟩ := finite_embedded_preimage_classification
292       (selectorLine S) L L.subtype Subtype.val_injective
293     exact ⟨m, hm, hs, Or.inl he⟩
294   · obtain ⟨e⟩ := rational_fg_equiv_int f.range hzero
295     let g : L →+ ℤ := e.toAddMonoidHom.comp f.rangeRestrict
296     have hg : Function.Surjective g := e.surjective.comp f.rangeRestrict_surjective
297     have hker : ∀ x : L, g x = 0 → selectorRational hS x.val = 0 := by
298       intro x hx
299       change e (f.rangeRestrict x) = 0 at hx
300       have hx' : e (f.rangeRestrict x) = e 0 := hx.trans (map_zero e).symm
301       have h := congrArg (fun y : f.range => y.val) (e.injective hx')
302       exact h
303     obtain ⟨m, hm, hs, he⟩ := fg_selector_subgroup_integer_classification hS L g hg hker
304     exact ⟨m, hm, hs, Or.inr he⟩
305 
306 /-- Monograph 5.5, with C_1 represented by the trivial group ZMod 1. -/
307 theorem paired_fg_subgroup_classification (a : ℕ → Bool)
308     (L : AddSubgroup (pairedGroup a)) (hL : L.FG) :
309     ∃ m : ℕ, 0 < m ∧ Squarefree m ∧
310       (Nonempty (L ≃+ ZMod m) ∨ Nonempty (L ≃+ ℤ × ZMod m)) := by
311   exact @fg_selector_subgroup_classification (pairedSelector a) (pairedSelector_infinite a) L
312     ((AddGroup.fg_iff_addSubgroup_fg L).mpr hL)
313 
314 end RealizationBoundaries

Back to source controls