DenseTraceSeparation.lean

1 import PaperX.FiniteSeparation
2 import Mathlib.RepresentationTheory.Character
3 import Mathlib.Topology.Algebra.Module.Basic
4 import Mathlib.Tactic.FunProp
5 
6 /-! Density and conjugacy input for finite trace separation.
7 Density of arithmetic Frobenius classes and character independence for general
8 Galois representations are hypotheses, not axioms or asserted new results. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperX.DenseTraceSeparation
12 
13 open scoped BigOperators
14 open PaperX.FiniteSeparation
15 universe u v w z
16 variable {K : Type u} [Field K] [TopologicalSpace K] [IsTopologicalRing K] [T2Space K]
17 variable {I : Type v} [Fintype I] {G : Type w} [TopologicalSpace G] {X : Type z}
18 
19 /-- Restriction along a dense map preserves independence of continuous functions. -/
20 theorem independent_dense_restriction (f : I → G → K)
21     (hc : ∀ i, Continuous (f i)) (hi : LinearIndependent K f)
22     (s : X → G) (hd : DenseRange s) :
23     LinearIndependent K (fun i => f i ∘ s) := by
24   rw [Fintype.linearIndependent_iff]
25   intro c hzero
26   apply (Fintype.linearIndependent_iff.mp hi) c
27   have hcont : Continuous (fun g => ∑ i, c i * f i g) := by fun_prop
28   have heq : (fun g => ∑ i, c i * f i g) = (fun _ => (0 : K)) := by
29     apply hd.equalizer hcont continuous_const
30     funext x
31     simpa [Function.comp_def] using congrFun hzero x
32   funext g
33   simpa using congrFun heq g
34 
35 /-- Only the conjugacy saturation must be dense. Chosen representatives themselves
36 need not be a dense subset of a noncommutative group. -/
37 theorem independent_conjugacy_samples [Group G] (f : I → G → K)
38     (hc : ∀ i, Continuous (f i)) (hi : LinearIndependent K f)
39     (s : X → G)
40     (hd : DenseRange (fun p : X × G => p.2 * s p.1 * p.2⁻¹))
41     (hconj : ∀ i g x, f i (g * s x * g⁻¹) = f i (s x)) :
42     LinearIndependent K (fun i x => f i (s x)) := by
43   rw [Fintype.linearIndependent_iff]
44   intro c hzero
45   apply (Fintype.linearIndependent_iff.mp hi) c
46   have hcont : Continuous (fun g => ∑ i, c i * f i g) := by fun_prop
47   have heq : (fun g => ∑ i, c i * f i g) = (fun _ => (0 : K)) := by
48     apply hd.equalizer hcont continuous_const
49     funext p
50     simpa [Function.comp_def, hconj] using congrFun hzero p.1
51   funext g
52   simpa using congrFun heq g
53 
54 /-- The exact finite conclusion under explicit topological and character inputs. -/
55 theorem finite_conjugacy_separator [Group G] [DecidableEq I]
56     (f : I → G → K) (hc : ∀ i, Continuous (f i)) (hi : LinearIndependent K f)
57     (s : X → G)
58     (hd : DenseRange (fun p : X × G => p.2 * s p.1 * p.2⁻¹))
59     (hconj : ∀ i g x, f i (g * s x * g⁻¹) = f i (s x)) :
60     ∃ v : I → X, Function.Injective v ∧
61       (sampleMatrix (fun i x => f i (s x)) v).det ≠ 0 :=
62   exists_nonsingular_samples _ (independent_conjugacy_samples f hc hi s hd hconj)
63 
64 /-- Specialization to actual representation characters, with varying finite dimensions.
65 Character invariance under conjugation is proved by Mathlib, not assumed. -/
66 theorem representation_trace_separator [Group G] [DecidableEq I]
67     (n : I → ℕ) (ρ : ∀ i, Representation K G (Fin (n i) → K))
68     (hc : ∀ i, Continuous (ρ i).character)
69     (hi : LinearIndependent K (fun i => (ρ i).character))
70     (s : X → G)
71     (hd : DenseRange (fun p : X × G => p.2 * s p.1 * p.2⁻¹)) :
72     ∃ v : I → X, Function.Injective v ∧
73       (sampleMatrix (fun i x => (ρ i).character (s x)) v).det ≠ 0 := by
74   apply finite_conjugacy_separator _ hc hi s hd
75   intro i g x
76   exact (ρ i).char_conj (s x) g
77 
78 end PaperX.DenseTraceSeparation

Back to source controls