ProfiniteSeparation.lean

1 import PaperX.GeneralCharacters
2 import Mathlib.Topology.Algebra.ClopenNhdofOne
3 
4 /-! The topological step from coverage in every finite quotient to density.
5 The arithmetic theorem that Frobenius samples have this coverage is not assumed
6 as a Lean axiom and is not proved in this module. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.ProfiniteSeparation
10 variable {G X : Type*} [Group G] [TopologicalSpace G]
11 
12 /-- Every coset of every open normal subgroup contains a conjugate of a sample.
13 For a compact group these are finite quotients. -/
14 def QuotientCoverage (s : X → G) : Prop :=
15   ∀ (H : OpenNormalSubgroup G) (g : G),
16     ∃ x k, g⁻¹ * (k * s x * k⁻¹) ∈ H
17 
18 variable [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
19 
20 theorem dense_of_quotient_coverage (s : X → G) (h : QuotientCoverage s) :
21     DenseRange (fun p : X × G => p.2 * s p.1 * p.2⁻¹) := by
22   apply dense_iff_inter_open.mpr
23   rintro U hU ⟨g, hg⟩
24   have hopen : IsOpen ((fun z : G => g * z) ⁻¹' U) :=
25     hU.preimage (continuous_const.mul continuous_id)
26   have hone : (1 : G) ∈ ((fun z : G => g * z) ⁻¹' U) := by simpa using hg
27   obtain ⟨H, hH⟩ := ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one hopen hone
28   obtain ⟨x, k, hx⟩ := h H g
29   have hu : k * s x * k⁻¹ ∈ U := by simpa [mul_assoc] using hH hx
30   exact ⟨_, hu, ⟨(x,k), rfl⟩⟩
31 
32 theorem irreducible_separator_of_quotient_coverage
33     {K I : Type*} [Field K] [CharZero K] [TopologicalSpace K]
34     [IsTopologicalRing K] [T2Space K] [Fintype I] [DecidableEq I]
35     {W : I → Type*} [∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)]
36     [∀ i, FiniteDimensional K (W i)]
37     (ρ : ∀ i, Representation K G (W i)) [∀ i, (ρ i).IsIrreducible]
38     (hne : ∀ i j, Nonempty ((ρ i).Equiv (ρ j)) → i = j)
39     (hc : ∀ i, Continuous (ρ i).character) (s : X → G) (h : QuotientCoverage s) :
40     ∃ v : I → X, Function.Injective v ∧
41       (PaperX.FiniteSeparation.sampleMatrix (fun i x => (ρ i).character (s x)) v).det ≠ 0 :=
42   PaperX.GeneralCharacters.irreducible_dense_separator ρ hne hc s
43     (dense_of_quotient_coverage s h)
44 
45 end PaperX.ProfiniteSeparation

Back to source controls