HeisenbergSource.lean

1 import PaperXI.HeisenbergPrime
2 import PaperXI.HeisenbergRepresentation
3 import PaperXI.HeisenbergDimension
4 import PaperXI.HeisenbergFinite
5 import PaperXI.HeisenbergCenter
6 import PaperXI.SchrodingerTrace
7 
8 /-! Source propositions 7.2 and 7.3 for odd prime p and the canonical
9 exponential character, with the manuscript's dimension parameter. -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperXI.HeisenbergSource
13 open PaperXI.Heisenberg
14 open scoped Classical
15 
16 variable {p : ℕ} [Fact p.Prime]
17 variable {X : Type*} [AddCommGroup X] [Module (ZMod p) X]
18 
19 def model (hp : p ≠ 2) : Representation ℂ (Element (ZMod p) X) (X → ℂ) :=
20   representation ZMod.stdAddChar (HeisenbergPrime.two_ne_zero hp)
21 
22 theorem model_formula (hp : p ≠ 2) (a : Element (ZMod p) X) (f : X → ℂ) (u : X) :
23     model hp a f u =
24       ZMod.stdAddChar (a.central + a.frequency u + (2 : ZMod p)⁻¹ *
25         a.frequency a.position) * f (u + a.position) := rfl
26 
27 theorem center_character (hp : p ≠ 2) (a : Element (ZMod p) X)
28     (ha : a ∈ Subgroup.center (Element (ZMod p) X)) :
29     model hp a = ZMod.stdAddChar a.central • LinearMap.id := by
30   rw [(HeisenbergCenter.center_eq_centralElement (HeisenbergPrime.two_ne_zero hp) a).mp ha]
31   exact central_action _ _ _
32 
33 theorem model_invertible (hp : p ≠ 2) (a : Element (ZMod p) X) :
34     IsUnit (model hp a) := representation_isUnit _ _ a
35 
36 variable [Fintype X]
37 
38 theorem model_irreducible (hp : p ≠ 2) :
39     Representation.IsIrreducible (model (X := X) hp) :=
40   irreducible _ HeisenbergPrime.character_nontrivial _
41 
42 variable [FiniteDimensional (ZMod p) X]
43 
44 theorem dimension_power : Module.finrank ℂ (X → ℂ) = p ^ Module.finrank (ZMod p) X := by
45   simpa only [Nat.card_zmod] using HeisenbergDimension.finrank_function_pow
46     (K := ZMod p) (X := X)
47 
48 theorem dimension_sqrt : Module.finrank ℂ (X → ℂ) =
49     Nat.sqrt (Nat.card (X × Module.Dual (ZMod p) X)) :=
50   HeisenbergDimension.finrank_function_sqrt
51 
52 theorem character_support (hp : p ≠ 2) (a : Element (ZMod p) X) :
53     LinearMap.trace ℂ (X → ℂ) (model hp a) =
54       if a.position = 0 ∧ a.frequency = 0 then
55         (p : ℂ) ^ Module.finrank (ZMod p) X * ZMod.stdAddChar a.central else 0 := by
56   have hc : Fintype.card X = p ^ Module.finrank (ZMod p) X := by
57     rw [← Nat.card_eq_fintype_card,
58       Module.natCard_eq_pow_finrank (K := ZMod p) (V := X), Nat.card_zmod]
59   simpa only [hc, Nat.cast_pow, model, representation, MonoidHom.coe_mk, OneHom.coe_mk] using
60     SchrodingerTrace.character_support HeisenbergPrime.character_nontrivial
61       a.position a.frequency a.central
62 
63 end PaperXI.HeisenbergSource

Back to source controls