TypeSideExtension.lean

1 import PaperXI.TypeSideDescent
2 import PaperXI.CentralExtensionCocycle
3 import Mathlib.Algebra.Group.IsCommutative
4 import Mathlib.Algebra.Group.AddChar
5 import Mathlib.LinearAlgebra.BilinearMap
6 
7 /-! The actual type-side central extension, its source commutator formula,
8 and scalar nondegeneracy transferred from a supplied source pairing. These
9 interfaces retain the simple-character facts as explicit inputs. -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperXI.TypeSideExtension
13 
14 open TypeSideDescent
15 open scoped IsMulCommutative
16 
17 variable {G V : Type*} [Group G] [AddCommGroup V] [Module ℂ V]
18 
19 /-- The central quotient is abelian because its actual character is faithful. -/
20 instance centralQuotient_isMulCommutative (H : Subgroup G) (θ : H →* ℂˣ) :
21     IsMulCommutative (H ⧸ θ.ker) :=
22   ⟨⟨fun a b => (centralCharacter_injective H θ) (by simp [map_mul, mul_comm])⟩⟩
23 
24 theorem finite_center (H : Subgroup G) (θ : H →* ℂˣ) [Finite θ.range] :
25     Finite (H ⧸ θ.ker) := inferInstance
26 
27 theorem centralCharacter_ne_one (H : Subgroup G) (θ : H →* ℂˣ) (hθ : θ ≠ 1) :
28     centralCharacter H θ ≠ 1 := by
29   intro heq
30   apply hθ
31   apply MonoidHom.ext
32   intro h
33   exact DFunLike.congr_fun heq (QuotientGroup.mk' θ.ker h)
34 
35 /-- The exact extension formed from the actual source groups and character. -/
36 def datum (H : Subgroup G) [H.Normal] [IsMulCommutative (G ⧸ H)]
37     (θ : H →* ℂˣ) (hθ : Invariant H θ) :
38     CentralExtension.Datum (H ⧸ θ.ker) (G ⧸ characterKernel H θ hθ) (G ⧸ H) where
39   i := centerInclusion H θ hθ
40   q := quotientProjection H θ hθ
41   i_injective := centerInclusion_injective H θ hθ
42   q_surjective := quotientProjection_surjective H θ hθ
43   range_i_eq_ker_q := exact_center_quotient H θ hθ
44   central z h :=
45     ((Subgroup.mem_center_iff.mp (centerInclusion_central H θ hθ ⟨z, rfl⟩)) h).symm
46 
47 /-- Commutators lie in the actual normal subgroup because the quotient is abelian. -/
48 theorem commutator_mem (H : Subgroup G) [H.Normal] [IsMulCommutative (G ⧸ H)]
49     (x y : G) : x * y * x⁻¹ * y⁻¹ ∈ H := by
50   apply (QuotientGroup.eq_one_iff _).mp
51   simp [QuotientGroup.mk_mul, mul_comm, mul_left_comm]
52 
53 /-- The source scalar pairing on actual representatives, namely `θ([x,y])`. -/
54 def characterCommutator (H : Subgroup G) [H.Normal] [IsMulCommutative (G ⧸ H)]
55     (θ : H →* ℂˣ) (x y : G) : ℂˣ :=
56   θ ⟨x * y * x⁻¹ * y⁻¹, commutator_mem H x y⟩
57 
58 /-- The constructed extension cocycle reproduces exactly the source scalar
59 commutator on every pair of actual group representatives. -/
60 theorem scalar_commutator_source (H : Subgroup G) [H.Normal]
61     [IsMulCommutative (G ⧸ H)] (θ : H →* ℂˣ) (hθ : Invariant H θ) (x y : G) :
62     CocycleCommutator.commutator
63       (CentralExtension.scalarCocycle (datum H θ hθ) (centralCharacter H θ))
64       (QuotientGroup.mk' H x) (QuotientGroup.mk' H y) = characterCommutator H θ x y := by
65   let D := datum H θ hθ
66   let q := QuotientGroup.mk' (characterKernel H θ hθ)
67   change CocycleCommutator.commutator (CentralExtension.scalarCocycle D (centralCharacter H θ))
68     (D.q (q x)) (D.q (q y)) = _
69   rw [CentralExtension.scalar_commutator]
70   have hc : CentralExtension.centralCommutator D (q x) (q y) =
71       QuotientGroup.mk' θ.ker ⟨x * y * x⁻¹ * y⁻¹, commutator_mem H x y⟩ := by
72     apply D.i_injective
73     rw [CentralExtension.i_centralCommutator]
74     change q x * q y * (q x)⁻¹ * (q y)⁻¹ = q (x * y * x⁻¹ * y⁻¹)
75     simp
76   rw [hc]
77   rfl
78 
79 /-- A supplied scalar source pairing is the scalar commutator of the actual
80 constructed extension, not merely a pairing on an unrelated quotient. -/
81 theorem scalar_commutator_eq_pairing (H : Subgroup G) [H.Normal]
82     [IsMulCommutative (G ⧸ H)] (θ : H →* ℂˣ) (hθ : Invariant H θ)
83     (b : (G ⧸ H) → (G ⧸ H) → ℂˣ)
84     (hb : ∀ x y, b (QuotientGroup.mk' H x) (QuotientGroup.mk' H y) =
85       characterCommutator H θ x y) (a d : G ⧸ H) :
86     CocycleCommutator.commutator
87       (CentralExtension.scalarCocycle (datum H θ hθ) (centralCharacter H θ)) a d = b a d := by
88   obtain ⟨x, rfl⟩ := QuotientGroup.mk_surjective a
89   obtain ⟨y, rfl⟩ := QuotientGroup.mk_surjective d
90   exact (scalar_commutator_source H θ hθ x y).trans (hb x y).symm
91 
92 /-- Source nondegeneracy is needed after applying the character. No assertion
93 that an arbitrary nontrivial central character is faithful is used here. -/
94 theorem nondegenerate_of_pairing (H : Subgroup G) [H.Normal]
95     [IsMulCommutative (G ⧸ H)] (θ : H →* ℂˣ) (hθ : Invariant H θ)
96     (b : (G ⧸ H) → (G ⧸ H) → ℂˣ)
97     (hb : ∀ x y, b (QuotientGroup.mk' H x) (QuotientGroup.mk' H y) =
98       characterCommutator H θ x y)
99     (hnd : ∀ a, (∀ d, b a d = 1) → a = 1) :
100     CocycleCommutator.radical
101       (CentralExtension.scalarCocycle (datum H θ hθ) (centralCharacter H θ)) = ⊥ := by
102   apply le_antisymm ?_ bot_le
103   intro a ha
104   apply Subgroup.mem_bot.mpr
105   apply hnd a
106   intro d
107   rw [← scalar_commutator_eq_pairing H θ hθ b hb]
108   exact (CocycleCommutator.mem_radical_iff _ a).mp ha d
109 
110 section BilinearSource
111 
112 variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]
113 
114 /-- A nonzero functional is surjective, so composing a nondegenerate
115 bilinear pairing with a nontrivial additive character is still nondegenerate
116 as a scalar pairing. No faithfulness of the additive character is assumed. -/
117 theorem bilinear_character_nondegenerate
118     (β : X →ₗ[K] X →ₗ[K] K)
119     (hβ : ∀ x, (∀ y, β x y = 0) → x = 0)
120     (ψ : AddChar K ℂˣ) (hψ : ψ ≠ 1) (x : X)
121     (hx : ∀ y, ψ (β x y) = 1) : x = 0 := by
122   apply hβ x
123   intro y
124   by_contra hxy
125   have ht : ∃ t : K, ψ t ≠ 1 := by
126     by_contra hn
127     apply hψ
128     apply AddChar.ext
129     intro t
130     exact not_not.mp (not_exists.mp hn t)
131   obtain ⟨t, ht⟩ := ht
132   have heq : β x ((t / β x y) • y) = t := by
133     rw [map_smul, smul_eq_mul, div_mul_cancel₀ t hxy]
134   exact ht (heq ▸ hx ((t / β x y) • y))
135 
136 /-- The source vector-space pairing gives the actual extension's scalar
137 nondegeneracy through an explicit identification of the quotient group. -/
138 theorem nondegenerate_of_bilinear_pairing (H : Subgroup G) [H.Normal]
139     [IsMulCommutative (G ⧸ H)] (θ : H →* ℂˣ) (hθ : Invariant H θ)
140     (e : (G ⧸ H) ≃* Multiplicative X) (β : X →ₗ[K] X →ₗ[K] K)
141     (hβ : ∀ x, (∀ y, β x y = 0) → x = 0)
142     (ψ : AddChar K ℂˣ) (hψ : ψ ≠ 1)
143     (hsource : ∀ x y,
144       ψ (β (e (QuotientGroup.mk' H x)).toAdd (e (QuotientGroup.mk' H y)).toAdd) =
145         characterCommutator H θ x y) :
146     CocycleCommutator.radical
147       (CentralExtension.scalarCocycle (datum H θ hθ) (centralCharacter H θ)) = ⊥ := by
148   apply nondegenerate_of_pairing H θ hθ
149     (fun a d => ψ (β (e a).toAdd (e d).toAdd)) hsource
150   intro a ha
151   have hz : (e a).toAdd = 0 := by
152     apply bilinear_character_nondegenerate β hβ ψ hψ
153     intro y
154     simpa using ha (e.symm (Multiplicative.ofAdd y))
155   apply e.injective
156   simpa using congrArg Multiplicative.ofAdd hz
157 
158 end BilinearSource
159 
160 /-- The supplied irreducible source action, descended through its proved
161 character kernel, has the required action of the constructed extension center. -/
162 theorem representation_central_action (H : Subgroup G) [H.Normal]
163     [IsMulCommutative (G ⧸ H)] (θ : H →* ℂˣ) (hθ : Invariant H θ)
164     (η : Representation ℂ G V) [Representation.IsIrreducible η]
165     (hcontains : Contains H θ η) (z : H ⧸ θ.ker) :
166     representation H θ hθ η hcontains ((datum H θ hθ).i z) =
167       (centralCharacter H θ z : ℂ) • LinearMap.id :=
168   central_action H θ hθ η hcontains z
169 
170 end PaperXI.TypeSideExtension

Back to source controls