FiniteAvoidanceBoundary.lean

1 import PaperX.ProfiniteSeparation
2 import PaperX.QuadraticCharacters
3 
4 /-! Quotient coverage alone need not survive a finite deletion of sample indices.
5 The actual group is C2 with its discrete topology. Its nonidentity element occurs
6 only at index zero, while the identity occurs at every positive index. -/
7 set_option autoImplicit false
8 noncomputable section
9 
10 namespace PaperX.FiniteAvoidanceBoundary
11 open PaperX.CompletionExamples PaperX.QuadraticCharacters
12 open PaperX.ProfiniteSeparation
13 
14 /-- A surjective family with only one occurrence of the nonidentity element. -/
15 def sample (n : ℕ) : C2 := if n = 0 then generator else 1
16 
17 @[simp] theorem sample_zero : sample 0 = generator := by simp [sample]
18 
19 @[simp] theorem sample_succ (n : ℕ) : sample (n + 1) = 1 := by simp [sample]
20 
21 theorem sample_surjective : Function.Surjective sample := by
22   intro g
23   rcases c2_cases g with rfl | rfl
24   · exact ⟨1, sample_succ 0⟩
25   · exact ⟨0, sample_zero⟩
26 
27 theorem sample_dense : DenseRange sample := sample_surjective.denseRange
28 
29 theorem sample_conjugacy_dense :
30     DenseRange (fun p : ℕ × C2 => p.2 * sample p.1 * p.2⁻¹) := by
31   apply Function.Surjective.denseRange
32   intro g
33   obtain ⟨n, hn⟩ := sample_surjective g
34   exact ⟨(n, 1), by simpa using hn⟩
35 
36 /-- Even the original finite-quotient coverage premise holds. -/
37 theorem sample_quotient_coverage : QuotientCoverage sample := by
38   intro H g
39   obtain ⟨n, hn⟩ := sample_surjective g
40   refine ⟨n, 1, ?_⟩
41   simp [hn]
42 
43 /-- The remaining indices after deleting the finite set `{0}`. -/
44 abbrev Remaining := {n : ℕ // n ∉ ({0} : Finset ℕ)}
45 
46 def remainingSample (n : Remaining) : C2 := sample n.val
47 
48 @[simp] theorem remainingSample_eq_one (n : Remaining) : remainingSample n = 1 := by
49   have hn : n.val ≠ 0 := by simpa using n.property
50   simp [remainingSample, sample, hn]
51 
52 theorem remaining_conjugate_eq_one (p : Remaining × C2) :
53     p.2 * remainingSample p.1 * p.2⁻¹ = 1 := by simp
54 
55 theorem remaining_misses_generator :
56     ∀ n : Remaining, remainingSample n ≠ generator := by
57   intro n
58   simpa using generator_ne_one.symm
59 
60 theorem remaining_not_dense : ¬ DenseRange remainingSample := by
61   intro hd
62   obtain ⟨n, hn⟩ := denseRange_discrete.mp hd generator
63   exact remaining_misses_generator n hn
64 
65 theorem remaining_conjugacy_not_dense :
66     ¬ DenseRange (fun p : Remaining × C2 =>
67       p.2 * remainingSample p.1 * p.2⁻¹) := by
68   intro hd
69   obtain ⟨p, hp⟩ := denseRange_discrete.mp hd generator
70   exact generator_ne_one (hp.symm.trans (remaining_conjugate_eq_one p))
71 
72 theorem remaining_quotient_coverage_fails : ¬ QuotientCoverage remainingSample := by
73   intro hc
74   exact remaining_conjugacy_not_dense (dense_of_quotient_coverage remainingSample hc)
75 
76 /-- These are actual unit-valued characters, with different generator values. -/
77 def signCharacter : C2 →* ℚˣ := ofRoot ⟨-1, by norm_num⟩
78 
79 def trivialCharacter : C2 →* ℚˣ := 1
80 
81 theorem characters_agree_after_deletion (n : Remaining) :
82     signCharacter (remainingSample n) = trivialCharacter (remainingSample n) := by
83   simp
84 
85 theorem characters_differ : signCharacter ≠ trivialCharacter := by
86   intro h
87   have hv := congrArg (fun χ : C2 →* ℚˣ => (χ generator : ℚ)) h
88   norm_num [signCharacter, trivialCharacter, ofRoot_generator] at hv
89 
90 end PaperX.FiniteAvoidanceBoundary

Back to source controls