TwistedSimple.lean

1 import PaperXI.CocycleBasis
2 import PaperXI.TwistedAlgebra
3 import PaperXI.SchrodingerFourier
4 import Mathlib.RingTheory.SimpleRing.Basic
5 import Mathlib.RingTheory.TwoSidedIdeal.Operations
6 
7 /-! Nondegenerate scalar commutators force simplicity of the actual twisted
8 algebra. Coordinate elimination is applied to two-sided ideals, so no
9 semisimplicity or matrix-algebra hypothesis enters the argument. -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperXI.TwistedSimple
13 open Module
14 open PaperXI.CocycleCommutator
15 
16 variable {A : Type*} [CommGroup A]
17 
18 /-- The commutator characters separate basis indices under nondegeneracy. -/
19 theorem commutator_separates (c : Cocycle A ℂˣ) (hnd : radical c = ⊥) :
20     ∀ u v : A, u ≠ v → ∃ i : A,
21       (↑(commutator c i u) : ℂ) ≠ (↑(commutator c i v) : ℂ) := by
22   intro u v huv
23   by_contra h
24   push Not at h
25   apply huv
26   apply (MonoidHom.ker_eq_bot_iff (characterMap c)).mp hnd
27   apply MonoidHom.ext
28   intro i
29   have hi : commutator c i u = commutator c i v := Units.ext (h i)
30   change commutator c u i = commutator c v i
31   rw [commutator_swap c i u, commutator_swap c i v, hi]
32 
33 /-- The multiplication law itself yields the scalar commutation law. -/
34 theorem basis_commute {B : Type*} [Ring B] [Algebra ℂ B]
35     (c : Cocycle A ℂˣ) (b : Basis A ℂ B)
36     (hmul : ∀ a d, b a * b d = (c.coeff a d : ℂ) • b (a * d)) (a d : A) :
37     b a * b d = (↑(commutator c a d) : ℂ) • (b d * b a) := by
38   rw [hmul, hmul, mul_comm d a, smul_smul]
39   congr 1
40   change (c.coeff a d : ℂ) = ((c.coeff a d / c.coeff d a : ℂˣ) : ℂ) * _
41   exact congrArg (fun z : ℂˣ => (z : ℂ)) (div_mul_cancel (c.coeff a d) (c.coeff d a)).symm
42 
43 /-- A two-sided ideal is closed under the scalar action from the algebra. -/
44 theorem ideal_smul_mem {B : Type*} [Ring B] [Algebra ℂ B]
45     (J : TwoSidedIdeal B) (z : ℂ) {x : B} (hx : x ∈ J) : z • x ∈ J := by
46   rw [Algebra.smul_def]
47   exact J.mul_mem_left _ _ hx
48 
49 omit [CommGroup A] in
50 /-- For a basis of units, separating scalar commutators imply that every
51 nonzero two-sided ideal contains a unit basis element. -/
52 theorem simple_of_basis {B : Type*} [Ring B] [Algebra ℂ B] [Nontrivial B]
53     [Fintype A] (b : Basis A ℂ B) (χ : A → A → ℂ)
54     (hsep : ∀ u v : A, u ≠ v → ∃ i : A, χ i u ≠ χ i v)
55     (hcomm : ∀ i a, b i * b a = χ i a • (b a * b i))
56     (hunit : ∀ i, IsUnit (b i)) : IsSimpleRing B := by
57   classical
58   apply IsSimpleRing.of_eq_bot_or_eq_top
59   intro J
60   by_cases hJ : J = ⊥
61   · exact Or.inl hJ
62   right
63   obtain ⟨x, hxJ, hx0 : x ≠ 0⟩ :=
64     SetLike.exists_of_lt (bot_lt_iff_ne_bot.mpr hJ : ⊥ < J)
65   let S : Submodule ℂ (A → ℂ) :=
66     { carrier := {f | b.equivFun.symm f ∈ J}
67       zero_mem' := by simpa only [Set.mem_ofPred_eq, map_zero] using J.zero_mem
68       add_mem' := by
69         intro f g hf hg
70         simpa only [Set.mem_ofPred_eq, map_add] using J.add_mem hf hg
71       smul_mem' := by
72         intro z f hf
73         simpa only [Set.mem_ofPred_eq, map_smul] using ideal_smul_mem J z hf }
74   have hstable : ∀ i f, f ∈ S → (fun a => χ i a * f a) ∈ S := by
75     intro i f hf
76     change b.equivFun.symm (fun a => χ i a * f a) ∈ J
77     have heq : b.equivFun.symm (fun a => χ i a * f a) * b i =
78         b i * b.equivFun.symm f := by
79       rw [Basis.equivFun_symm_apply, Basis.equivFun_symm_apply,
80         Finset.sum_mul, Finset.mul_sum]
81       apply Finset.sum_congr rfl
82       intro a _
83       rw [mul_smul_comm, hcomm]
84       simp only [smul_mul_assoc, smul_smul]
85       rw [mul_comm]
86     obtain ⟨v, hv⟩ := hunit i
87     have hmem := J.mul_mem_right _ (↑(v⁻¹) : B)
88       (heq.symm ▸ J.mul_mem_left (b i) _ hf)
89     simpa only [← hv, mul_assoc, Units.mul_inv,
90       mul_one] using hmem
91   have hxcoord : ∃ u, b.equivFun x u ≠ 0 := by
92     by_contra h
93     push Not at h
94     apply hx0
95     apply b.equivFun.injective
96     ext a
97     simpa using h a
98   obtain ⟨u, hu⟩ := hxcoord
99   have hxu : b.equivFun x ∈ S := by
100     change b.equivFun.symm (b.equivFun x) ∈ J
101     simpa using hxJ
102   have hdelta := SchrodingerFourier.coordinate_unit_mem χ hsep S hstable u
103     (b.equivFun x) hxu hu
104   have hbJ : b u ∈ J := by
105     change b.equivFun.symm (fun a => if a = u then (1 : ℂ) else 0) ∈ J at hdelta
106     have hd : (fun a => if a = u then (1 : ℂ) else 0) = b.equivFun (b u) := by
107       ext a
108       simp [Basis.equivFun_self, eq_comm]
109     simpa only [hd, LinearEquiv.symm_apply_apply] using hdelta
110   obtain ⟨v, hv⟩ := hunit u
111   apply J.eq_top
112   have h := J.mul_mem_left (↑(v⁻¹) : B) (b u) hbJ
113   simpa only [← hv, Units.inv_mul] using h
114 
115 /-- Simplicity of the constructed twisted algebra, without an assumed
116 semisimplicity, center, multiplication table, or matrix equivalence. -/
117 theorem isSimpleRing [Fintype A] (c : Cocycle A ℂˣ) (hc : Normalized c)
118     (hnd : radical c = ⊥) : IsSimpleRing (TwistedAlgebra.Algebra c hc) := by
119   apply simple_of_basis (TwistedAlgebra.basis c hc) (fun i a => ↑(commutator c i a))
120     (commutator_separates c hnd) _ (TwistedAlgebra.basis_isUnit c hc)
121   intro a d
122   rw [TwistedAlgebra.basis_mul, TwistedAlgebra.basis_mul, mul_comm d a, smul_smul]
123   congr 1
124   change (c.coeff a d : ℂ) = ((c.coeff a d / c.coeff d a : ℂˣ) : ℂ) * _
125   exact congrArg (fun z : ℂˣ => (z : ℂ))
126     (div_mul_cancel (c.coeff a d) (c.coeff d a)).symm
127 
128 /-- Elementwise nondegeneracy is equivalent to a trivial radical. -/
129 theorem radical_eq_bot_iff (c : Cocycle A ℂˣ) : radical c = ⊥ ↔
130     ∀ a : A, (∀ x : A, commutator c a x = 1) → a = 1 := by
131   rw [eq_bot_iff]
132   simp only [SetLike.le_def, mem_radical_iff, Subgroup.mem_bot]
133 
134 /-- The source-facing form of the simplicity result. -/
135 theorem isSimpleRing_of_nondegenerate [Fintype A] (c : Cocycle A ℂˣ)
136     (hc : Normalized c)
137     (hnd : ∀ a : A, (∀ x : A, commutator c a x = 1) → a = 1) :
138     IsSimpleRing (TwistedAlgebra.Algebra c hc) :=
139   isSimpleRing c hc ((radical_eq_bot_iff c).2 hnd)
140 
141 omit [CommGroup A] in
142 /-- The diagonal coordinate action is conjugation by a basis unit. This form
143 avoids choosing its inverse. -/
144 theorem diagonal_mul_basis {B : Type*} [Ring B] [Algebra ℂ B] [Fintype A]
145     (b : Basis A ℂ B) (χ : A → A → ℂ)
146     (hcomm : ∀ i a, b i * b a = χ i a • (b a * b i)) (i : A) (z : B) :
147     b.equivFun.symm (fun a => χ i a * b.equivFun z a) * b i = b i * z := by
148   conv_rhs => rw [← b.sum_equivFun z]
149   rw [Basis.equivFun_symm_apply, Finset.sum_mul, Finset.mul_sum]
150   apply Finset.sum_congr rfl
151   intro a _
152   rw [mul_smul_comm, hcomm]
153   simp only [smul_mul_assoc, smul_smul]
154   rw [mul_comm]
155 
156 /-- A central element has only its identity coefficient under nondegeneracy. -/
157 theorem center_scalar_of_basis {B : Type*} [Ring B] [Algebra ℂ B] [Fintype A]
158     (c : Cocycle A ℂˣ) (hnd : radical c = ⊥) (b : Basis A ℂ B)
159     (hmul : ∀ a d, b a * b d = (c.coeff a d : ℂ) • b (a * d))
160     (hunit : ∀ i, IsUnit (b i)) (hone : b 1 = 1)
161     (z : B) (hz : ∀ y : B, y * z = z * y) :
162     z = b.equivFun z 1 • (1 : B) := by
163   classical
164   let χ : A → A → ℂ := fun i a => ↑(commutator c i a)
165   have hcomm : ∀ i a, b i * b a = χ i a • (b a * b i) := basis_commute c b hmul
166   have hdiag (i : A) : b.equivFun.symm (fun a => χ i a * b.equivFun z a) = z :=
167     (hunit i).mul_right_cancel ((diagonal_mul_basis b χ hcomm i z).trans (hz (b i)))
168   have hcoeff (i a : A) : χ i a * b.equivFun z a = b.equivFun z a := by
169     have h := congrArg (fun w => b.equivFun w a) (hdiag i)
170     simpa only [LinearEquiv.apply_symm_apply] using h
171   have hzero (a : A) (ha : a ≠ 1) : b.equivFun z a = 0 := by
172     obtain ⟨i, hi⟩ := commutator_separates c hnd a 1 ha
173     have hi' : χ i a ≠ 1 := by simpa [χ] using hi
174     have heq : (χ i a - 1) * b.equivFun z a = 0 := by
175       rw [sub_mul, one_mul, hcoeff, sub_self]
176     exact (mul_eq_zero.mp heq).resolve_left (sub_ne_zero.mpr hi')
177   calc
178     z = ∑ a, b.equivFun z a • b a := (b.sum_equivFun z).symm
179     _ = b.equivFun z 1 • b 1 := by
180       apply Finset.sum_eq_single 1
181       · intro a _ ha
182         rw [hzero a ha, zero_smul]
183       · simp
184     _ = _ := by rw [hone]
185 
186 
187 set_option backward.isDefEq.respectTransparency false in
188 /-- The center of the actual algebra consists of unique complex scalars. -/
189 theorem center_eq_scalars [Fintype A] (c : Cocycle A ℂˣ) (hc : Normalized c)
190     (hnd : radical c = ⊥) (z : TwistedAlgebra.Algebra c hc)
191     (hz : ∀ y : TwistedAlgebra.Algebra c hc, y * z = z * y) :
192     ∃! s : ℂ, z = s • (1 : TwistedAlgebra.Algebra c hc) := by
193   have hzscalar : z = (TwistedAlgebra.basis c hc).equivFun z 1 •
194       (1 : TwistedAlgebra.Algebra c hc) := by
195     apply center_scalar_of_basis (B := TwistedAlgebra.Algebra c hc) c hnd (TwistedAlgebra.basis c hc)
196     · exact TwistedAlgebra.basis_mul c hc
197     · exact TwistedAlgebra.basis_isUnit c hc
198     · exact TwistedAlgebra.basis_one c hc
199     · exact hz
200   refine ⟨(TwistedAlgebra.basis c hc).equivFun z 1, hzscalar, ?_⟩
201   intro s hs
202   exact smul_left_injective ℂ (m := (1 : TwistedAlgebra.Algebra c hc)) (one_ne_zero : (1 : TwistedAlgebra.Algebra c hc) ≠ 0)
203     (hs.symm.trans hzscalar)
204 
205 end PaperXI.TwistedSimple

Back to source controls