HeisenbergSourceProjector.lean

1 import PaperXI.HeisenbergSource
2 import PaperXI.HeisenbergSelector
3 import PaperXI.HeisenbergProjector
4 
5 /-! Source propositions 7.5 and 7.6 for the canonical odd-prime model.
6 The finite enumeration of each isotropic subspace is constructed here. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.HeisenbergSourceProjector
10 open HeisenbergForm HeisenbergGeometry
11 open scoped Classical BigOperators
12 
13 variable {p : ℕ} [Fact p.Prime]
14 variable {X : Type*} [AddCommGroup X] [Module (ZMod p) X] [Fintype X]
15   [FiniteDimensional (ZMod p) X]
16 
17 def projector (hp : p ≠ 2) (L : Submodule (ZMod p) (X × Module.Dual (ZMod p) X))
18     (hL : IsIsotropic form L) : Module.End ℂ (X → ℂ) := by
19   let : Finite L := Module.finite_of_finite (ZMod p)
20   let : Fintype L := Fintype.ofFinite L
21   exact HeisenbergProjector.projector (K := ZMod p) ZMod.stdAddChar (HeisenbergPrime.two_ne_zero hp) L hL
22 
23 omit [Fintype X] in
24 theorem idempotent (hp : p ≠ 2)
25     (L : Submodule (ZMod p) (X × Module.Dual (ZMod p) X)) (hL : IsIsotropic form L) :
26     (projector hp L hL).comp (projector hp L hL) = projector hp L hL := by
27   unfold projector
28   let : Finite L := Module.finite_of_finite (ZMod p)
29   let : Fintype L := Fintype.ofFinite L
30   exact HeisenbergProjector.idempotent (K := ZMod p) (X := X) ZMod.stdAddChar
31     (HeisenbergPrime.two_ne_zero hp) L hL
32 
33 omit [Fintype X] in
34 theorem range_eq_invariants (hp : p ≠ 2)
35     (L : Submodule (ZMod p) (X × Module.Dual (ZMod p) X)) (hL : IsIsotropic form L) :
36     LinearMap.range (projector hp L hL) =
37       Representation.invariants (G := Multiplicative L)
38         (HeisenbergProjector.restriction ZMod.stdAddChar
39           (HeisenbergPrime.two_ne_zero hp) L hL) := by
40   unfold projector
41   let : Finite L := Module.finite_of_finite (ZMod p)
42   let : Fintype L := Fintype.ofFinite L
43   exact HeisenbergProjector.range_eq_invariants (K := ZMod p) (X := X) ZMod.stdAddChar
44     (HeisenbergPrime.two_ne_zero hp) L hL
45 
46 theorem self_adjoint (hp : p ≠ 2)
47     (L : Submodule (ZMod p) (X × Module.Dual (ZMod p) X)) (hL : IsIsotropic form L)
48     (f g : X → ℂ) :
49     TranslationAverage.pairing (projector hp L hL f) g =
50       TranslationAverage.pairing f (projector hp L hL g) := by
51   unfold projector
52   let : Finite L := Module.finite_of_finite (ZMod p)
53   let : Fintype L := Fintype.ofFinite L
54   exact HeisenbergProjector.self_adjoint (K := ZMod p) (X := X) ZMod.stdAddChar
55     (HeisenbergPrime.two_ne_zero hp) L hL f g
56 
57 theorem residual_orthogonal (hp : p ≠ 2)
58     (L : Submodule (ZMod p) (X × Module.Dual (ZMod p) X)) (hL : IsIsotropic form L)
59     (f : X → ℂ) {g : X → ℂ} (hg : g ∈ LinearMap.range (projector hp L hL)) :
60     TranslationAverage.pairing (f - projector hp L hL f) g = 0 := by
61   unfold projector
62   let : Finite L := Module.finite_of_finite (ZMod p)
63   let : Fintype L := Fintype.ofFinite L
64   exact HeisenbergProjector.residual_orthogonal (K := ZMod p) (X := X) ZMod.stdAddChar
65     (HeisenbergPrime.two_ne_zero hp) L hL f hg
66 
67 omit [Fintype X] [FiniteDimensional (ZMod p) X] in
68 theorem lift_central_iff_identity (hp : p ≠ 2)
69     (L : Submodule (ZMod p) (X × Module.Dual (ZMod p) X)) (hL : IsIsotropic form L)
70     (a : Multiplicative L) :
71     HeisenbergProjector.liftHom L hL a ∈ Subgroup.center (Heisenberg.Element (ZMod p) X) ↔
72       a = 1 := by
73   rw [HeisenbergCenter.mem_center_iff (HeisenbergPrime.two_ne_zero hp)]
74   exact HeisenbergSelector.coordinates_zero_iff L a
75 
76 theorem position_range (hp : p ≠ 2) :
77     LinearMap.range (projector (X := X) hp HeisenbergProjector.positionSpace
78       HeisenbergProjector.position_isotropic) = TranslationAverage.constantSubmodule := by
79   unfold projector
80   dsimp only
81   have he : Fintype.ofFinite (HeisenbergProjector.positionSpace (K := ZMod p) (X := X)) =
82       HeisenbergProjector.positionFintype := Subsingleton.elim _ _
83   rw [he]
84   exact HeisenbergProjector.position_range_eq
85     (K := ZMod p) (X := X) ZMod.stdAddChar (HeisenbergPrime.two_ne_zero hp)
86 
87 theorem position_rank_one (hp : p ≠ 2) :
88     Module.finrank ℂ (LinearMap.range (projector (X := X) hp HeisenbergProjector.positionSpace
89       HeisenbergProjector.position_isotropic)) = 1 := by
90   rw [position_range]
91   have h := HeisenbergProjector.position_rank_one
92     (K := ZMod p) (X := X) ZMod.stdAddChar (HeisenbergPrime.two_ne_zero hp)
93   rw [HeisenbergProjector.position_range_eq] at h
94   exact h
95 
96 
97 theorem maximal_rank_one (hp : p ≠ 2)
98     (L : Submodule (ZMod p) (X × Module.Dual (ZMod p) X))
99     (hL : IsMaximalIsotropic form L) :
100     Module.finrank ℂ (LinearMap.range (projector hp L hL.1)) = 1 := by
101   unfold projector
102   let : Finite L := Module.finite_of_finite (ZMod p)
103   let : Fintype L := Fintype.ofFinite L
104   exact HeisenbergSelector.maximal_rank_one (K := ZMod p) (X := X) HeisenbergPrime.character_nontrivial
105     (HeisenbergPrime.two_ne_zero hp) L hL
106 
107 theorem maximal_fixed_line (hp : p ≠ 2)
108     (L : Submodule (ZMod p) (X × Module.Dual (ZMod p) X))
109     (hL : IsMaximalIsotropic form L) :
110     Module.finrank ℂ (Representation.invariants (G := Multiplicative L)
111       (HeisenbergProjector.restriction ZMod.stdAddChar
112         (HeisenbergPrime.two_ne_zero hp) L hL.1)) = 1 := by
113   let : Finite L := Module.finite_of_finite (ZMod p)
114   let : Fintype L := Fintype.ofFinite L
115   exact HeisenbergSelector.maximal_fixed_line (K := ZMod p) (X := X) HeisenbergPrime.character_nontrivial
116     (HeisenbergPrime.two_ne_zero hp) L hL
117 
118 end PaperXI.HeisenbergSourceProjector

Back to source controls