AbstractHeisenbergExtension.lean

1 import PaperXI.AbstractHeisenberg
2 import PaperXI.CentralExtensionCocycle
3 import PaperXI.SymplecticCentralExtension
4 
5 /-! The actual commutator of the abstract odd-characteristic Heisenberg extension
6 is the supplied alternating form, independently of the chosen quotient section. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.AbstractHeisenberg
10 
11 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
12 variable (b : LinearMap.BilinForm K V)
13 
14 /-- The abstract symplectic pairing is the actual central preimage of the group commutator. -/
15 theorem centralCommutator_eq (hb : b.IsAlt) (h2 : (2 : K) ≠ 0) (h k : Element b) :
16     CentralExtension.centralCommutator (datum b) h k =
17       Multiplicative.ofAdd (b h.vector k.vector) := by
18   apply (datum b).i_injective
19   rw [CentralExtension.i_centralCommutator, commutator b hb h2]
20   rfl
21 
22 /-- Any central character evaluates the scalar cocycle commutator through the actual form. -/
23 theorem scalar_commutator (hb : b.IsAlt) (h2 : (2 : K) ≠ 0)
24     (ζ : Multiplicative K →* ℂˣ) (v w : Multiplicative V) :
25     CocycleCommutator.commutator (CentralExtension.scalarCocycle (datum b) ζ) v w =
26       ζ (Multiplicative.ofAdd (b v.toAdd w.toAdd)) := by
27   have h := CentralExtension.scalar_commutator (datum b) ζ
28     (⟨v.toAdd, 0⟩ : Element b) (⟨w.toAdd, 0⟩ : Element b)
29   simpa [centralCommutator_eq b hb h2] using h
30 
31 /-- The nontrivial additive character detects the supplied abstract symplectic form.
32 No faithfulness of the character, coordinate identification, or finite target is assumed. -/
33 theorem scalar_radical_eq_bot (hb : b.IsAlt) (h2 : (2 : K) ≠ 0)
34     (hsep : b.SeparatingLeft) (ψ : AddChar K ℂ) (hψ : ψ ≠ 1)
35     (ζ : Multiplicative K →* ℂˣ)
36     (hζ : ∀ t : K, (ζ (Multiplicative.ofAdd t) : ℂ) = ψ t) :
37     CocycleCommutator.radical (CentralExtension.scalarCocycle (datum b) ζ) = ⊥ := by
38   apply SymplecticCentralExtension.radical_eq_bot (datum b) b hsep _ ψ hψ ζ hζ
39   intro h k
40   simpa using centralCommutator_eq b hb h2 h k
41 
42 /-- Scalar nondegeneracy for the canonical unit-valued form of the given additive character. -/
43 theorem scalar_radical_eq_bot_scalarCharacter (hb : b.IsAlt) (h2 : (2 : K) ≠ 0)
44     (hsep : b.SeparatingLeft) (ψ : AddChar K ℂ) (hψ : ψ ≠ 1) :
45     CocycleCommutator.radical (CentralExtension.scalarCocycle (datum b)
46       (SymplecticCentralExtension.scalarCharacter ψ)) = ⊥ :=
47   scalar_radical_eq_bot b hb h2 hsep ψ hψ
48     (SymplecticCentralExtension.scalarCharacter ψ)
49     (SymplecticCentralExtension.scalarCharacter_ofAdd ψ)
50 
51 /-- The distinguished scalar subgroup is proved to be the full center. -/
52 theorem center_eq_inclusion_range (hb : b.IsAlt) (h2 : (2 : K) ≠ 0)
53     (hsep : b.SeparatingLeft) (ψ : AddChar K ℂ) (hψ : ψ ≠ 1) :
54     Subgroup.center (Element b) = (inclusion b).range :=
55   CentralExtension.center_eq_range (datum b) (SymplecticCentralExtension.scalarCharacter ψ)
56     (scalar_radical_eq_bot_scalarCharacter b hb h2 hsep ψ hψ)
57 
58 end PaperXI.AbstractHeisenberg

Back to source controls