GenerationConsequences.lean

1 import RealizationBoundaries.Procyclic
2 
3 /-! # Where the new completion generator lives, and which contract it satisfies -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace RealizationBoundaries
7 
8 /-- The all-one point is not an element of the direct sum. -/
9 theorem all_one_not_finiteSupport : (1 : Ambient) ∉ finiteSupport := by
10   intro h
11   let x : finiteSupport := ⟨1, h⟩
12   obtain ⟨p, hp⟩ := finiteSupport_finite_seeds_missing {x} (Set.finite_singleton x)
13   have hz : (1 : Coordinate p) = 0 := hp x (Set.mem_singleton _)
14   exact one_ne_zero hz
15 
16 /-- The new topological generator is absent from every original paired group. -/
17 theorem all_one_not_pairedGroup (a : ℕ → Bool) : (1 : Ambient) ∉ pairedGroup a := by
18   intro h
19   let x : pairedGroup a := ⟨1, h⟩
20   obtain ⟨n, hn⟩ := paired_finite_seeds_missing a {x} (Set.finite_singleton x)
21   have hz : (1 : Coordinate (primeAt (omittedIndex a n))) = 0 := hn x (Set.mem_singleton _)
22   exact one_ne_zero hz
23 
24 /-- Infinite order is a global statement, despite finite order at every coordinate. -/
25 theorem all_one_infinite_order (m : ℕ) (hm : 0 < m) : m • (1 : Ambient) ≠ 0 := by
26   intro h
27   exact all_one_not_finiteSupport ((torsion_iff_finiteSupport 1).mp ⟨m, hm, h⟩)
28 
29 /-- The named generator in the actual completion is not an original eta point. -/
30 theorem paired_completionGenerator_not_in_eta_range (a : ℕ → Bool) :
31     completionGenerator (selectorLine (pairedSelector a)) ∉
32       Set.range (ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of (pairedGroup a))) := by
33   rintro ⟨x, hx⟩
34   have h := congrArg (profiniteCompletionEquiv (selectorLine (pairedSelector a))) hx
35   have he : x.val = (1 : Ambient) := by
36     simpa [completionGenerator] using (profiniteCompletionEquiv_eta _ x).symm.trans h
37   exact all_one_not_pairedGroup a (he ▸ x.property)
38 
39 /-- Ordinary cyclic generation is strictly smaller than topological generation. -/
40 theorem primeSeed_not_in_all_one_cyclic (p : Prime) :
41     (primeSeed p).val ∉ AddSubgroup.closure {(1 : Ambient)} := by
42   classical
43   intro h
44   obtain ⟨z, hz⟩ := AddSubgroup.mem_closure_singleton.mp h
45   have hq : (z : ℚ) • quotientMap (1 : Ambient) = 0 := by
46     rw [Int.cast_smul_eq_zsmul, ← map_zsmul, hz]
47     exact (quotientMap_eq_zero_iff _).mpr (primeSeed p).property
48   have hu : quotientMap (1 : Ambient) ≠ 0 := by
49     exact fun h0 => all_one_not_finiteSupport ((quotientMap_eq_zero_iff _).mp h0)
50   have hzq : (z : ℚ) = 0 := (smul_eq_zero.mp hq).resolve_right hu
51   have hz0 : z = 0 := by exact_mod_cast hzq
52   subst z
53   have hc := congrArg (fun x : Ambient => x p) hz
54   simp [primeSeed, cut] at hc
55 
56 theorem all_one_cyclic_ne_top : AddSubgroup.closure {(1 : Ambient)} ≠ ⊤ := by
57   intro h
58   exact primeSeed_not_in_all_one_cyclic (primeAt 0) (h.symm ▸ AddSubgroup.mem_top _)
59 
60 /-- All endomorphisms are a different contract: coordinate multiplication can produce any point. -/
61 theorem ambient_single_endomorphism_generator : endomorphismHull {(1 : Ambient)} = ⊤ := by
62   apply top_unique
63   intro x _
64   have h := orbit_mem_endomorphismHull {(1 : Ambient)} (diagonal x) (Set.mem_singleton _)
65   have he : diagonal x 1 = x := by funext p; simp
66   exact he ▸ h
67 
68 /-- Exact rank one for the full operator contract, not ordinary group generation. -/
69 theorem ambient_endomorphismSeedRank : endomorphismSeedRank Ambient = 1 := by
70   apply IsLeast.csInf_eq
71   constructor
72   · exact ⟨{1}, Cardinal.mk_set_eq_one_iff.mpr ⟨1, rfl⟩, ambient_single_endomorphism_generator⟩
73   · rintro c ⟨S, hcard, hgen⟩
74     apply Cardinal.one_le_iff_ne_zero.mpr
75     intro hc
76     have he : S = ∅ := Cardinal.mk_set_eq_zero_iff.mp (hcard.trans hc)
77     rw [he, endomorphismHull_empty] at hgen
78     exact bot_ne_top hgen
79 
80 end RealizationBoundaries

Back to source controls