Countability.lean

1 import RealizationBoundaries.NormalForms
2 import RealizationBoundaries.PairedPrimes
3 import Mathlib.Data.DFinsupp.Encodable
4 import Mathlib.Data.Rat.Encodable
5 
6 /-! # Countability of the actual infinite groups -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace RealizationBoundaries
10 
11 /-- A faithful finite-support encoding, not a finite truncation. -/
12 def finiteSupportCode (x : finiteSupport) : Π₀ p : Prime, Coordinate p := by
13   classical
14   refine ⟨x.val, Trunc.mk ⟨x.property.toFinset.val, ?_⟩⟩
15   intro p
16   by_cases hp : x.val p = 0
17   · exact Or.inr hp
18   · exact Or.inl (by simpa [support] using hp)
19 
20 @[simp] theorem finiteSupportCode_apply (x : finiteSupport) (p : Prime) :
21     finiteSupportCode x p = x.val p := rfl
22 
23 theorem finiteSupportCode_injective : Function.Injective finiteSupportCode := by
24   intro x y h
25   apply Subtype.ext
26   exact congrArg (fun f : Π₀ p : Prime, Coordinate p => (f : Ambient)) h
27 
28 instance finiteSupport_countable : Countable finiteSupport :=
29   finiteSupportCode_injective.countable
30 
31 instance normalForm_countable (S : Set Prime) : Countable (NormalForm S) :=
32   Countable.of_equiv (ℚ × finiteSupport) (NormalForm.pairEquiv S).symm
33 
34 /-- Countability does not require infinite selected support; uniqueness does. -/
35 instance selectorGroup_countable (S : Set Prime) : Countable (selectorGroup S) := by
36   apply Function.Surjective.countable (f := normalEvaluate S)
37   intro x
38   obtain ⟨r, d, h⟩ := normalForm_exists S x
39   exact ⟨(r,d), Subtype.ext h.symm⟩
40 
41 /-- For an arbitrary countable rational subspace, choose representatives and record
42 only the residual finite-support correction. No effectiveness of choice is claimed. -/
43 def preimageCountableCode (W : Submodule ℚ TailSpace) (x : preimage W) : W × finiteSupport := by
44   let w : W := preimageProjection W x
45   let y := (preimageProjection_surjective W w).choose
46   have hy := (preimageProjection_surjective W w).choose_spec
47   refine (w, ⟨x.val - y.val, ?_⟩)
48   apply (quotientMap_eq_iff _ _).mp
49   exact (congrArg Subtype.val hy).symm
50 
51 theorem preimageCountableCode_injective (W : Submodule ℚ TailSpace) :
52     Function.Injective (preimageCountableCode W) := by
53   intro x y h
54   have hw : preimageProjection W x = preimageProjection W y := congrArg Prod.fst h
55   have hd := congrArg (fun z : W × finiteSupport => z.2.val) h
56   dsimp [preimageCountableCode] at hd
57   rw [hw] at hd
58   exact Subtype.ext ((sub_left_inj.mp hd))
59 
60 instance preimage_countable (W : Submodule ℚ TailSpace) [Countable W] :
61     Countable (preimage W) :=
62   (preimageCountableCode_injective W).countable
63 
64 /-- The unit at one prime gives infinitely many distinct points of D. -/
65 def primeSeed (p : Prime) : finiteSupport :=
66   ⟨cut {p} (fun _ => 1), cut_mem_finiteSupport {p} (fun _ => 1)⟩
67 
68 theorem primeSeed_injective : Function.Injective primeSeed := by
69   classical
70   intro p q h
71   by_contra hpq
72   have heq := congrArg (fun x : finiteSupport => x.val p) h
73   simp [primeSeed, cut, hpq] at heq
74 
75 instance finiteSupport_infinite : Infinite finiteSupport :=
76   Infinite.of_injective (fun n => primeSeed (primeAt n))
77     (primeSeed_injective.comp primeAt_injective)
78 
79 instance preimage_infinite (W : Submodule ℚ TailSpace) : Infinite (preimage W) := by
80   let f : finiteSupport → preimage W := fun x => ⟨x.val, finiteSupport_le_preimage W x.property⟩
81   apply Infinite.of_injective f
82   intro x y h
83   have hv : (f x).val = (f y).val := congrArg (fun z : preimage W => z.val) h
84   exact Subtype.ext hv
85 
86 /-- Countability of a preimage is equivalent to countability of its rational quotient. -/
87 theorem preimage_countable_iff (W : Submodule ℚ TailSpace) :
88     Countable (preimage W) ↔ Countable W := by
89   constructor
90   · intro h
91     let := h
92     exact (preimageProjection_surjective W).countable
93   · intro h
94     let := h
95     infer_instance
96 
97 theorem paired_countably_infinite (a : ℕ → Bool) :
98     Countable (pairedGroup a) ∧ Infinite (pairedGroup a) := by
99   change Countable (selectorGroup (pairedSelector a)) ∧
100     Infinite (preimage (selectorLine (pairedSelector a)))
101   exact ⟨inferInstance, inferInstance⟩
102 
103 end RealizationBoundaries

Back to source controls