TwistedAction.lean

1 import PaperXI.TwistedAlgebra
2 
3 /-! Universal extension of actual projective operators to an action of the
4 constructed twisted group algebra. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.TwistedAction
8 
9 open CocycleCommutator Module
10 variable {A V : Type*} [CommGroup A] [Fintype A]
11 variable [AddCommGroup V] [Module ℂ V]
12 
13 /-- The canonical linear extension of a family of operators along the actual
14 basis of the constructed twisted algebra. -/
15 def linearExtension (c : Cocycle A ℂˣ) (hc : Normalized c)
16     (T : A → Module.End ℂ V) : TwistedAlgebra.Algebra c hc →ₗ[ℂ] Module.End ℂ V :=
17   (TwistedAlgebra.basis c hc).constr ℂ T
18 
19 @[simp] theorem linearExtension_basis (c : Cocycle A ℂˣ) (hc : Normalized c)
20     (T : A → Module.End ℂ V) (a : A) :
21     linearExtension c hc T (TwistedAlgebra.basis c hc a) = T a :=
22   (TwistedAlgebra.basis c hc).constr_basis ℂ T a
23 
24 theorem linearExtension_one (c : Cocycle A ℂˣ) (hc : Normalized c)
25     (T : A → Module.End ℂ V) (hOne : T 1 = 1) :
26     linearExtension c hc T 1 = 1 := by
27   rw [← TwistedAlgebra.basis_one c hc, linearExtension_basis, hOne]
28 
29 theorem linearExtension_mul (c : Cocycle A ℂˣ) (hc : Normalized c)
30     (T : A → Module.End ℂ V)
31     (hMul : ∀ a b, T a * T b = (c.coeff a b : ℂ) • T (a * b))
32     (x y : TwistedAlgebra.Algebra c hc) :
33     linearExtension c hc T (x * y) = linearExtension c hc T x * linearExtension c hc T y := by
34   classical
35   conv_lhs => rw [← (TwistedAlgebra.basis c hc).sum_repr x,
36     ← (TwistedAlgebra.basis c hc).sum_repr y]
37   conv_rhs => rw [← (TwistedAlgebra.basis c hc).sum_repr x,
38     ← (TwistedAlgebra.basis c hc).sum_repr y]
39   simp only [Finset.sum_mul, Finset.mul_sum, map_sum, map_smul, smul_mul_assoc,
40     mul_smul_comm, TwistedAlgebra.basis_mul, linearExtension_basis, hMul]
41 
42 /-- Actual algebra action extending projective operators with the prescribed
43 normalized cocycle. No action of the algebra is assumed in the inputs. -/
44 def action (c : Cocycle A ℂˣ) (hc : Normalized c)
45     (T : A → Module.End ℂ V) (hOne : T 1 = 1)
46     (hMul : ∀ a b, T a * T b = (c.coeff a b : ℂ) • T (a * b)) :
47     TwistedAlgebra.Algebra c hc →ₐ[ℂ] Module.End ℂ V :=
48   AlgHom.ofLinearMap (linearExtension c hc T)
49     (linearExtension_one c hc T hOne) (linearExtension_mul c hc T hMul)
50 
51 @[simp] theorem action_basis (c : Cocycle A ℂˣ) (hc : Normalized c)
52     (T : A → Module.End ℂ V) (hOne : T 1 = 1)
53     (hMul : ∀ a b, T a * T b = (c.coeff a b : ℂ) • T (a * b)) (a : A) :
54     action c hc T hOne hMul (TwistedAlgebra.basis c hc a) = T a :=
55   linearExtension_basis c hc T a
56 
57 /-- An algebra action is uniquely determined by its prescribed basis operators. -/
58 theorem action_unique (c : Cocycle A ℂˣ) (hc : Normalized c)
59     (T : A → Module.End ℂ V) (hOne : T 1 = 1)
60     (hMul : ∀ a b, T a * T b = (c.coeff a b : ℂ) • T (a * b))
61     (F : TwistedAlgebra.Algebra c hc →ₐ[ℂ] Module.End ℂ V)
62     (hF : ∀ a, F (TwistedAlgebra.basis c hc a) = T a) :
63     F = action c hc T hOne hMul := by
64   apply AlgHom.toLinearMap_injective
65   apply (TwistedAlgebra.basis c hc).ext
66   intro a
67   exact (hF a).trans (action_basis c hc T hOne hMul a).symm
68 
69 /-- The complete universal action property of the constructed twisted algebra. -/
70 theorem existsUnique_action (c : Cocycle A ℂˣ) (hc : Normalized c)
71     (T : A → Module.End ℂ V) (hOne : T 1 = 1)
72     (hMul : ∀ a b, T a * T b = (c.coeff a b : ℂ) • T (a * b)) :
73     ∃! F : TwistedAlgebra.Algebra c hc →ₐ[ℂ] Module.End ℂ V,
74       ∀ a, F (TwistedAlgebra.basis c hc a) = T a := by
75   refine ⟨action c hc T hOne hMul, action_basis c hc T hOne hMul, ?_⟩
76   intro F hF
77   exact action_unique c hc T hOne hMul F hF
78 
79 end PaperXI.TwistedAction

Back to source controls