SubgroupTopology.lean

1 import RealizationBoundaries.SubgroupSpectrum
2 import Mathlib.Topology.Order
3 import Mathlib.Topology.Homeomorph.Lemmas
4 
5 /-!
6 # Cantor topology on the actual subgroup lattice of D
7 
8 The topology on Sub(D) is induced by its actual Boolean membership functions
9 on D. It is not a topology transported along the spectrum classification.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace RealizationBoundaries
14 attribute [local instance] Classical.propDecidable
15 
16 /-- The actual membership function of an arbitrary subgroup of D. -/
17 def subgroupMembership (H : AddSubgroup finiteSupport) (x : finiteSupport) : Bool :=
18   decide (x ∈ H)
19 
20 /-- The topology inherited from {0,1}^D by actual subgroup membership. -/
21 instance subgroupMembershipTopology : TopologicalSpace (AddSubgroup finiteSupport) :=
22   TopologicalSpace.induced subgroupMembership inferInstance
23 
24 /-- Binary prime selectors interpreted in the actual subgroup lattice. -/
25 def binarySpectrumEquiv : (Prime → Bool) ≃ AddSubgroup finiteSupport where
26   toFun a := spectrumSubgroup {p | a p = true}
27   invFun H p := decide (primeSeed p ∈ H)
28   left_inv a := by
29     funext p
30     simp only [primeSeed_mem_spectrumSubgroup, Set.mem_ofPred_eq, Bool.decide_coe]
31   right_inv H := by
32     have he : {p : Prime | decide (primeSeed p ∈ H) = true} = subgroupSpectrum H := by
33       ext p
34       simp [subgroupSpectrum]
35     change spectrumSubgroup {p : Prime | decide (primeSeed p ∈ H) = true} = H
36     rw [he, spectrumSubgroup_subgroupSpectrum]
37 
38 /-- Every fixed vector membership question uses only its finitely many support bits. -/
39 theorem subgroupMembership_binarySpectrum (x : finiteSupport) (a : Prime → Bool) :
40     subgroupMembership (binarySpectrumEquiv a) x =
41       decide (∀ p : {p : Prime // p ∈ x.property.toFinset}, a p.val = true) := by
42   change decide (support x.val ⊆ {p | a p = true}) = _
43   congr 1
44   apply propext
45   constructor
46   · intro hx p
47     exact hx ((Set.Finite.mem_toFinset x.property).mp p.property)
48   · intro hx p hp
49     exact hx ⟨p, (Set.Finite.mem_toFinset x.property).mpr hp⟩
50 
51 /-- Finite dependence makes every membership coordinate continuous on Cantor space. -/
52 theorem subgroupMembership_binarySpectrum_continuous (x : finiteSupport) :
53     Continuous (fun a : Prime → Bool => subgroupMembership (binarySpectrumEquiv a) x) := by
54   have he : (fun a : Prime → Bool => subgroupMembership (binarySpectrumEquiv a) x) =
55       fun a => decide (∀ p : {p : Prime // p ∈ x.property.toFinset}, a p.val = true) := by
56     funext a
57     exact subgroupMembership_binarySpectrum x a
58   rw [he]
59   let F := {p : Prime // p ∈ x.property.toFinset}
60   have hrestriction : Continuous (fun a : Prime → Bool => fun p : F => a p.val) :=
61     continuous_pi (fun p => continuous_apply p.val)
62   exact (continuous_of_discreteTopology : Continuous
63     (fun z : F → Bool => decide (∀ p, z p = true))).comp hrestriction
64 
65 /-- The subgroup membership embedding is continuous by the defining inherited topology. -/
66 theorem subgroupMembership_continuous : Continuous subgroupMembership :=
67   continuous_induced_dom
68 
69 /-- The spectrum parametrization is continuous for the independently defined
70 membership topology, because every vector has finite support. -/
71 theorem binarySpectrumEquiv_continuous : Continuous binarySpectrumEquiv := by
72   apply continuous_induced_rng.mpr
73   exact continuous_pi subgroupMembership_binarySpectrum_continuous
74 
75 /-- Prime-seed membership recovers each bit continuously. -/
76 theorem binarySpectrumEquiv_symm_continuous : Continuous binarySpectrumEquiv.symm := by
77   apply continuous_pi
78   intro p
79   exact (continuous_apply (primeSeed p)).comp subgroupMembership_continuous
80 
81 /-- The printed Cantor-space homeomorphism, with the actual inherited subgroup
82 topology and the standard product of discrete Boolean prime coordinates. -/
83 def subgroupCantorHomeomorph : (Prime → Bool) ≃ₜ AddSubgroup finiteSupport where
84   toEquiv := binarySpectrumEquiv
85   continuous_toFun := binarySpectrumEquiv_continuous
86   continuous_invFun := binarySpectrumEquiv_symm_continuous
87 
88 /-- The homeomorphism reads exactly the original prime-seed membership bits. -/
89 theorem subgroupCantorHomeomorph_primeSeed (a : Prime → Bool) (p : Prime) :
90     primeSeed p ∈ subgroupCantorHomeomorph a ↔ a p = true :=
91   primeSeed_mem_spectrumSubgroup _ _
92 
93 /-- The fixed increasing prime enumeration is onto every prime coordinate. -/
94 theorem primeAt_surjective_for_topology : Function.Surjective primeAt := by
95   intro p
96   obtain ⟨n, _, hn⟩ := Nat.exists_lt_card_nth_eq p.property
97   exact ⟨n, Subtype.ext hn⟩
98 
99 def primeEnumerationEquiv : ℕ ≃ Prime :=
100   Equiv.ofBijective primeAt ⟨primeAt_injective, primeAt_surjective_for_topology⟩
101 
102 /-- The same homeomorphism with the printed natural-number Cantor index. -/
103 def natSubgroupCantorHomeomorph : (ℕ → Bool) ≃ₜ AddSubgroup finiteSupport :=
104   (Homeomorph.piCongrLeft (Y := fun _ : Prime => Bool) primeEnumerationEquiv).trans
105     subgroupCantorHomeomorph
106 
107 end RealizationBoundaries

Back to source controls