GenerationRanks.lean

1 import RealizationBoundaries.SeedObstructions
2 import Mathlib.SetTheory.Cardinal.Order
3 
4 /-! # Exact least generating cardinals, with distinct generation contracts -/
5 set_option autoImplicit false
6 noncomputable section
7 open Cardinal
8 namespace RealizationBoundaries
9 universe u
10 variable {G : Type u} [AddGroup G]
11 
12 /-- The cardinals actually attained by a generating seed set. -/
13 def generationCardinals (hull : Set G → AddSubgroup G) : Set Cardinal :=
14   {c | ∃ S : Set G, Cardinal.mk S = c ∧ hull S = ⊤}
15 
16 /-- The least generating cardinal for the explicitly supplied hull operation. -/
17 def generationRank (hull : Set G → AddSubgroup G) : Cardinal :=
18   sInf (generationCardinals hull)
19 
20 /-- Ordinary topological generation does not admit extra endomorphisms. -/
21 def ordinaryTopologicalHull [TopologicalSpace G] [IsTopologicalAddGroup G]
22     (S : Set G) : AddSubgroup G := (AddSubgroup.closure S).topologicalClosure
23 
24 def endomorphismSeedRank (G : Type u) [AddGroup G] : Cardinal :=
25   generationRank (endomorphismHull (G := G))
26 
27 def topologicalEndomorphismSeedRank (G : Type u) [AddGroup G]
28     [TopologicalSpace G] [IsTopologicalAddGroup G] : Cardinal :=
29   generationRank (topologicalEndomorphismHull (G := G))
30 
31 def ordinaryTopologicalRank (G : Type u) [AddGroup G]
32     [TopologicalSpace G] [IsTopologicalAddGroup G] : Cardinal :=
33   generationRank (ordinaryTopologicalHull (G := G))
34 
35 /-- A minimum theorem, not an assigned rank: countable upper witness and finite lower obstruction. -/
36 theorem generationCardinals_isLeast_aleph0 [Countable G] [Infinite G]
37     (hull : Set G → AddSubgroup G) (hu : hull Set.univ = ⊤)
38     (hf : ∀ S : Set G, S.Finite → hull S ≠ ⊤) :
39     IsLeast (generationCardinals hull) ℵ₀ := by
40   constructor
41   · refine ⟨Set.univ, ?_, hu⟩
42     rw [Cardinal.mk_univ, Cardinal.mk_eq_aleph0 G]
43   · rintro c ⟨S, rfl, hS⟩
44     apply Cardinal.aleph0_le_mk_set.mpr
45     intro hfin
46     exact hf S hfin hS
47 
48 theorem generationRank_eq_aleph0 [Countable G] [Infinite G]
49     (hull : Set G → AddSubgroup G) (hu : hull Set.univ = ⊤)
50     (hf : ∀ S : Set G, S.Finite → hull S ≠ ⊤) :
51     generationRank hull = ℵ₀ := (generationCardinals_isLeast_aleph0 hull hu hf).csInf_eq
52 
53 theorem ordinaryHull_le_endomorphismHull (S : Set G) :
54     AddSubgroup.closure S ≤ endomorphismHull S :=
55   (AddSubgroup.closure_le _).mpr (fun _ hx => seed_mem_endomorphismHull hx)
56 
57 theorem ordinaryTopologicalHull_le_endomorphism [TopologicalSpace G]
58     [IsTopologicalAddGroup G] (S : Set G) :
59     ordinaryTopologicalHull S ≤ topologicalEndomorphismHull S :=
60   AddSubgroup.topologicalClosure_mono (ordinaryHull_le_endomorphismHull S)
61 
62 @[simp] theorem topologicalEndomorphismHull_univ [TopologicalSpace G]
63     [IsTopologicalAddGroup G] : topologicalEndomorphismHull (Set.univ : Set G) = ⊤ := by
64   apply top_unique
65   exact (endomorphismHull_univ (G := G)) ▸
66     (endomorphismHull (Set.univ : Set G)).le_topologicalClosure
67 
68 @[simp] theorem ordinaryTopologicalHull_univ [TopologicalSpace G]
69     [IsTopologicalAddGroup G] : ordinaryTopologicalHull (Set.univ : Set G) = ⊤ := by
70   apply top_unique
71   intro x _
72   exact (AddSubgroup.closure (Set.univ : Set G)).le_topologicalClosure
73     (AddSubgroup.subset_closure (Set.mem_univ x))
74 
75 /-- Monograph 2.3: the full endomorphism ring still needs exactly countably many seeds. -/
76 theorem finiteSupport_endomorphismSeedRank : endomorphismSeedRank finiteSupport = ℵ₀ :=
77   generationRank_eq_aleph0 _ endomorphismHull_univ finiteSupport_no_finite_endomorphism_seeds
78 
79 theorem finiteSupport_topologicalEndomorphismSeedRank :
80     topologicalEndomorphismSeedRank finiteSupport = ℵ₀ :=
81   generationRank_eq_aleph0 _ topologicalEndomorphismHull_univ
82     finiteSupport_no_finite_topological_seeds
83 
84 theorem finiteSupport_ordinaryTopologicalRank : ordinaryTopologicalRank finiteSupport = ℵ₀ := by
85   apply generationRank_eq_aleph0 _ ordinaryTopologicalHull_univ
86   intro S hS h
87   exact finiteSupport_no_finite_topological_seeds S hS
88     (top_unique (h ▸ ordinaryTopologicalHull_le_endomorphism S))
89 
90 instance pairedGroup_countable (a : ℕ → Bool) : Countable (pairedGroup a) :=
91   (paired_countably_infinite a).1
92 
93 instance pairedGroup_infinite (a : ℕ → Bool) : Infinite (pairedGroup a) :=
94   (paired_countably_infinite a).2
95 
96 /-- Monograph 7.9: algebraic and topological operator ranks are proved separately. -/
97 theorem paired_endomorphismSeedRank (a : ℕ → Bool) :
98     endomorphismSeedRank (pairedGroup a) = ℵ₀ :=
99   generationRank_eq_aleph0 _ endomorphismHull_univ (paired_no_finite_endomorphism_seeds a)
100 
101 theorem paired_topologicalEndomorphismSeedRank (a : ℕ → Bool) :
102     topologicalEndomorphismSeedRank (pairedGroup a) = ℵ₀ :=
103   generationRank_eq_aleph0 _ topologicalEndomorphismHull_univ
104     (paired_no_finite_topological_seeds a)
105 
106 theorem paired_ordinaryTopologicalRank (a : ℕ → Bool) :
107     ordinaryTopologicalRank (pairedGroup a) = ℵ₀ := by
108   apply generationRank_eq_aleph0 _ ordinaryTopologicalHull_univ
109   intro S hS h
110   exact paired_no_finite_topological_seeds a S hS
111     (top_unique (h ▸ ordinaryTopologicalHull_le_endomorphism S))
112 
113 end RealizationBoundaries

Back to source controls