FiniteCharacters.lean

1 import PaperX.DenseTraceSeparation
2 
3 /-! Character independence with all representation hypotheses discharged in the
4 finite-group, splitting-field case. This is NOT a proof for arbitrary profinite
5 Galois representations. Mathlib's character orthogonality theorem is the input. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.FiniteCharacters
9 
10 open scoped BigOperators
11 open PaperX.FiniteSeparation
12 universe u v w
13 variable {K : Type u} [Field K] {I : Type v} [Fintype I]
14 
15 /-- A biorthogonal family of linear tests proves linear independence. -/
16 theorem independent_of_tests {X : Type*} [DecidableEq I]
17     (f : I → X → K) (test : I → (X → K) →ₗ[K] K)
18     (ht : ∀ i j, test i (f j) = if j = i then 1 else 0) :
19     LinearIndependent K f := by
20   rw [Fintype.linearIndependent_iff]
21   intro c hc i
22   have h := congrArg (test i) hc
23   simpa [ht] using h
24 
25 /-- Averaging against an inverse character is an actual linear functional. -/
26 def characterTest {G : Type w} [Group G] [Fintype G]
27     (χ : G → K) : (G → K) →ₗ[K] K :=
28   (Nat.card G : K)⁻¹ • ∑ g, χ g⁻¹ • LinearMap.proj g
29 
30 theorem characterTest_apply {G : Type w} [Group G] [Fintype G]
31     (χ ψ : G → K) : characterTest χ ψ =
32       (Nat.card G : K)⁻¹ * ∑ g, ψ g * χ g⁻¹ := by
33   simp [characterTest, mul_comm]
34 
35 /-- Pairwise nonisomorphic irreducible finite-dimensional representations of a finite
36  group have independent characters over an algebraically closed field in which the
37  group order is invertible. Dimensions are allowed to differ. -/
38 theorem independent_irreducible_characters {G : Type w} [Group G] [Fintype G]
39     [IsAlgClosed K] [Invertible (Nat.card G : K)]
40     (n : I → ℕ) (ρ : ∀ i, Representation K G (Fin (n i) → K))
41     [∀ i, (ρ i).IsIrreducible]
42     (hne : ∀ i j, Nonempty ((ρ i).Equiv (ρ j)) → i = j) :
43     LinearIndependent K (fun i => (ρ i).character) := by
44   classical
45   apply independent_of_tests _ (fun i => characterTest (ρ i).character)
46   intro i j
47   rw [characterTest_apply, Representation.char_orthonormal]
48   by_cases h : j = i
49   · subst j
50     simp only [ite_true]
51     have he : Nonempty ((ρ i).Equiv (ρ i)) := ⟨Representation.Equiv.refl _⟩
52     simp [he]
53   · have he : ¬ Nonempty ((ρ i).Equiv (ρ j)) := fun hn => h (hne i j hn).symm
54     simp [he, h]
55 
56 /-- In this finite-group case the separator does not assume character independence. -/
57 theorem finite_group_separator {G : Type w} [Group G] [Fintype G]
58     [DecidableEq I] [IsAlgClosed K] [Invertible (Nat.card G : K)]
59     (n : I → ℕ) (ρ : ∀ i, Representation K G (Fin (n i) → K))
60     [∀ i, (ρ i).IsIrreducible]
61     (hne : ∀ i j, Nonempty ((ρ i).Equiv (ρ j)) → i = j) :
62     ∃ s : I → G, Function.Injective s ∧
63       (sampleMatrix (fun i => (ρ i).character) s).det ≠ 0 :=
64   exists_nonsingular_samples _ (independent_irreducible_characters n ρ hne)
65 
66 end PaperX.FiniteCharacters

Back to source controls