Procyclic.lean

1 import RealizationBoundaries.GenerationRanks
2 import Mathlib.Data.Nat.ChineseRemainder
3 
4 /-! # Finite-coordinate interpolation and an actual topological generator -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace RealizationBoundaries
8 
9 /-- Every finite prime-coordinate pattern is realized by one nonnegative integer. -/
10 theorem finite_coordinate_interpolation (J : Finset Prime) (x : Ambient) :
11     ∃ n : ℕ, ∀ p ∈ J, (n : Coordinate p) = x p := by
12   classical
13   have hc : Set.Pairwise (J : Set Prime) (fun p q => Nat.Coprime p.val q.val) := by
14     intro p _ q _ hpq
15     exact (Nat.coprime_primes p.property q.property).mpr (fun h => hpq (Subtype.ext h))
16   let n := Nat.chineseRemainderOfFinset (fun p : Prime => (x p).val)
17     (fun p : Prime => p.val) J (fun p _ => p.property.ne_zero) hc
18   refine ⟨n.val, ?_⟩
19   intro p hp
20   have h := (ZMod.natCast_eq_natCast_iff n.val (x p).val p.val).mpr (n.property p hp)
21   simpa using h
22 
23 /-- The ordinary cyclic subgroup of the all-one point meets every open cylinder. -/
24 theorem ambient_cyclic_dense : Dense (AddSubgroup.closure {(1 : Ambient)} : Set Ambient) := by
25   apply dense_iff_inter_open.mpr
26   intro U hU hne
27   obtain ⟨x, hx⟩ := hne
28   obtain ⟨J, fJ, hJ1, hJ2⟩ := isOpen_pi_iff.mp hU x hx
29   obtain ⟨n, hn⟩ := finite_coordinate_interpolation J x
30   refine ⟨n • (1 : Ambient), ?_, ?_⟩
31   · apply hJ2
32     intro p hp
33     have he : (n • (1 : Ambient)) p = x p := by simpa using hn p hp
34     rw [he]
35     exact (hJ1 p hp).2
36   · exact (AddSubgroup.closure {(1 : Ambient)}).nsmul_mem
37       (AddSubgroup.subset_closure (Set.mem_singleton _)) n
38 
39 /-- Monograph 2.4: the closure is taken in the genuine infinite product topology. -/
40 theorem ambient_topological_generator : ordinaryTopologicalHull {(1 : Ambient)} = ⊤ := by
41   apply SetLike.ext'
42   exact ambient_cyclic_dense.closure_eq
43 
44 universe u v
45 variable {G : Type u} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G]
46 
47 @[simp] theorem ordinaryTopologicalHull_empty [T2Space G] :
48     ordinaryTopologicalHull (∅ : Set G) = ⊥ := by
49   change (AddSubgroup.closure (∅ : Set G)).topologicalClosure = ⊥
50   rw [AddSubgroup.closure_empty]
51   apply le_antisymm _ bot_le
52   apply AddSubgroup.topologicalClosure_minimal _ le_rfl
53   exact isClosed_singleton
54 
55 /-- One generator is minimal when the group is nontrivial and Hausdorff. -/
56 theorem ordinaryTopologicalRank_eq_one_of_generator [T2Space G] [Nontrivial G]
57     (g : G) (hg : ordinaryTopologicalHull {g} = ⊤) : ordinaryTopologicalRank G = 1 := by
58   apply IsLeast.csInf_eq
59   constructor
60   · exact ⟨{g}, Cardinal.mk_set_eq_one_iff.mpr ⟨g, rfl⟩, hg⟩
61   · rintro c ⟨S, hcard, hgen⟩
62     apply Cardinal.one_le_iff_ne_zero.mpr
63     intro hc
64     have he : S = ∅ := Cardinal.mk_set_eq_zero_iff.mp (hcard.trans hc)
65     rw [he, ordinaryTopologicalHull_empty] at hgen
66     exact bot_ne_top hgen
67 
68 /-- Transport of a specific generator along a genuine continuous additive equivalence. -/
69 theorem topological_generator_transport {H : Type v} [AddGroup H]
70     [TopologicalSpace H] [IsTopologicalAddGroup H]
71     (e : G ≃ₜ+ H) (g : G) (hg : ordinaryTopologicalHull {g} = ⊤) :
72     ordinaryTopologicalHull {e g} = ⊤ := by
73   let K := AddSubgroup.closure {g}
74   let L := AddSubgroup.closure {e g}
75   have hd : Dense (K : Set G) := by
76     rw [dense_iff_closure_eq]
77     exact congrArg (fun A : AddSubgroup G => (A : Set G)) hg
78   have hi : Dense (e '' (K : Set G)) := e.surjective.denseRange.dense_image e.continuous hd
79   have hsub : K ≤ L.comap e.toAddMonoidHom := by
80     apply (AddSubgroup.closure_le _).mpr
81     intro x hx
82     have h : x = g := Set.mem_singleton_iff.mp hx
83     subst x
84     exact AddSubgroup.subset_closure (Set.mem_singleton _)
85   have hl : Dense (L : Set H) := hi.mono (by
86     rintro y ⟨x, hx, rfl⟩
87     exact hsub hx)
88   apply SetLike.ext'
89   exact hl.closure_eq
90 
91 theorem ambient_ordinaryTopologicalRank : ordinaryTopologicalRank Ambient = 1 :=
92   ordinaryTopologicalRank_eq_one_of_generator 1 ambient_topological_generator
93 
94 /-- A named generator in the canonical completion, rather than a renamed product. -/
95 def completionGenerator (W : Submodule ℚ TailSpace) : CanonicalCompletion W :=
96   (profiniteCompletionEquiv W).symm 1
97 
98 theorem completionGenerator_generates (W : Submodule ℚ TailSpace) :
99     ordinaryTopologicalHull {completionGenerator W} = ⊤ :=
100   topological_generator_transport (profiniteCompletionEquiv W).symm 1 ambient_topological_generator
101 
102 theorem canonicalCompletion_ordinaryTopologicalRank (W : Submodule ℚ TailSpace) :
103     ordinaryTopologicalRank (CanonicalCompletion W) = 1 := by
104   let : Nontrivial (CanonicalCompletion W) :=
105     Function.Injective.nontrivial (profiniteCompletionEquiv W).symm.injective
106   exact ordinaryTopologicalRank_eq_one_of_generator _ (completionGenerator_generates W)
107 
108 /-- The complete seed-rank separation for every binary selector. -/
109 theorem paired_seed_rank_separation (a : ℕ → Bool) :
110     endomorphismSeedRank (pairedGroup a) = Cardinal.aleph0 ∧
111     topologicalEndomorphismSeedRank (pairedGroup a) = Cardinal.aleph0 ∧
112     ordinaryTopologicalRank (pairedGroup a) = Cardinal.aleph0 ∧
113     ordinaryTopologicalRank (CanonicalCompletion (selectorLine (pairedSelector a))) = 1 :=
114   ⟨paired_endomorphismSeedRank a, paired_topologicalEndomorphismSeedRank a,
115     paired_ordinaryTopologicalRank a, canonicalCompletion_ordinaryTopologicalRank _⟩
116 
117 end RealizationBoundaries

Back to source controls