TypeSideUniqueness.lean

1 import PaperXI.TypeSideExtension
2 import PaperXI.CentralExtensionUniqueness
3 
4 /-! Uniqueness and dimension for the original actual type-side actions.
5 Character containment is converted to scalar restriction and quotient
6 descent by proved constructions. The source simple-character structure and
7 nondegenerate pairing remain explicit inputs. The first intertwiner and
8 the representation dimensions are conclusions. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.TypeSideUniqueness
12 
13 open TypeSideDescent TypeSideExtension
14 open scoped IsMulCommutative
15 
16 variable {G V W : Type*} [Group G]
17 variable [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W]
18 
19 /-- Finite dimensionality of the actual representation is derived after
20 descending its proved character kernel to the constructed central extension. -/
21 theorem finiteDimensional (H : Subgroup G) [H.Normal] [IsMulCommutative (G ⧸ H)]
22     [Finite (G ⧸ H)] (θ : H →* ℂˣ) (hθ : Invariant H θ)
23     (hnd : CocycleCommutator.radical
24       (CentralExtension.scalarCocycle (datum H θ hθ) (centralCharacter H θ)) = ⊥)
25     (η : Representation ℂ G V) [Representation.IsIrreducible η]
26     (hcontains : Contains H θ η) : FiniteDimensional ℂ V := by
27   let : Fintype (G ⧸ H) := Fintype.ofFinite _
28   let : Representation.IsIrreducible (representation H θ hθ η hcontains) :=
29     representation_irreducible H θ hθ η hcontains
30   exact CentralExtensionUniqueness.finiteDimensional (datum H θ hθ) (centralCharacter H θ)
31     hnd (representation H θ hθ η hcontains) (representation_central_action H θ hθ η hcontains)
32 
33 /-- The dimension formula is for the original supplied representation space. -/
34 theorem finrank_sqrt (H : Subgroup G) [H.Normal] [IsMulCommutative (G ⧸ H)]
35     [Finite (G ⧸ H)] (θ : H →* ℂˣ) (hθ : Invariant H θ)
36     (hnd : CocycleCommutator.radical
37       (CentralExtension.scalarCocycle (datum H θ hθ) (centralCharacter H θ)) = ⊥)
38     (η : Representation ℂ G V) [Representation.IsIrreducible η]
39     (hcontains : Contains H θ η) :
40     Module.finrank ℂ V = Nat.sqrt (Nat.card (G ⧸ H)) := by
41   let : Fintype (G ⧸ H) := Fintype.ofFinite _
42   let : Representation.IsIrreducible (representation H θ hθ η hcontains) :=
43     representation_irreducible H θ hθ η hcontains
44   simpa only [Nat.card_eq_fintype_card] using
45     CentralExtensionUniqueness.finrank_sqrt (datum H θ hθ) (centralCharacter H θ)
46       hnd (representation H θ hθ η hcontains) (representation_central_action H θ hθ η hcontains)
47 
48 /-- Construct an equivalence of the original actual representations, not
49 merely an equivalence of two separately assumed quotient actions. -/
50 theorem exists_equiv (H : Subgroup G) [H.Normal] [IsMulCommutative (G ⧸ H)]
51     [Finite (G ⧸ H)] (θ : H →* ℂˣ) (hθ : Invariant H θ)
52     (hnd : CocycleCommutator.radical
53       (CentralExtension.scalarCocycle (datum H θ hθ) (centralCharacter H θ)) = ⊥)
54     (η : Representation ℂ G V) (τ : Representation ℂ G W)
55     [Representation.IsIrreducible η] [Representation.IsIrreducible τ]
56     (hη : Contains H θ η) (hτ : Contains H θ τ) :
57     Nonempty (Representation.Equiv η τ) := by
58   let : Fintype (G ⧸ H) := Fintype.ofFinite _
59   let : Representation.IsIrreducible (representation H θ hθ η hη) :=
60     representation_irreducible H θ hθ η hη
61   let : Representation.IsIrreducible (representation H θ hθ τ hτ) :=
62     representation_irreducible H θ hθ τ hτ
63   obtain ⟨U⟩ := CentralExtensionUniqueness.exists_equiv (datum H θ hθ) (centralCharacter H θ)
64     hnd (representation H θ hθ η hη) (representation H θ hθ τ hτ)
65     (representation_central_action H θ hθ η hη) (representation_central_action H θ hθ τ hτ)
66   exact ⟨Representation.Equiv.mk U.toLinearEquiv
67     (fun g => U.toIntertwiningMap.isIntertwining' (QuotientGroup.mk' (characterKernel H θ hθ) g))⟩
68 
69 /-- The first nonzero invertible comparison and its unique unit-scalar
70 ambiguity, on all original group elements and original representation vectors. -/
71 theorem exists_unique_intertwiner (H : Subgroup G) [H.Normal]
72     [IsMulCommutative (G ⧸ H)] [Finite (G ⧸ H)] (θ : H →* ℂˣ) (hθ : Invariant H θ)
73     (hnd : CocycleCommutator.radical
74       (CentralExtension.scalarCocycle (datum H θ hθ) (centralCharacter H θ)) = ⊥)
75     (η : Representation ℂ G V) (τ : Representation ℂ G W)
76     [Representation.IsIrreducible η] [Representation.IsIrreducible τ]
77     (hη : Contains H θ η) (hτ : Contains H θ τ) :
78     ∃ U : V ≃ₗ[ℂ] W, U.toLinearMap ≠ 0 ∧
79       (∀ g v, U (η g v) = τ g (U v)) ∧
80       ∀ T : V ≃ₗ[ℂ] W, (∀ g v, T (η g v) = τ g (T v)) →
81         ∃! c : ℂˣ, ∀ v, T v = (c : ℂ) • U v := by
82   obtain ⟨E⟩ := exists_equiv H θ hθ hnd η τ hη hτ
83   let U := E.toLinearEquiv
84   have hU : ∀ g v, U (η g v) = τ g (U v) :=
85     Representation.IntertwiningMap.isIntertwining η τ E.toIntertwiningMap
86   let : Nontrivial V := GeneratedIrreducibility.nontrivial_space η
87   let : FiniteDimensional ℂ V := finiteDimensional H θ hθ hnd η hη
88   refine ⟨U, ?_, hU, ?_⟩
89   · intro hzero
90     obtain ⟨v, hv⟩ := exists_ne (0 : V)
91     have hz : U v = 0 := LinearMap.congr_fun hzero v
92     exact hv (U.injective (hz.trans U.map_zero.symm))
93   · intro T hT
94     exact SchurScalar.bridge_unique η τ U T hU hT
95 
96 end PaperXI.TypeSideUniqueness

Back to source controls