SymplecticCentralExtension.lean

1 import PaperXI.CentralExtensionStructure
2 import Mathlib.Algebra.Group.AddChar
3 import Mathlib.LinearAlgebra.BilinearForm.Basic
4 import Mathlib.LinearAlgebra.SesquilinearForm.Basic
5 
6 /-! A nontrivial additive character detects every nonzero vector through a
7 left-nondegenerate field-valued bilinear commutator. This supplies scalar
8 nondegeneracy for actual symplectic central extensions in every characteristic. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.SymplecticCentralExtension
12 open PaperXI.CentralExtension PaperXI.CocycleCommutator
13 variable {K V H : Type*} [Field K] [AddCommGroup V] [Module K V] [Group H]
14 
15 /-- An additive character is an honest unit-valued character of the
16 multiplicatively tagged scalar group. -/
17 def scalarCharacter (ψ : AddChar K ℂ) : Multiplicative K →* ℂˣ :=
18   ψ.toMonoidHom.toHomUnits
19 
20 @[simp] theorem scalarCharacter_apply (ψ : AddChar K ℂ) (z : Multiplicative K) :
21     (scalarCharacter ψ z : ℂ) = ψ z.toAdd := rfl
22 
23 @[simp] theorem scalarCharacter_ofAdd (ψ : AddChar K ℂ) (z : K) :
24     (scalarCharacter ψ (Multiplicative.ofAdd z) : ℂ) = ψ z := rfl
25 
26 /-- A merely nontrivial character suffices because every nonzero field-linear
27 functional takes every scalar value. Faithfulness of the character is not assumed. -/
28 theorem character_separating_left (b : LinearMap.BilinForm K V) (hb : b.SeparatingLeft)
29     (ψ : AddChar K ℂ) (hψ : ψ ≠ 1) (v : V)
30     (hv : ∀ w : V, ψ (b v w) = 1) : v = 0 := by
31   apply hb v
32   intro w
33   by_contra hw
34   obtain ⟨t, ht⟩ := AddChar.ne_one_iff.mp hψ
35   have hscale : b v ((t / b v w) • w) = t := by
36     simp only [map_smul, smul_eq_mul]
37     exact div_mul_cancel₀ t hw
38   apply ht
39   rw [← hscale]
40   exact hv ((t / b v w) • w)
41 
42 /-- Actual symplectic commutators and a nontrivial additive character force
43 the scalar cocycle radical to vanish. No division by two or finite-dimensionality
44 assumption occurs; the quotient map is the actual surjective map in the datum. -/
45 theorem radical_eq_bot
46     (D : Datum (Multiplicative K) H (Multiplicative V))
47     (b : LinearMap.BilinForm K V) (hb : b.SeparatingLeft)
48     (hcomm : ∀ h k : H, centralCommutator D h k =
49       Multiplicative.ofAdd (b (D.q h).toAdd (D.q k).toAdd))
50     (ψ : AddChar K ℂ) (hψ : ψ ≠ 1)
51     (ζ : Multiplicative K →* ℂˣ)
52     (hζ : ∀ t : K, (ζ (Multiplicative.ofAdd t) : ℂ) = ψ t) :
53     radical (scalarCocycle D ζ) = ⊥ := by
54   apply (radical_scalarCocycle_eq_bot_iff D ζ).2
55   intro h hh
56   have hv : (D.q h).toAdd = 0 := by
57     apply character_separating_left b hb ψ hψ
58     intro w
59     obtain ⟨k, hk⟩ := D.q_surjective (Multiplicative.ofAdd w)
60     have hscalar := congrArg (fun z : ℂˣ => (z : ℂ)) (hh k)
61     rw [hcomm, hζ, hk] at hscalar
62     exact hscalar
63   exact congrArg Multiplicative.ofAdd hv
64 
65 /-- Canonical unit-valued character formulation of scalar nondegeneracy. -/
66 theorem radical_eq_bot_scalarCharacter
67     (D : Datum (Multiplicative K) H (Multiplicative V))
68     (b : LinearMap.BilinForm K V) (hb : b.SeparatingLeft)
69     (hcomm : ∀ h k : H, centralCommutator D h k =
70       Multiplicative.ofAdd (b (D.q h).toAdd (D.q k).toAdd))
71     (ψ : AddChar K ℂ) (hψ : ψ ≠ 1) :
72     radical (scalarCocycle D (scalarCharacter ψ)) = ⊥ :=
73   radical_eq_bot D b hb hcomm ψ hψ (scalarCharacter ψ) (scalarCharacter_ofAdd ψ)
74 
75 end PaperXI.SymplecticCentralExtension

Back to source controls