TwistedActionEquivalence.lean

1 import PaperXI.TwistedAction
2 import PaperXI.TwistedModules
3 import PaperXI.AlgebraActionModule
4 import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
5 
6 /-! The actual algebra action of an irreducible projective operator family is
7 an isomorphism when its scalar commutator is nondegenerate. -/
8 set_option autoImplicit false
9 set_option backward.isDefEq.respectTransparency false
10 noncomputable section
11 namespace PaperXI.TwistedActionEquivalence
12 open CocycleCommutator AlgebraActionModule
13 
14 variable {A V : Type*} [CommGroup A] [Fintype A]
15 variable [AddCommGroup V] [Module ℂ V]
16 variable (c : Cocycle A ℂˣ) (hc : Normalized c)
17 variable (T : A → Module.End ℂ V) (hOne : T 1 = 1)
18 variable (hMul : ∀ a b, T a * T b = (c.coeff a b : ℂ) • T (a * b))
19 
20 /-- Stability for the actual extended action is equivalent to generator stability. -/
21 theorem stable_iff (S : Submodule ℂ V) :
22     Stable (B := ↥(TwistedAlgebra.Algebra c hc)) (TwistedAction.action c hc T hOne hMul) S ↔
23       ∀ a v, v ∈ S → T a v ∈ S := by
24   constructor
25   · intro h a v hv
26     simpa only [TwistedAction.action_basis] using h (TwistedAlgebra.basis c hc a) v hv
27   · intro h x v hv
28     rw [← (TwistedAlgebra.basis c hc).sum_repr x]
29     simp only [map_sum, map_smul, TwistedAction.action_basis,
30       LinearMap.sum_apply, LinearMap.smul_apply]
31     exact S.sum_mem fun a _ => S.smul_mem _ (h a v hv)
32 
33 /-- The actual operator irreducibility criterion gives a simple algebra module. -/
34 theorem simpleModule [Nontrivial V]
35     (hIrr : ∀ S : Submodule ℂ V, (∀ a v, v ∈ S → T a v ∈ S) → S = ⊥ ∨ S = ⊤) :
36     IsSimpleModule (TwistedAlgebra.Algebra c hc)
37       (Space (B := ↥(TwistedAlgebra.Algebra c hc)) (TwistedAction.action c hc T hOne hMul)) := by
38   apply (simple_iff (B := ↥(TwistedAlgebra.Algebra c hc)) _).2
39   exact ⟨inferInstance, fun S hS => hIrr S ((stable_iff c hc T hOne hMul S).1 hS)⟩
40 
41 variable (hnd : radical c = ⊥) [Nontrivial V]
42 variable (hIrr : ∀ S : Submodule ℂ V, (∀ a v, v ∈ S → T a v ∈ S) → S = ⊥ ∨ S = ⊤)
43 
44 include c hc T hOne hMul hnd hIrr
45 
46 /-- Finite dimensionality of the actual operator space follows from irreducibility. -/
47 theorem finiteDimensional : FiniteDimensional ℂ V := by
48   let φ := TwistedAction.action c hc T hOne hMul
49   let : IsSimpleModule (TwistedAlgebra.Algebra c hc)
50       (Space (B := ↥(TwistedAlgebra.Algebra c hc)) φ) := simpleModule c hc T hOne hMul hIrr
51   let : FiniteDimensional ℂ (Space (B := ↥(TwistedAlgebra.Algebra c hc)) φ) :=
52     TwistedModules.finiteDimensional c hc hnd _
53   exact FiniteDimensional.of_injective
54     (AlgebraActionModule.equiv (B := ↥(TwistedAlgebra.Algebra c hc)) φ).symm.toLinearMap
55     (AlgebraActionModule.equiv (B := ↥(TwistedAlgebra.Algebra c hc)) φ).symm.injective
56 
57 /-- The square of the actual operator-space dimension equals the group order. -/
58 theorem finrank_sq : Module.finrank ℂ V ^ 2 = Fintype.card A := by
59   let φ := TwistedAction.action c hc T hOne hMul
60   let : IsSimpleModule (TwistedAlgebra.Algebra c hc)
61       (Space (B := ↥(TwistedAlgebra.Algebra c hc)) φ) := simpleModule c hc T hOne hMul hIrr
62   rw [← (AlgebraActionModule.equiv (B := ↥(TwistedAlgebra.Algebra c hc)) φ).finrank_eq]
63   exact TwistedModules.finrank_sq c hc hnd _
64 
65 /-- The source packet dimension, derived for the actual operator space. -/
66 theorem finrank_sqrt : Module.finrank ℂ V = Nat.sqrt (Fintype.card A) := by
67   rw [← finrank_sq c hc T hOne hMul hnd hIrr, Nat.sqrt_eq']
68 
69 omit hIrr in
70 /-- Simplicity forces injectivity of this action map. -/
71 theorem action_injective : Function.Injective (TwistedAction.action c hc T hOne hMul) := by
72   let : IsSimpleRing (TwistedAlgebra.Algebra c hc) := TwistedSimple.isSimpleRing c hc hnd
73   exact RingHom.injective (R := ↥(TwistedAlgebra.Algebra c hc))
74     (TwistedAction.action c hc T hOne hMul).toRingHom
75 
76 /-- Equal dimensions and injectivity prove surjectivity of this action map. -/
77 theorem action_surjective : Function.Surjective (TwistedAction.action c hc T hOne hMul) := by
78   let : FiniteDimensional ℂ V := finiteDimensional c hc T hOne hMul hnd hIrr
79   have hd : Module.finrank ℂ (TwistedAlgebra.Algebra c hc) =
80       Module.finrank ℂ (Module.End ℂ V) := by
81     rw [TwistedAlgebra.finrank_eq_card, Module.finrank_linearMap, ← pow_two,
82       finrank_sq c hc T hOne hMul hnd hIrr]
83   let F : (TwistedAlgebra.Algebra c hc) →ₗ[ℂ] Module.End ℂ V :=
84     (TwistedAction.action c hc T hOne hMul).toLinearMap
85   have hf : Function.Injective F := action_injective c hc T hOne hMul hnd
86   change Function.Surjective F
87   exact (LinearMap.injective_iff_surjective_of_finrank_eq_finrank
88     (K := ℂ) (V := ↥(TwistedAlgebra.Algebra c hc)) (V₂ := Module.End ℂ V)
89     hd (f := F)).1 hf
90 
91 /-- Bijectivity belongs to the literal action homomorphism. -/
92 theorem action_bijective : Function.Bijective (TwistedAction.action c hc T hOne hMul) :=
93   ⟨action_injective c hc T hOne hMul hnd, action_surjective c hc T hOne hMul hnd hIrr⟩
94 
95 /-- The actual action, bundled as an algebra equivalence. -/
96 def actionEquiv : TwistedAlgebra.Algebra c hc ≃ₐ[ℂ] Module.End ℂ V :=
97   AlgEquiv.ofBijective (TwistedAction.action c hc T hOne hMul)
98     (action_bijective c hc T hOne hMul hnd hIrr)
99 
100 @[simp] theorem actionEquiv_apply (x : TwistedAlgebra.Algebra c hc) :
101     actionEquiv c hc T hOne hMul hnd hIrr x = TwistedAction.action c hc T hOne hMul x := rfl
102 
103 @[simp] theorem actionEquiv_basis (a : A) :
104     actionEquiv c hc T hOne hMul hnd hIrr (TwistedAlgebra.basis c hc a) = T a :=
105   TwistedAction.action_basis c hc T hOne hMul a
106 
107 end PaperXI.TwistedActionEquivalence

Back to source controls