OddPhase.lean

1 import Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
2 import Mathlib.LinearAlgebra.Charpoly.Basic
3 import Mathlib.Tactic
4 
5 /-! Determinant-defined finite-field phases. These declarations do not identify
6 the phase with a Weil trace or assume any Weil normalization theorem. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.OddPhase
10 
11 variable {p : ℕ} [Fact p.Prime]
12 variable {V : Type*} [AddCommGroup V] [Module (ZMod p) V]
13 
14 /-- The actual difference between an automorphism and the identity. -/
15 def difference (g : V ≃ₗ[ZMod p] V) : Module.End (ZMod p) V := g.toLinearMap - 1
16 
17 @[simp] theorem difference_apply (g : V ≃ₗ[ZMod p] V) (v : V) :
18     difference g v = g v - v := rfl
19 
20 /-- Fixed-point-free means that there is no nonzero fixed vector. -/
21 def FixedPointFree (g : V ≃ₗ[ZMod p] V) : Prop := ∀ v, g v = v → v = 0
22 
23 theorem fixedPointFree_iff_ker (g : V ≃ₗ[ZMod p] V) :
24     FixedPointFree g ↔ LinearMap.ker (difference g) = ⊥ := by
25   rw [LinearMap.ker_eq_bot']
26   simp only [FixedPointFree, difference_apply, sub_eq_zero]
27 
28 theorem fixedPointFree_iff_injective (g : V ≃ₗ[ZMod p] V) :
29     FixedPointFree g ↔ Function.Injective (difference g) := by
30   rw [fixedPointFree_iff_ker, LinearMap.ker_eq_bot]
31 
32 section FiniteDimensional
33 variable [FiniteDimensional (ZMod p) V]
34 
35 theorem fixedPointFree_iff_bijective (g : V ≃ₗ[ZMod p] V) :
36     FixedPointFree g ↔ Function.Bijective (difference g) := by
37   rw [fixedPointFree_iff_injective]
38   exact ⟨fun h => ⟨h, LinearMap.injective_iff_surjective.mp h⟩, fun h => h.1⟩
39 
40 theorem fixedPointFree_iff_det_ne_zero (g : V ≃ₗ[ZMod p] V) :
41     FixedPointFree g ↔ LinearMap.det (difference g) ≠ 0 := by
42   rw [fixedPointFree_iff_ker, ne_eq, LinearMap.det_eq_zero_iff_ker_ne_bot, not_not]
43 
44 /-- The difference is an actual linear equivalence under the fixed-point-free hypothesis. -/
45 def differenceEquiv (g : V ≃ₗ[ZMod p] V) (hg : FixedPointFree g) : V ≃ₗ[ZMod p] V :=
46   LinearEquiv.ofBijective (difference g) ((fixedPointFree_iff_bijective g).mp hg)
47 
48 @[simp] theorem differenceEquiv_apply (g : V ≃ₗ[ZMod p] V) (hg : FixedPointFree g) (v : V) :
49     differenceEquiv g hg v = g v - v := rfl
50 
51 /-- The source determinant phase. Its trace interpretation is a separate external fact. -/
52 def phase (g : V ≃ₗ[ZMod p] V) : ℤ :=
53   quadraticChar (ZMod p) (-1) ^ (Module.finrank (ZMod p) V / 2) *
54     quadraticChar (ZMod p) (LinearMap.det (difference g))
55 
56 theorem phase_sq_one (g : V ≃ₗ[ZMod p] V) (hg : FixedPointFree g) : phase g ^ 2 = 1 := by
57   rw [phase, mul_pow, ← pow_mul, Nat.mul_comm _ 2, pow_mul]
58   rw [quadraticChar_sq_one (neg_ne_zero.mpr one_ne_zero), one_pow,
59     quadraticChar_sq_one ((fixedPointFree_iff_det_ne_zero g).mp hg), one_mul]
60 
61 theorem phase_sign (g : V ≃ₗ[ZMod p] V) (hg : FixedPointFree g) :
62     phase g = 1 ∨ phase g = -1 := sq_eq_one_iff.mp (phase_sq_one g hg)
63 
64 theorem phase_ne_zero (g : V ≃ₗ[ZMod p] V) (hg : FixedPointFree g) : phase g ≠ 0 := by
65   rcases phase_sign g hg with h | h <;> simp [h]
66 
67 omit [FiniteDimensional (ZMod p) V] in
68 /-- The zero space has phase one, including its vacuous fixed-point-free condition. -/
69 theorem phase_zero_space [Subsingleton V] (g : V ≃ₗ[ZMod p] V) : phase g = 1 := by
70   have hg : difference g = 1 := Subsingleton.elim _ _
71   simp [phase, hg, Module.finrank_zero_of_subsingleton]
72 
73 omit [FiniteDimensional (ZMod p) V] in
74 theorem fixedPointFree_zero_space [Subsingleton V] (g : V ≃ₗ[ZMod p] V) : FixedPointFree g :=
75   fun v _ => Subsingleton.elim v 0
76 
77 
78 /-- Outside the fixed-point-free domain, the determinant-defined extension of
79 the phase is zero. This is not a formula for the full Weil trace there. -/
80 theorem phase_eq_zero_iff (g : V ≃ₗ[ZMod p] V) : phase g = 0 ↔ ¬FixedPointFree g := by
81   have hneg : quadraticChar (ZMod p) (-1) ≠ 0 := by
82     rw [ne_eq, quadraticChar_eq_zero_iff]
83     exact neg_ne_zero.mpr one_ne_zero
84   rw [phase, mul_eq_zero]
85   simp only [pow_ne_zero _ hneg, false_or, quadraticChar_eq_zero_iff,
86     fixedPointFree_iff_det_ne_zero, not_not]
87 
88 end FiniteDimensional
89 end PaperXI.OddPhase

Back to source controls