GeneralCharacters.lean

1 import PaperX.SimpleModuleSeparation
2 import PaperX.DenseTraceSeparation
3 
4 /-! Character independence for arbitrary monoids in characteristic zero.
5 The arithmetic Frobenius-density input remains separate. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.GeneralCharacters
9 open scoped BigOperators MonoidAlgebra
10 section Algebra
11 variable {K G I : Type*} [Field K] [Monoid G] [Fintype I]
12 variable {W : I → Type*} [∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)]
13 variable [∀ i, FiniteDimensional K (W i)]
14 
15 omit [Fintype I] [∀ i, FiniteDimensional K (W i)] in
16 theorem module_nonisomorphic (ρ : ∀ i, Representation K G (W i))
17     (hne : ∀ i j, Nonempty ((ρ i).Equiv (ρ j)) → i = j) :
18     ∀ i j, Nonempty ((ρ i).asModule ≃ₗ[K[G]] (ρ j).asModule) → i = j := by
19   rintro i j ⟨e⟩
20   let f := (Representation.IntertwiningMap.equivLinearMapAsModule (ρ i) (ρ j)).symm
21     e.toLinearMap
22   exact hne i j ⟨f.ofBijective e.bijective⟩
23 
24 omit [Fintype I] [∀ i, FiniteDimensional K (W i)] in
25 theorem module_trace (ρ : ∀ i, Representation K G (W i)) (i : I) (a : K[G]) :
26     LinearMap.trace K (ρ i).asModule (Module.toModuleEnd K (ρ i).asModule a) =
27       LinearMap.trace K (W i) ((ρ i).asAlgebraHom a) := by
28   have h : (ρ i).asModuleEquiv.conj (Module.toModuleEnd K (ρ i).asModule a) =
29       (ρ i).asAlgebraHom a := by
30     apply LinearMap.ext
31     intro x
32     rfl
33   rw [← h, LinearMap.trace_conj']
34 
35 omit [∀ i, FiniteDimensional K (W i)] in
36 /-- A linear combination vanishing on monoid elements vanishes on the actual monoid algebra. -/
37 theorem combination_on_algebra (ρ : ∀ i, Representation K G (W i)) (c : I → K)
38     (hc : ∀ g, ∑ i, c i * (ρ i).character g = 0) (a : K[G]) :
39     ∑ i, c i * LinearMap.trace K (W i) ((ρ i).asAlgebraHom a) = 0 := by
40   induction a using MonoidAlgebra.induction_linear with
41   | zero => simp
42   | add a b ha hb => simp [map_add, mul_add, Finset.sum_add_distrib, ha, hb]
43   | single g k =>
44       simp only [Representation.asAlgebraHom_single, map_smul, smul_eq_mul]
45       calc
46         _ = k * ∑ i, c i * (ρ i).character g := by
47           rw [Finset.mul_sum]
48           apply Finset.sum_congr rfl
49           intro i _
50           simp [Representation.character, mul_left_comm]
51         _ = 0 := by rw [hc, mul_zero]
52 
53 /-- No finite-group or algebraically-closed-field hypothesis is needed here. -/
54 theorem independent_irreducible_characters [CharZero K]
55     (ρ : ∀ i, Representation K G (W i)) [∀ i, (ρ i).IsIrreducible]
56     (hne : ∀ i j, Nonempty ((ρ i).Equiv (ρ j)) → i = j) :
57     LinearIndependent K (fun i => (ρ i).character) := by
58   classical
59   have hi := PaperX.SimpleModuleSeparation.independent_module_traces
60     (K := K) (module_nonisomorphic ρ hne)
61   rw [Fintype.linearIndependent_iff] at hi ⊢
62   intro c hc
63   apply hi c
64   funext a
65   simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, Pi.zero_apply, module_trace]
66   apply combination_on_algebra ρ c
67   intro g
68   simpa using congrFun hc g
69 
70 end Algebra
71 
72 section Topological
73 variable {K G I : Type*} [Field K] [Group G] [Fintype I]
74 variable {W : I → Type*} [∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)]
75 variable [∀ i, FiniteDimensional K (W i)]
76 
77 /-- Joint continuity of the actual action gives continuous characters in coordinates. -/
78 theorem continuous_character_of_action [TopologicalSpace G] [TopologicalSpace K]
79     [IsTopologicalRing K] {n : ℕ}
80     (ρ : Representation K G (Fin n → K))
81     (hρ : Continuous (fun p : G × (Fin n → K) => ρ p.1 p.2)) :
82     Continuous ρ.character := by
83   have he (g : G) : ρ.character g =
84       ∑ i : Fin n, ρ g (Pi.single i 1) i := by
85     rw [Representation.character, LinearMap.trace_eq_matrix_trace K (Pi.basisFun K (Fin n))]
86     simp [Matrix.trace]
87   have heq : ρ.character = (fun g => ∑ i : Fin n, ρ g (Pi.single i 1) i) := funext he
88   rw [heq]
89   apply continuous_finsetSum
90   intro i _
91   exact (continuous_apply i).comp (hρ.comp (continuous_id.prodMk continuous_const))
92 
93 /-- General irreducible characters give the finite separator under the sole
94 remaining sampling hypothesis: density of the conjugacy-saturated samples. -/
95 theorem irreducible_dense_separator [CharZero K]
96     [TopologicalSpace G] [TopologicalSpace K] [IsTopologicalRing K] [T2Space K]
97     {X : Type*} [DecidableEq I]
98     (ρ : ∀ i, Representation K G (W i)) [∀ i, (ρ i).IsIrreducible]
99     (hne : ∀ i j, Nonempty ((ρ i).Equiv (ρ j)) → i = j)
100     (hc : ∀ i, Continuous (ρ i).character) (s : X → G)
101     (hd : DenseRange (fun p : X × G => p.2 * s p.1 * p.2⁻¹)) :
102     ∃ v : I → X, Function.Injective v ∧
103       (PaperX.FiniteSeparation.sampleMatrix (fun i x => (ρ i).character (s x)) v).det ≠ 0 := by
104   apply PaperX.DenseTraceSeparation.finite_conjugacy_separator _ hc
105     (independent_irreducible_characters ρ hne) s hd
106   intro i g x
107   exact (ρ i).char_conj (s x) g
108 
109 end Topological
110 end PaperX.GeneralCharacters

Back to source controls