TensorIrreducible.lean

1 import PaperXI.CentralExtensionUniqueness
2 import Mathlib.LinearAlgebra.Dual.Lemmas
3 import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
4 
5 /-! A dimension criterion for irreducibility of an actual central-character
6 representation. Simplicity proves injectivity of its actual algebra action;
7 the dimension identity then proves surjectivity and irreducibility. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.TensorIrreducible
11 open CentralExtension CentralCharacter CocycleCommutator
12 
13 variable {Z H A W : Type*} [CommGroup Z] [Group H] [CommGroup A] [Fintype A]
14 variable [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W] [Nontrivial W]
15 
16 omit [FiniteDimensional ℂ W] [Nontrivial W] in
17 /-- The square dimension identity for each actual irreducible factor. -/
18 theorem finrank_sq_of_irreducible (D : Datum Z H A) (ζ : Z →* ℂˣ)
19     (hnd : radical (scalarCocycle D ζ) = ⊥)
20     (σ : Representation ℂ H W) [Representation.IsIrreducible σ]
21     (hσ : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id) :
22     Module.finrank ℂ W ^ 2 = Fintype.card A := by
23   let φ := toAlgebraAction D ζ σ hσ
24   let : IsSimpleModule (Algebra D ζ)
25       (AlgebraActionModule.Space (B := ↥(Algebra D ζ)) φ) := simpleModule D ζ σ hσ
26   rw [← (AlgebraActionModule.equiv (B := ↥(Algebra D ζ)) φ).finrank_eq]
27   exact TwistedModules.finrank_sq (scalarCocycle D ζ) (normalized_scalarCocycle D ζ)
28     hnd (AlgebraActionModule.Space (B := ↥(Algebra D ζ)) φ)
29 
30 omit [FiniteDimensional ℂ W] in
31 /-- The simple central-character algebra acts faithfully on every nonzero space. -/
32 theorem action_injective (D : Datum Z H A) (ζ : Z →* ℂˣ)
33     (hnd : radical (scalarCocycle D ζ) = ⊥)
34     (σ : Representation ℂ H W)
35     (hσ : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id) :
36     Function.Injective (toAlgebraAction D ζ σ hσ) := by
37   let : IsSimpleRing (Algebra D ζ) :=
38     TwistedSimple.isSimpleRing (scalarCocycle D ζ) (normalized_scalarCocycle D ζ) hnd
39   exact RingHom.injective (R := ↥(Algebra D ζ)) (toAlgebraAction D ζ σ hσ).toRingHom
40 
41 /-- The required dimension forces this literal action to fill every endomorphism. -/
42 theorem action_surjective (D : Datum Z H A) (ζ : Z →* ℂˣ)
43     (hnd : radical (scalarCocycle D ζ) = ⊥)
44     (σ : Representation ℂ H W)
45     (hσ : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id)
46     (hdim : Module.finrank ℂ W ^ 2 = Fintype.card A) :
47     Function.Surjective (toAlgebraAction D ζ σ hσ) := by
48   have hd : Module.finrank ℂ (Algebra D ζ) = Module.finrank ℂ (Module.End ℂ W) := by
49     rw [TwistedAlgebra.finrank_eq_card, Module.finrank_linearMap, ← pow_two, hdim]
50   let F : Algebra D ζ →ₗ[ℂ] Module.End ℂ W := (toAlgebraAction D ζ σ hσ).toLinearMap
51   have hf : Function.Injective F := action_injective D ζ hnd σ hσ
52   change Function.Surjective F
53   exact (LinearMap.injective_iff_surjective_of_finrank_eq_finrank
54     (K := ℂ) (V := ↥(Algebra D ζ)) (V₂ := Module.End ℂ W) hd (f := F)).1 hf
55 
56 /-- Equality of the Heisenberg dimension and central character is sufficient
57 because the actual action was proved surjective, not because uniqueness was assumed. -/
58 theorem irreducible (D : Datum Z H A) (ζ : Z →* ℂˣ)
59     (hnd : radical (scalarCocycle D ζ) = ⊥)
60     (σ : Representation ℂ H W)
61     (hσ : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id)
62     (hdim : Module.finrank ℂ W ^ 2 = Fintype.card A) :
63     Representation.IsIrreducible σ := by
64   apply RepresentationStability.irreducible_of_stable
65   intro S hS
66   by_cases hbot : S = ⊥
67   · exact Or.inl hbot
68   · right
69     obtain ⟨x, hx, hx0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hbot
70     obtain ⟨f, hf⟩ := Module.Projective.exists_dual_eq_one ℂ hx0
71     apply top_unique
72     intro y _
73     obtain ⟨b, hb⟩ := action_surjective D ζ hnd σ hσ hdim (f.smulRight y)
74     have hmem := (action_stable_iff D ζ σ hσ S).2 hS b x hx
75     rw [hb] at hmem
76     simpa [hf] using hmem
77 
78 end PaperXI.TensorIrreducible

Back to source controls