OddPhaseTransport.lean

1 import PaperXI.OddPhase
2 
3 /-! Actual conjugacy and determinant-square comparisons of the determinant phase. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperXI.OddPhase
7 
8 variable {p : ℕ} [Fact p.Prime]
9 variable {V W : Type*} [AddCommGroup V] [Module (ZMod p) V]
10 variable [AddCommGroup W] [Module (ZMod p) W]
11 
12 /-- Conjugating the actual action also conjugates its difference from the identity. -/
13 theorem difference_intertwines (g : V ≃ₗ[ZMod p] V) (h : W ≃ₗ[ZMod p] W)
14     (e : V ≃ₗ[ZMod p] W) (he : ∀ v, e (g v) = h (e v)) (v : V) :
15     e (difference g v) = difference h (e v) := by
16   simp only [difference_apply, map_sub, he]
17 
18 theorem difference_conjugacy (g : V ≃ₗ[ZMod p] V) (h : W ≃ₗ[ZMod p] W)
19     (e : V ≃ₗ[ZMod p] W) (he : ∀ v, e (g v) = h (e v)) :
20     difference h = e.toLinearMap.comp ((difference g).comp e.symm.toLinearMap) := by
21   ext w
22   have hh := difference_intertwines g h e he (e.symm w)
23   simpa using hh.symm
24 
25 /-- Fixed-point-freeness is preserved under the supplied actual conjugacy. -/
26 theorem fixedPointFree_conjugacy (g : V ≃ₗ[ZMod p] V) (h : W ≃ₗ[ZMod p] W)
27     (e : V ≃ₗ[ZMod p] W) (he : ∀ v, e (g v) = h (e v)) :
28     FixedPointFree g ↔ FixedPointFree h := by
29   constructor
30   · intro hg w hw
31     have hgw : g (e.symm w) = e.symm w := by
32       apply e.injective
33       simpa only [he, e.apply_symm_apply] using hw
34     have hzero := congrArg e (hg (e.symm w) hgw)
35     simpa using hzero
36   · intro hh v hv
37     apply e.injective
38     have hev : h (e v) = e v := by rw [← he, hv]
39     simpa using hh (e v) hev
40 
41 /-- Determinants of the actual differences agree under conjugacy. -/
42 theorem determinant_conjugacy (g : V ≃ₗ[ZMod p] V) (h : W ≃ₗ[ZMod p] W)
43     (e : V ≃ₗ[ZMod p] W) (he : ∀ v, e (g v) = h (e v)) :
44     LinearMap.det (difference h) = LinearMap.det (difference g) := by
45   rw [difference_conjugacy g h e he]
46   exact LinearMap.det_conj (difference g) e
47 
48 /-- Source 12.3: invariance under actual symplectic conjugacy follows from the
49 stronger invariance under every actual linear conjugacy. -/
50 theorem conjugacy (g : V ≃ₗ[ZMod p] V) (h : W ≃ₗ[ZMod p] W)
51     (e : V ≃ₗ[ZMod p] W) (he : ∀ v, e (g v) = h (e v)) : phase g = phase h := by
52   rw [phase, phase, determinant_conjugacy g h e he, e.finrank_eq]
53 
54 /-- A nonzero square witness for the actual determinants gives the phase-only
55 comparison. No isometry or equivalence of representations is concluded. -/
56 theorem square_class (g : V ≃ₗ[ZMod p] V) (h : W ≃ₗ[ZMod p] W)
57     (hdim : Module.finrank (ZMod p) V / 2 = Module.finrank (ZMod p) W / 2)
58     (u : ZMod p) (hu : u ≠ 0)
59     (hdet : LinearMap.det (difference h) = u ^ 2 * LinearMap.det (difference g)) :
60     phase g = phase h := by
61   simp only [phase, hdim, hdet, map_mul, quadraticChar_sq_one' hu, one_mul]
62 
63 /-- An existential square-class witness suffices for the same actual phase comparison. -/
64 theorem square_class_of_exists (g : V ≃ₗ[ZMod p] V) (h : W ≃ₗ[ZMod p] W)
65     (hdim : Module.finrank (ZMod p) V / 2 = Module.finrank (ZMod p) W / 2)
66     (hdet : ∃ u : ZMod p, u ≠ 0 ∧
67       LinearMap.det (difference h) = u ^ 2 * LinearMap.det (difference g)) :
68     phase g = phase h := by
69   obtain ⟨u, hu, hdet⟩ := hdet
70   exact square_class g h hdim u hu hdet
71 
72 end PaperXI.OddPhase

Back to source controls