CentralExtensionExistence.lean

1 import PaperXI.CentralExtensionUniqueness
2 import PaperXI.CentralCharacterRepresentation
3 
4 /-! Existence is obtained from an actual simple ideal of the constructed
5 twisted algebra, then the reverse action construction. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CentralExtensionExistence
9 open CentralExtension CentralCharacter CocycleCommutator
10 
11 variable {Z H A : Type*} [CommGroup Z] [Group H] [CommGroup A] [Fintype A]
12 
13 set_option backward.isDefEq.respectTransparency false in
14 /-- There exists an actual irreducible representation with the prescribed
15 central action and square-root dimension. -/
16 theorem exists_irreducible (D : Datum Z H A) (ζ : Z →* ℂˣ)
17     (hnd : radical (scalarCocycle D ζ) = ⊥) :
18     let B : Type _ := CentralCharacter.Algebra D ζ
19     letI : Ring B := inferInstance
20     letI : Algebra ℂ B := inferInstance
21     ∃ I : Ideal B, ∃ σ : Representation ℂ H I,
22       Representation.IsIrreducible σ ∧
23       (∀ z, σ (D.i z) = (ζ z : ℂ) • (LinearMap.id : Module.End ℂ I)) ∧
24       Module.finrank ℂ I = Nat.sqrt (Fintype.card A) := by
25   let B : Type _ := CentralCharacter.Algebra D ζ
26   let : Ring B := inferInstance
27   let : Algebra ℂ B := inferInstance
28   let : IsSimpleRing B :=
29     TwistedSimple.isSimpleRing (scalarCocycle D ζ) (normalized_scalarCocycle D ζ) hnd
30   obtain ⟨I, hI⟩ := SimpleModuleClassification.exists_simple_ideal B
31   let : IsSimpleModule B I := hI
32   let φ : B →ₐ[ℂ] Module.End ℂ I := Algebra.lsmul ℂ ℂ I (A := B)
33   let σ := ofAlgebraAction (W := I) D ζ φ
34   have hc : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id := ofAlgebraAction_central (W := I) D ζ φ
35   have hs : IsSimpleModule B (AlgebraActionModule.Space (B := B) φ) :=
36     (AlgebraActionModule.ofModule_simple_iff (B := B) (W := I)).mpr hI
37   have hirr : Representation.IsIrreducible σ :=
38     (ofAlgebraAction_irreducible_iff (W := I) D ζ φ).mpr hs
39   have hd : Module.finrank ℂ I = Nat.sqrt (Fintype.card A) :=
40     TwistedModules.finrank_sqrt (scalarCocycle D ζ) (normalized_scalarCocycle D ζ) hnd I
41   exact ⟨I, σ, hirr, hc, hd⟩
42 
43 end PaperXI.CentralExtensionExistence

Back to source controls