MovingPhase.lean

1 import PaperXI.FixedMovingSource
2 import PaperXI.OddPhaseTransport
3 
4 /-! The determinant phase on the actual moving image, with its source
5 validity, conjugacy invariance and square-class comparison. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.MovingPhase
9 open FixedMoving
10 
11 variable {p : ℕ} [Fact p.Prime]
12 variable {V W : Type*} [AddCommGroup V] [Module (ZMod p) V]
13 variable [AddCommGroup W] [Module (ZMod p) W]
14 
15 /-- Source definition 12.7: the phase of the actual restriction to `im(g-1)`. -/
16 def phase (g : V ≃ₗ[ZMod p] V) : ℤ := OddPhase.phase (movingAction g)
17 
18 theorem phase_formula (g : V ≃ₗ[ZMod p] V) :
19     phase g = quadraticChar (ZMod p) (-1) ^ (Module.finrank (ZMod p) (moving g) / 2) *
20       quadraticChar (ZMod p) (LinearMap.det (OddPhase.difference (movingAction g))) := rfl
21 
22 /-- Under the actual source order hypothesis the moving determinant is nonzero. -/
23 theorem determinant_ne_zero [FiniteDimensional (ZMod p) V] (g : V ≃ₗ[ZMod p] V) (horder : Nat.Coprime (orderOf g) p) :
24     LinearMap.det (OddPhase.difference (movingAction g)) ≠ 0 :=
25   (OddPhase.fixedPointFree_iff_det_ne_zero (movingAction g)).mp
26     (source_moving_fixedPointFree g horder)
27 
28 theorem phase_sq_one [FiniteDimensional (ZMod p) V] (g : V ≃ₗ[ZMod p] V) (horder : Nat.Coprime (orderOf g) p) :
29     phase g ^ 2 = 1 := OddPhase.phase_sq_one (movingAction g) (source_moving_fixedPointFree g horder)
30 
31 theorem phase_sign [FiniteDimensional (ZMod p) V] (g : V ≃ₗ[ZMod p] V) (horder : Nat.Coprime (orderOf g) p) :
32     phase g = 1 ∨ phase g = -1 :=
33   OddPhase.phase_sign (movingAction g) (source_moving_fixedPointFree g horder)
34 
35 /-- The moving-phase input is an actual nondegenerate alternating space and a
36 form-preserving fixed-point-free restriction, all derived from the original data. -/
37 theorem source_valid [FiniteDimensional (ZMod p) V] (g : V ≃ₗ[ZMod p] V) (horder : Nat.Coprime (orderOf g) p)
38     (b : LinearMap.BilinForm (ZMod p) V) (hb : b.IsAlt) (hbn : b.Nondegenerate)
39     (hg : ∀ x y, b (g x) (g y) = b x y) :
40     (movingForm g b).IsAlt ∧ (movingForm g b).Nondegenerate ∧
41       (∀ x y : moving g, movingForm g b (movingAction g x) (movingAction g y) = movingForm g b x y) ∧
42       OddPhase.FixedPointFree (movingAction g) ∧
43       LinearMap.det (OddPhase.difference (movingAction g)) ≠ 0 ∧
44       (phase g = 1 ∨ phase g = -1) := by
45   exact ⟨movingForm_alt g b hb,
46     movingForm_nondegenerate_of_isCompl g b hb hbn hg (source_isCompl g horder),
47     movingAction_preserves g b hg, source_moving_fixedPointFree g horder,
48     determinant_ne_zero g horder, phase_sign g horder⟩
49 
50 /-- Actual ambient conjugacy induces conjugacy on the moving images and hence equal phases. -/
51 theorem conjugacy (g : V ≃ₗ[ZMod p] V) (h : W ≃ₗ[ZMod p] W)
52     (e : V ≃ₗ[ZMod p] W) (he : ∀ v, e (g v) = h (e v)) : phase g = phase h :=
53   OddPhase.conjugacy (movingAction g) (movingAction h) (movingEquiv g h e he)
54     (movingEquiv_intertwines g h e he)
55 
56 /-- Equal moving half dimensions and an actual nonzero determinant square witness
57 give equal moving phases. The conclusion is only a scalar phase comparison. -/
58 theorem square_class (g : V ≃ₗ[ZMod p] V) (h : W ≃ₗ[ZMod p] W)
59     (hdim : Module.finrank (ZMod p) (moving g) / 2 = Module.finrank (ZMod p) (moving h) / 2)
60     (u : ZMod p) (hu : u ≠ 0)
61     (hdet : LinearMap.det (OddPhase.difference (movingAction h)) =
62       u ^ 2 * LinearMap.det (OddPhase.difference (movingAction g))) : phase g = phase h :=
63   OddPhase.square_class (movingAction g) (movingAction h) hdim u hu hdet
64 
65 /-- Source 12.9, including the verified nonzero moving determinants and sign-valued phase. -/
66 theorem source_square_class [FiniteDimensional (ZMod p) V] [FiniteDimensional (ZMod p) W] (g : V ≃ₗ[ZMod p] V) (h : W ≃ₗ[ZMod p] W)
67     (hg : Nat.Coprime (orderOf g) p) (hh : Nat.Coprime (orderOf h) p)
68     (hdim : Module.finrank (ZMod p) (moving g) / 2 = Module.finrank (ZMod p) (moving h) / 2)
69     (hdet : ∃ u : ZMod p, u ≠ 0 ∧
70       LinearMap.det (OddPhase.difference (movingAction h)) =
71         u ^ 2 * LinearMap.det (OddPhase.difference (movingAction g))) :
72     phase g = phase h ∧ (phase g = 1 ∨ phase g = -1) ∧
73       LinearMap.det (OddPhase.difference (movingAction g)) ≠ 0 ∧
74       LinearMap.det (OddPhase.difference (movingAction h)) ≠ 0 := by
75   obtain ⟨u, hu, hdet⟩ := hdet
76   exact ⟨square_class g h hdim u hu hdet, phase_sign g hg,
77     determinant_ne_zero g hg, determinant_ne_zero h hh⟩
78 
79 /-- An entirely fixed space has zero moving space and moving phase one. -/
80 theorem phase_identity : phase (LinearEquiv.refl (ZMod p) V) = 1 := by
81   have hm : moving (LinearEquiv.refl (ZMod p) V) = ⊥ := by
82     ext v
83     simp [moving]
84   let : Subsingleton (moving (LinearEquiv.refl (ZMod p) V)) := by rw [hm]; infer_instance
85   exact OddPhase.phase_zero_space (movingAction (LinearEquiv.refl (ZMod p) V))
86 
87 end PaperXI.MovingPhase

Back to source controls