RestrictedHeisenbergBridge.lean

1 import PaperXI.CentralExtensionComparison
2 import PaperXI.AbstractHeisenbergExtension
3 import PaperXI.SymplecticCentralExtension
4 
5 /-! Source 11.2: the initial bridge between the supplied Heisenberg envelopes.
6 The odd branch constructs the lift on arbitrary abstract symplectic spaces.
7 The dyadic branch retains the supplied isomorphism of actual central
8 extensions. Neither branch assumes an initial intertwiner, scalar-cocycle
9 nondegeneracy, or finite-dimensionality of either representation space. -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperXI.RestrictedHeisenbergBridge
13 
14 open CentralExtension SymplecticCentralExtension
15 variable {K V V' W W' : Type*} [Field K] [Finite K]
16 variable [AddCommGroup V] [Module K V] [FiniteDimensional K V]
17 variable [AddCommGroup V'] [Module K V']
18 variable [AddCommGroup W] [Module ℂ W] [AddCommGroup W'] [Module ℂ W']
19 
20 /-- Odd-characteristic source bridge on arbitrary abstract symplectic spaces.
21 The group lift is constructed from the supplied linear isometry. The
22 nontrivial character and field-valued nondegenerate form supply the scalar
23 nondegeneracy required by the uniqueness theorem. -/
24 theorem odd_source
25     (b : LinearMap.BilinForm K V) (b' : LinearMap.BilinForm K V')
26     (hb : b.IsAlt) (hbn : b.Nondegenerate) (h2 : (2 : K) ≠ 0)
27     (ι : V ≃ₗ[K] V') (hι : ∀ v w, b' (ι v) (ι w) = b v w)
28     (ψ : AddChar K ℂ) (hψ : ψ ≠ 1)
29     (ρ : Representation ℂ (AbstractHeisenberg.Element b) W)
30     (σ : Representation ℂ (AbstractHeisenberg.Element b') W')
31     [Representation.IsIrreducible ρ] [Representation.IsIrreducible σ]
32     (hρ : ∀ z : K, ρ (AbstractHeisenberg.centralElement b z) = ψ z • LinearMap.id)
33     (hσ : ∀ z : K, σ (AbstractHeisenberg.centralElement b' z) = ψ z • LinearMap.id) :
34     ∃ U : W ≃ₗ[ℂ] W', U.toLinearMap ≠ 0 ∧
35       (∀ h w, U (ρ h w) = σ (AbstractHeisenberg.lift b b' ι hι h) (U w)) ∧
36       ∀ T : W ≃ₗ[ℂ] W',
37         (∀ h w, T (ρ h w) = σ (AbstractHeisenberg.lift b b' ι hι h) (T w)) →
38           ∃! c : ℂˣ, ∀ w, T w = (c : ℂ) • U w := by
39   let : Finite V := Module.finite_of_finite K
40   let : Fintype (Multiplicative V) := Fintype.ofFinite _
41   apply CentralExtensionComparison.exists_unique_along (AbstractHeisenberg.datum b)
42     (scalarCharacter ψ)
43     (AbstractHeisenberg.scalar_radical_eq_bot_scalarCharacter b hb h2 hbn.1 ψ hψ)
44     (AbstractHeisenberg.lift b b' ι hι) ρ σ
45   · intro z
46     exact hρ z.toAdd
47   · intro z
48     rw [AbstractHeisenberg.lift_inclusion]
49     exact hσ z.toAdd
50 
51 variable {H H' : Type*} [Group H] [Group H']
52 
53 omit [Module K V'] in
54 /-- The source branch for supplied actual extensions, including residue
55 characteristic two. The actual lift is an input from the compatible dyadic
56 extension data; an alternating form is not used to manufacture that lift.
57 The argument works in every characteristic and never divides by two. -/
58 theorem dyadic_source
59     (D : Datum (Multiplicative K) H (Multiplicative V))
60     (D' : Datum (Multiplicative K) H' (Multiplicative V'))
61     (b : LinearMap.BilinForm K V) (hbn : b.Nondegenerate)
62     (hcomm : ∀ h k : H, centralCommutator D h k =
63       Multiplicative.ofAdd (b (D.q h).toAdd (D.q k).toAdd))
64     (e : H ≃* H') (he : ∀ z : Multiplicative K, e (D.i z) = D'.i z)
65     (ψ : AddChar K ℂ) (hψ : ψ ≠ 1)
66     (ρ : Representation ℂ H W) (σ : Representation ℂ H' W')
67     [Representation.IsIrreducible ρ] [Representation.IsIrreducible σ]
68     (hρ : ∀ z : K, ρ (D.i (Multiplicative.ofAdd z)) = ψ z • LinearMap.id)
69     (hσ : ∀ z : K, σ (D'.i (Multiplicative.ofAdd z)) = ψ z • LinearMap.id) :
70     ∃ U : W ≃ₗ[ℂ] W', U.toLinearMap ≠ 0 ∧
71       (∀ h w, U (ρ h w) = σ (e h) (U w)) ∧
72       ∀ T : W ≃ₗ[ℂ] W', (∀ h w, T (ρ h w) = σ (e h) (T w)) →
73         ∃! c : ℂˣ, ∀ w, T w = (c : ℂ) • U w := by
74   let : Finite V := Module.finite_of_finite K
75   let : Fintype (Multiplicative V) := Fintype.ofFinite _
76   apply CentralExtensionComparison.exists_unique_along D (scalarCharacter ψ)
77     (radical_eq_bot_scalarCharacter D b hbn.1 hcomm ψ hψ) e ρ σ
78   · intro z
79     exact hρ z.toAdd
80   · intro z
81     rw [he]
82     exact hσ z.toAdd
83 
84 end PaperXI.RestrictedHeisenbergBridge

Back to source controls