OddPhaseSum.lean

1 import PaperXI.FiniteProductDeterminant
2 import PaperXI.OddPhaseTransport
3 import PaperXI.OddSymplectic
4 
5 /-! Finite-product laws for the actual determinant phases. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.OddPhaseSum
9 open scoped BigOperators Classical
10 
11 variable {p : ℕ} [Fact p.Prime]
12 variable {ι : Type*} [Fintype ι] {V : ι → Type*}
13 variable [∀ i, AddCommGroup (V i)] [∀ i, Module (ZMod p) (V i)]
14 variable [∀ i, FiniteDimensional (ZMod p) (V i)]
15 
16 def action (g : ∀ i, V i ≃ₗ[ZMod p] V i) :
17     (∀ i, V i) ≃ₗ[ZMod p] (∀ i, V i) := LinearEquiv.piCongrRight g
18 
19 omit [Fintype ι] [∀ i, FiniteDimensional (ZMod p) (V i)] in
20 @[simp] theorem action_apply (g : ∀ i, V i ≃ₗ[ZMod p] V i)
21     (x : ∀ i, V i) (i : ι) : action g x i = g i (x i) := rfl
22 
23 omit [Fintype ι] [∀ i, FiniteDimensional (ZMod p) (V i)] in
24 theorem difference (g : ∀ i, V i ≃ₗ[ZMod p] V i) :
25     OddPhase.difference (action g) =
26       FiniteProductDeterminant.map (fun i => OddPhase.difference (g i)) := by
27   apply LinearMap.ext
28   intro x
29   rfl
30 
31 theorem determinant (g : ∀ i, V i ≃ₗ[ZMod p] V i) :
32     (OddPhase.difference (action g)).det = ∏ i, (OddPhase.difference (g i)).det := by
33   rw [difference, FiniteProductDeterminant.determinant]
34 
35 omit [Fintype ι] [∀ i, FiniteDimensional (ZMod p) (V i)] in
36 theorem fixedPointFree (g : ∀ i, V i ≃ₗ[ZMod p] V i)
37     (hg : ∀ i, OddPhase.FixedPointFree (g i)) : OddPhase.FixedPointFree (action g) := by
38   intro x hx
39   funext i
40   exact hg i (x i) (congrFun hx i)
41 
42 theorem half_dimension (h : ∀ i, Even (Module.finrank (ZMod p) (V i))) :
43     Module.finrank (ZMod p) (∀ i, V i) / 2 =
44       ∑ i, Module.finrank (ZMod p) (V i) / 2 := by
45   rw [Module.finrank_pi_fintype]
46   have he (i : ι) : Module.finrank (ZMod p) (V i) =
47       2 * (Module.finrank (ZMod p) (V i) / 2) := by
48     obtain ⟨n, hn⟩ := h i
49     omega
50   have hs : (∑ i, Module.finrank (ZMod p) (V i)) =
51       2 * ∑ i, Module.finrank (ZMod p) (V i) / 2 := by
52     calc
53       _ = ∑ i, 2 * (Module.finrank (ZMod p) (V i) / 2) :=
54         Finset.sum_congr rfl (fun i _ => he i)
55       _ = _ := (Finset.mul_sum _ _ _).symm
56   omega
57 
58 theorem phase_product (g : ∀ i, V i ≃ₗ[ZMod p] V i)
59     (h : ∀ i, Even (Module.finrank (ZMod p) (V i))) :
60     OddPhase.phase (action g) = ∏ i, OddPhase.phase (g i) := by
61   simp only [OddPhase.phase, determinant, half_dimension h, map_prod,
62     Finset.prod_mul_distrib]
63   rw [Finset.prod_pow_eq_pow_sum]
64 
65 theorem phase_product_symplectic (hp : p ≠ 2)
66     (b : ∀ i, LinearMap.BilinForm (ZMod p) (V i))
67     (ha : ∀ i, (b i).IsAlt) (hn : ∀ i, (b i).Nondegenerate)
68     (g : ∀ i, V i ≃ₗ[ZMod p] V i) :
69     OddPhase.phase (action g) = ∏ i, OddPhase.phase (g i) :=
70   phase_product g (fun i => OddSymplectic.even_finrank_zmod hp (b i) (ha i) (hn i))
71 
72 variable {X : Type*} [AddCommGroup X] [Module (ZMod p) X]
73 
74 /-- An actual decomposition equivalence intertwining the actions transports the product law. -/
75 theorem of_decomposition (hp : p ≠ 2)
76     (b : ∀ i, LinearMap.BilinForm (ZMod p) (V i))
77     (ha : ∀ i, (b i).IsAlt) (hn : ∀ i, (b i).Nondegenerate)
78     (g : ∀ i, V i ≃ₗ[ZMod p] V i) (G : X ≃ₗ[ZMod p] X)
79     (e : (∀ i, V i) ≃ₗ[ZMod p] X)
80     (he : ∀ x, e (action g x) = G (e x)) :
81     OddPhase.phase G = ∏ i, OddPhase.phase (g i) := by
82   rw [← OddPhase.conjugacy (action g) G e he]
83   exact phase_product_symplectic hp b ha hn g
84 
85 omit [Fintype ι] [∀ i, FiniteDimensional (ZMod p) (V i)] in
86 theorem fixedPointFree_of_decomposition (g : ∀ i, V i ≃ₗ[ZMod p] V i)
87     (hg : ∀ i, OddPhase.FixedPointFree (g i)) (G : X ≃ₗ[ZMod p] X)
88     (e : (∀ i, V i) ≃ₗ[ZMod p] X)
89     (he : ∀ x, e (action g x) = G (e x)) : OddPhase.FixedPointFree G := by
90   exact (OddPhase.fixedPointFree_conjugacy (action g) G e he).mp (fixedPointFree g hg)
91 
92 end PaperXI.OddPhaseSum

Back to source controls