TwistedMatrix.lean

1 import PaperXI.TwistedSimple
2 import Mathlib.RingTheory.SimpleModule.IsAlgClosed
3 import Mathlib.Analysis.Complex.Polynomial.Basic
4 import Mathlib.LinearAlgebra.Dimension.Constructions
5 import Mathlib.Data.Nat.Sqrt
6 
7 /-! The matrix-algebra part of Paper XI, Proposition 8.3. Simplicity is proved
8 for the constructed twisted algebra before invoking Wedderburn–Artin. No
9 finite-image condition is imposed on the cocycle. -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperXI.TwistedMatrix
13 
14 open Module CocycleCommutator
15 
16 /-- A finite-dimensional simple complex algebra has square dimension and an
17 actual matrix-algebra equivalence of that degree. -/
18 theorem exists_matrix (R : Type*) [Ring R] [Algebra ℂ R]
19     [FiniteDimensional ℂ R] [IsSimpleRing R] :
20     ∃ n : ℕ, 0 < n ∧ Module.finrank ℂ R = n ^ 2 ∧
21       Nonempty (R ≃ₐ[ℂ] Matrix (Fin n) (Fin n) ℂ) := by
22   obtain ⟨n, hn, ⟨e⟩⟩ := IsSimpleRing.exists_algEquiv_matrix_of_isAlgClosed ℂ R
23   refine ⟨n, Nat.pos_of_ne_zero (NeZero.ne n), ?_, ⟨e⟩⟩
24   simpa [Module.finrank_matrix, pow_two] using e.toLinearEquiv.finrank_eq
25 
26 /-- The matrix size is the integer square root of the algebra dimension. -/
27 theorem matrix_sqrt (R : Type*) [Ring R] [Algebra ℂ R]
28     [FiniteDimensional ℂ R] [IsSimpleRing R] :
29     Nonempty (R ≃ₐ[ℂ]
30       Matrix (Fin (Nat.sqrt (Module.finrank ℂ R)))
31         (Fin (Nat.sqrt (Module.finrank ℂ R))) ℂ) := by
32   obtain ⟨n, _, hd, he⟩ := exists_matrix R
33   rw [hd, Nat.sqrt_eq']
34   exact he
35 
36 variable {A : Type*} [CommGroup A] [Fintype A]
37 
38 /-- Nondegeneracy proves that the order of the index group is a positive square. -/
39 theorem order_square (c : Cocycle A ℂˣ) (hc : Normalized c)
40     (hnd : radical c = ⊥) : ∃ n : ℕ, 0 < n ∧ Fintype.card A = n ^ 2 := by
41   let : IsSimpleRing (TwistedAlgebra.Algebra c hc) := TwistedSimple.isSimpleRing c hc hnd
42   obtain ⟨n, hn, hd, _⟩ := exists_matrix (TwistedAlgebra.Algebra c hc)
43   exact ⟨n, hn, (TwistedAlgebra.finrank_eq_card c hc).symm.trans hd⟩
44 
45 /-- Proposition 8.3's actual twisted-algebra isomorphism, at the claimed degree. -/
46 theorem classification (c : Cocycle A ℂˣ) (hc : Normalized c)
47     (hnd : radical c = ⊥) :
48     Nonempty (TwistedAlgebra.Algebra c hc ≃ₐ[ℂ]
49       Matrix (Fin (Nat.sqrt (Fintype.card A))) (Fin (Nat.sqrt (Fintype.card A))) ℂ) := by
50   let : IsSimpleRing (TwistedAlgebra.Algebra c hc) := TwistedSimple.isSimpleRing c hc hnd
51   rw [← TwistedAlgebra.finrank_eq_card c hc]
52   exact matrix_sqrt (TwistedAlgebra.Algebra c hc)
53 
54 end PaperXI.TwistedMatrix

Back to source controls