TwistedAlgebra.lean

1 import PaperXI.TwistedRegular
2 import Mathlib.LinearAlgebra.Dimension.StrongRankCondition
3 import Mathlib.LinearAlgebra.FiniteDimensional.Defs
4 
5 /-! A concrete realization of the complex twisted group algebra, including its
6 actual basis, multiplication, units, and dimension. The ambient endomorphism
7 algebra supplies the ring laws; all closure and basis assertions are proved. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.TwistedAlgebra
11 
12 open CocycleCommutator TwistedRegular Module
13 variable {A : Type*} [CommGroup A]
14 
15 /-- Linear span of all twisted left regular operators. -/
16 def operatorSpan (c : Cocycle A ℂˣ) : Submodule ℂ (Module.End ℂ (A → ℂ)) :=
17   Submodule.span ℂ (Set.range (regular c))
18 
19 theorem regular_mem (c : Cocycle A ℂˣ) (a : A) : regular c a ∈ operatorSpan c :=
20   Submodule.subset_span (Set.mem_range_self a)
21 
22 theorem one_mem (c : Cocycle A ℂˣ) (hc : Normalized c) :
23     (1 : Module.End ℂ (A → ℂ)) ∈ operatorSpan c := by
24   rw [← regular_one c hc]
25   exact regular_mem c 1
26 
27 theorem mul_mem (c : Cocycle A ℂˣ) {x y : Module.End ℂ (A → ℂ)}
28     (hx : x ∈ operatorSpan c) (hy : y ∈ operatorSpan c) : x * y ∈ operatorSpan c := by
29   induction hx using Submodule.span_induction with
30   | mem x hx =>
31       obtain ⟨a, rfl⟩ := hx
32       induction hy using Submodule.span_induction with
33       | mem y hy =>
34           obtain ⟨b, rfl⟩ := hy
35           rw [regular_mul]
36           exact (operatorSpan c).smul_mem _ (regular_mem c (a * b))
37       | zero => simp
38       | add x y _ _ hx hy => simpa [mul_add] using (operatorSpan c).add_mem hx hy
39       | smul z y _ hy => simpa [mul_smul_comm] using (operatorSpan c).smul_mem z hy
40   | zero => simp
41   | add x y _ _ hx hy => simpa [add_mul] using (operatorSpan c).add_mem hx hy
42   | smul z x _ hx => simpa [smul_mul_assoc] using (operatorSpan c).smul_mem z hx
43 
44 /-- The normalized twisted algebra as a concrete complex subalgebra. -/
45 def subalgebra (c : Cocycle A ℂˣ) (hc : Normalized c) :
46     Subalgebra ℂ (Module.End ℂ (A → ℂ)) where
47   carrier := operatorSpan c
48   zero_mem' := (operatorSpan c).zero_mem
49   add_mem' := (operatorSpan c).add_mem
50   one_mem' := one_mem c hc
51   mul_mem' := mul_mem c
52   algebraMap_mem' z := by
53     rw [Algebra.algebraMap_eq_smul_one]
54     exact (operatorSpan c).smul_mem z (one_mem c hc)
55 
56 /-- The actual complex twisted group algebra ℂᶜ[A]. -/
57 abbrev Algebra (c : Cocycle A ℂˣ) (hc : Normalized c) := subalgebra c hc
58 
59 variable [Fintype A]
60 
61 /-- Its canonical basis is proved independent by acting on the identity point mass. -/
62 def basis (c : Cocycle A ℂˣ) (hc : Normalized c) : Basis A ℂ (Algebra c hc) :=
63   (Basis.span (regular_linearIndependent c hc)).map (subalgebra c hc).toSubmoduleEquiv
64 
65 @[simp] theorem coe_basis (c : Cocycle A ℂˣ) (hc : Normalized c) (a : A) :
66     (basis c hc a : Module.End ℂ (A → ℂ)) = regular c a := by
67   unfold basis
68   erw [Basis.map_apply]
69   exact Basis.coe_span_apply (regular_linearIndependent c hc) a
70 
71 theorem basis_mul (c : Cocycle A ℂˣ) (hc : Normalized c) (a b : A) :
72     basis c hc a * basis c hc b = (c.coeff a b : ℂ) • basis c hc (a * b) := by
73   apply Subtype.ext
74   change (basis c hc a : Module.End ℂ (A → ℂ)) * basis c hc b =
75     (c.coeff a b : ℂ) • (basis c hc (a * b) : Module.End ℂ (A → ℂ))
76   simp only [coe_basis, regular_mul]
77 
78 @[simp] theorem basis_one (c : Cocycle A ℂˣ) (hc : Normalized c) :
79     basis c hc 1 = 1 := by
80   apply Subtype.ext
81   simpa using regular_one c hc
82 
83 /-- Every canonical basis vector has an explicit two-sided inverse. -/
84 def basisUnit (c : Cocycle A ℂˣ) (hc : Normalized c) (a : A) : (Algebra c hc)ˣ where
85   val := basis c hc a
86   inv := ((c.coeff a a⁻¹)⁻¹ : ℂˣ) • basis c hc a⁻¹
87   val_inv := by
88     rw [Units.smul_def, mul_smul_comm, basis_mul, mul_inv_cancel, basis_one, smul_smul]
89     simp
90   inv_val := by
91     have h : c.coeff a a⁻¹ = c.coeff a⁻¹ a := by
92       simpa [hc.1, hc.2] using c.assoc a a⁻¹ a
93     rw [Units.smul_def, smul_mul_assoc, basis_mul, inv_mul_cancel, basis_one, smul_smul, h]
94     simp
95 
96 @[simp] theorem coe_basisUnit (c : Cocycle A ℂˣ) (hc : Normalized c) (a : A) :
97     (basisUnit c hc a : Algebra c hc) = basis c hc a := rfl
98 
99 theorem basis_isUnit (c : Cocycle A ℂˣ) (hc : Normalized c) (a : A) :
100     IsUnit (basis c hc a) := (basisUnit c hc a).isUnit
101 
102 instance finiteDimensional (c : Cocycle A ℂˣ) (hc : Normalized c) :
103     FiniteDimensional ℂ (Algebra c hc) := Module.Finite.of_basis (basis c hc)
104 
105 theorem finrank_eq_card (c : Cocycle A ℂˣ) (hc : Normalized c) :
106     Module.finrank ℂ (Algebra c hc) = Fintype.card A :=
107   Module.finrank_eq_card_basis (basis c hc)
108 
109 end PaperXI.TwistedAlgebra

Back to source controls