SeparationForcesCoverage.lean

1 import Mathlib.Algebra.Group.ConjFinite
2 import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
3 import Mathlib.RepresentationTheory.Character
4 
5 /-! A necessary coverage condition for square trace separation.
6 This is an obstruction theorem: it does not establish arithmetic prime coverage.
7 The row count is the number of conjugacy classes. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperX.SeparationForcesCoverage
11 
12 section FiniteClasses
13 variable {C X R : Type*} [Fintype C] [DecidableEq C] [CommRing R]
14 
15 /-- A square nonsingular evaluation matrix of functions constant on fibers
16 must sample every fiber label when the label set is the row index set. -/
17 theorem surjective_labels_of_det_ne_zero (label : X → C) (f : C → X → R)
18     (hf : ∀ i x y, label x = label y → f i x = f i y) (points : C → X)
19     (hdet : Matrix.det (fun i j : C => f j (points i)) ≠ 0) :
20     Function.Surjective (fun i => label (points i)) := by
21   apply Finite.surjective_of_injective
22   intro i j hij
23   by_contra hne
24   exact hdet (Matrix.det_zero_of_row_eq hne (funext fun k => hf k _ _ hij))
25 
26 /-- Missing even one label rules out every square nonsingular evaluation matrix
27 of the indicated size. Repeating the available samples does not help. -/
28 theorem det_eq_zero_of_missing_label (label : X → C) (f : C → X → R)
29     (hf : ∀ i x y, label x = label y → f i x = f i y)
30     (missing : C) (hmiss : ∀ x, label x ≠ missing) (points : C → X) :
31     Matrix.det (fun i j : C => f j (points i)) = 0 := by
32   by_contra hdet
33   obtain ⟨i, hi⟩ := surjective_labels_of_det_ne_zero label f hf points hdet missing
34   exact hmiss (points i) hi
35 end FiniteClasses
36 
37 section Groups
38 variable {G X K : Type*} [Group G] [Fintype G] [Field K]
39 local instance : Fintype (ConjClasses G) := Fintype.ofFinite _
40 local instance : DecidableEq (ConjClasses G) := Classical.decEq _
41 
42 /-- When the matrix has one row for every conjugacy class, its invertibility
43 forces the sample family to meet every conjugacy class. -/
44 theorem conjugacy_coverage_of_det_ne_zero
45     (s : X → G) (χ : ConjClasses G → G → K)
46     (hχ : ∀ i g h, IsConj g h → χ i g = χ i h)
47     (points : ConjClasses G → X)
48     (hdet : Matrix.det (fun i j : ConjClasses G => χ j (s (points i))) ≠ 0) :
49     ∀ g : G, ∃ i : ConjClasses G, IsConj (s (points i)) g := by
50   classical
51   have hs := surjective_labels_of_det_ne_zero
52     (fun x => ConjClasses.mk (s x)) (fun j x => χ j (s x))
53     (fun i x y h => hχ i _ _ (ConjClasses.mk_eq_mk_iff_isConj.mp h)) points hdet
54   intro g
55   obtain ⟨i, hi⟩ := hs (ConjClasses.mk g)
56   exact ⟨i, ConjClasses.mk_eq_mk_iff_isConj.mp hi⟩
57 
58 /-- Finite-deletion square separation for a complete-size class-function family
59 already forces finite-deletion conjugacy coverage. -/
60 theorem cofinite_coverage_of_square_separation
61     (s : X → G) (χ : ConjClasses G → G → K)
62     (hχ : ∀ i g h, IsConj g h → χ i g = χ i h)
63     (hsep : ∀ bad : Finset X, ∃ points : ConjClasses G → X,
64       (∀ i, points i ∉ bad) ∧
65       Matrix.det (fun i j : ConjClasses G => χ j (s (points i))) ≠ 0) :
66     ∀ (bad : Finset X) (g : G), ∃ x : X, x ∉ bad ∧ IsConj (s x) g := by
67   classical
68   intro bad g
69   obtain ⟨points, hp, hd⟩ := hsep bad
70   obtain ⟨i, hi⟩ := conjugacy_coverage_of_det_ne_zero s χ hχ points hd g
71   exact ⟨points i, hp i, hi⟩
72 
73 /-- The obstruction applies to actual representation characters, even with
74 varying representation spaces. It assumes the number of rows equals the
75 number of finite conjugacy classes, but does not assume character completeness. -/
76 theorem representation_coverage_of_square_separation
77     (V : ConjClasses G → Type*) [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
78     (ρ : (i : ConjClasses G) → Representation K G (V i)) (s : X → G)
79     (hsep : ∀ bad : Finset X, ∃ points : ConjClasses G → X,
80       (∀ i, points i ∉ bad) ∧
81       Matrix.det (fun i j : ConjClasses G =>
82         Representation.character (ρ j) (s (points i))) ≠ 0) :
83     ∀ (bad : Finset X) (g : G), ∃ x : X, x ∉ bad ∧ IsConj (s x) g := by
84   apply cofinite_coverage_of_square_separation s
85     (fun i g => Representation.character (ρ i) g) ?_ hsep
86   intro i g h hgh
87   obtain ⟨a, ha⟩ := isConj_iff.mp hgh
88   rw [← ha, Representation.char_conj]
89 end Groups
90 end PaperX.SeparationForcesCoverage

Back to source controls