HeisenbergRepresentation.lean

1 import PaperXI.HeisenbergGroup
2 import PaperXI.SchrodingerOperator
3 import PaperXI.SchrodingerIrreducible
4 
5 /-! The actual finite Schrödinger representation of the Heisenberg group,
6 its invertible operators, central character, and irreducibility. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.Heisenberg
10 
11 variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]
12 
13 /-- The manuscript operator formula is a representation of the actual group. -/
14 def representation (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0) :
15     Representation ℂ (Element K X) (X → ℂ) where
16   toFun a := Schrodinger.operator ψ a.position a.frequency a.central
17   map_one' := Schrodinger.operator_one ψ
18   map_mul' a b := (Schrodinger.operator_mul ψ h2 a.position b.position
19     a.frequency b.frequency a.central b.central).symm
20 
21 @[simp] theorem representation_apply (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
22     (a : Element K X) (f : X → ℂ) (u : X) :
23     representation ψ h2 a f u =
24       ψ (a.central + a.frequency u + (2 : K)⁻¹ * a.frequency a.position) *
25         f (u + a.position) := rfl
26 
27 /-- The same representation with its values bundled in the general linear group. -/
28 def representationGL (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0) :
29     Element K X →* Units (Module.End ℂ (X → ℂ)) :=
30   (representation ψ h2).asGroupHom
31 
32 @[simp] theorem representationGL_coe (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
33     (a : Element K X) :
34     (representationGL ψ h2 a : Module.End ℂ (X → ℂ)) = representation ψ h2 a :=
35   Representation.asGroupHom_apply _ a
36 
37 /-- Every Schrödinger operator is invertible. -/
38 theorem representation_isUnit (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
39     (a : Element K X) : IsUnit (representation ψ h2 a) := by
40   rw [← representationGL_coe ψ h2 a]
41   exact (representationGL ψ h2 a).isUnit
42 
43 theorem central_action (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0) (z : K) :
44     representation ψ h2 (centralElement (X := X) z) = ψ z • LinearMap.id :=
45   Schrodinger.operator_central ψ z
46 
47 theorem translation_action (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0) (x : X) :
48     representation ψ h2 (translationElement (K := K) x) = Schrodinger.translation x :=
49   Schrodinger.operator_translation ψ x
50 
51 theorem modulation_action (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
52     (ξ : Module.Dual K X) :
53     representation ψ h2 (modulationElement ξ) = Schrodinger.modulation ψ ξ :=
54   Schrodinger.operator_modulation ψ ξ
55 
56 /-- The representation is irreducible for every nontrivial central character,
57 including the one-dimensional function space when `X` is zero-dimensional. -/
58 theorem irreducible [Fintype X] (ψ : AddChar K ℂ) (hψ : ψ ≠ 1)
59     (h2 : (2 : K) ≠ 0) : Representation.IsIrreducible (representation (X := X) ψ h2) := by
60   apply SchrodingerIrreducible.irreducible_of_actions ψ hψ
61   · intro x
62     refine ⟨translationElement (K := K) x, ?_⟩
63     intro f u
64     rw [translation_action]
65     rfl
66   · intro ξ
67     refine ⟨modulationElement ξ, ?_⟩
68     intro f u
69     rw [modulation_action]
70     rfl
71 
72 end PaperXI.Heisenberg

Back to source controls