CofiniteConjugacyCoverage.lean

1 import PaperX.ProfiniteSeparation
2 
3 /-! Finite avoidance must be retained when two coefficient primes have different
4 sets of good places. This module derives overlap density from quotient coverage
5 that survives every finite deletion. It does not prove arithmetic Chebotarev. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.CofiniteConjugacyCoverage
9 open PaperX.ProfiniteSeparation
10 
11 variable {G X : Type*} [Group G] [TopologicalSpace G]
12 
13 /-- Every finite deletion still covers every open normal quotient up to conjugacy. -/
14 def CofiniteQuotientCoverage (s : X → G) : Prop :=
15   ∀ bad : Finset X, QuotientCoverage (fun x : {x : X // x ∉ bad} => s x)
16 
17 /-- A finite exceptional set may include ramified places or a coefficient residue
18 characteristic. The chosen representatives themselves need not be dense. -/
19 theorem coverage_on_cofinite (s : X → G) (h : CofiniteQuotientCoverage s)
20     (good : X → Prop) (hf : Set.Finite {x | ¬ good x}) :
21     QuotientCoverage (fun x : {x : X // good x} => s x) := by
22   classical
23   intro H g
24   obtain ⟨x, k, hx⟩ := h hf.toFinset H g
25   have hg : good x.val := by
26     by_contra hn
27     exact x.property (hf.mem_toFinset.mpr hn)
28   exact ⟨⟨x.val, hg⟩, k, hx⟩
29 
30 variable [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
31 
32 /-- Cofinite quotient coverage supplies the precise conjugacy density on any
33 cofinite permitted domain. -/
34 theorem dense_on_cofinite (s : X → G) (h : CofiniteQuotientCoverage s)
35     (good : X → Prop) (hf : Set.Finite {x | ¬ good x}) :
36     DenseRange (fun p : {x : X // good x} × G => p.2 * s p.1 * p.2⁻¹) :=
37   dense_of_quotient_coverage _ (coverage_on_cofinite s h good hf)
38 
39 /-- Overlap density is proved for each pair; no universal all-prime good set is
40 postulated. The additional finite exclusions can be chosen freely. -/
41 theorem dense_good_overlap (s : X → G) (h : CofiniteQuotientCoverage s)
42     (good₁ good₂ : X → Prop) (h₁ : Set.Finite {x | ¬ good₁ x})
43     (h₂ : Set.Finite {x | ¬ good₂ x}) (bad : Finset X) :
44     DenseRange (fun p : {x : X // good₁ x ∧ good₂ x ∧ x ∉ bad} × G =>
45       p.2 * s p.1 * p.2⁻¹) := by
46   apply dense_on_cofinite s h
47   apply ((h₁.union h₂).union bad.finite_toSet).subset
48   intro x hx
49   simp only [Set.mem_ofPred_eq, not_and, not_not] at hx
50   by_cases ha : good₁ x
51   · by_cases hb : good₂ x
52     · exact Or.inr (hx ha hb)
53     · exact Or.inl (Or.inr hb)
54   · exact Or.inl (Or.inl ha)
55 
56 end PaperX.CofiniteConjugacyCoverage

Back to source controls