BreakOddPhase.lean

1 import PaperXI.BreakMoving
2 
3 /-! Source 15.3 in odd characteristic, using the moving phase of Definition
4 12.7. Fixed vectors do not enter a determinant on the full singular space. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.BreakOddPhase
8 open FixedMoving
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 variable {X : Type*} [AddCommGroup X] [Module (ZMod p) X]
16 
17 omit [Fintype ι] [∀ i, FiniteDimensional (ZMod p) (V i)] in
18 /-- Fixed-point-freeness of the actual total moving action descends to every
19 actual summand moving action through the constructed moving decomposition. -/
20 theorem component_fixedPointFree
21     (G : X ≃ₗ[ZMod p] X) (g : ∀ i, V i ≃ₗ[ZMod p] V i)
22     (e : X ≃ₗ[ZMod p] (∀ i, V i))
23     (he : ∀ x, e (G x) = LinearEquiv.piCongrRight g (e x))
24     (hf : OddPhase.FixedPointFree (movingAction G)) (i : ι) :
25     OddPhase.FixedPointFree (movingAction (g i)) := by
26   have hp := (OddPhase.fixedPointFree_conjugacy (movingAction G)
27     (LinearEquiv.piCongrRight (fun j => movingAction (g j)))
28     (BreakMoving.equiv G g e he) (BreakMoving.equiv_intertwines G g e he)).mp hf
29   intro x hx
30   have hsingle : LinearEquiv.piCongrRight (fun j => movingAction (g j)) (Pi.single i x) =
31       Pi.single i x := by
32     funext j
33     by_cases hji : j = i
34     · subst j
35       simpa using hx
36     · simp [Pi.single_eq_of_ne hji]
37   have hz := congrFun (hp (Pi.single i x) hsingle) i
38   simpa using hz
39 
40 /-- Finite multiplicativity after constructing the actual moving equivalence.
41 The hypotheses on the summand moving forms are derived in `source` below. -/
42 theorem product_of_moving_forms (hp : p ≠ 2)
43     (G : X ≃ₗ[ZMod p] X) (g : ∀ i, V i ≃ₗ[ZMod p] V i)
44     (e : X ≃ₗ[ZMod p] (∀ i, V i))
45     (he : ∀ x, e (G x) = LinearEquiv.piCongrRight g (e x))
46     (b : ∀ i, LinearMap.BilinForm (ZMod p) (V i))
47     (ha : ∀ i, (b i).IsAlt) (hn : ∀ i, (movingForm (g i) (b i)).Nondegenerate) :
48     MovingPhase.phase G = ∏ i, MovingPhase.phase (g i) := by
49   change OddPhase.phase (movingAction G) = ∏ i, OddPhase.phase (movingAction (g i))
50   rw [OddPhase.conjugacy (movingAction G)
51     (OddPhaseSum.action (fun i => movingAction (g i)))
52     (BreakMoving.equiv G g e he) (BreakMoving.equiv_intertwines G g e he)]
53   exact OddPhaseSum.phase_product_symplectic hp (fun i => movingForm (g i) (b i))
54     (fun i => movingForm_alt (g i) (b i) (ha i)) hn (fun i => movingAction (g i))
55 
56 /-- The source moving hypothesis supplies nondegenerate moving restrictions
57 and hence the product law. No extra condition on the order of g is required. -/
58 theorem product (hp : p ≠ 2)
59     (G : X ≃ₗ[ZMod p] X) (g : ∀ i, V i ≃ₗ[ZMod p] V i)
60     (e : X ≃ₗ[ZMod p] (∀ i, V i))
61     (he : ∀ x, e (G x) = LinearEquiv.piCongrRight g (e x))
62     (b : ∀ i, LinearMap.BilinForm (ZMod p) (V i))
63     (ha : ∀ i, (b i).IsAlt) (hn : ∀ i, (b i).Nondegenerate)
64     (hb : ∀ i x y, b i (g i x) (g i y) = b i x y)
65     (hf : OddPhase.FixedPointFree (movingAction G)) :
66     MovingPhase.phase G = ∏ i, MovingPhase.phase (g i) :=
67   product_of_moving_forms hp G g e he b ha (fun i =>
68     BreakMoving.movingForm_nondegenerate (g i)
69       (component_fixedPointFree G g e he hf i) (b i) (ha i) (hn i) (hb i))
70 
71 omit [Fintype ι] in
72 /-- Each determinant in the actual moving product is nonzero. This conclusion
73 includes a zero moving space, whose endomorphism determinant is one. -/
74 theorem determinants_ne_zero
75     (G : X ≃ₗ[ZMod p] X) (g : ∀ i, V i ≃ₗ[ZMod p] V i)
76     (e : X ≃ₗ[ZMod p] (∀ i, V i))
77     (he : ∀ x, e (G x) = LinearEquiv.piCongrRight g (e x))
78     (hf : OddPhase.FixedPointFree (movingAction G)) (i : ι) :
79     (OddPhase.difference (movingAction (g i))).det ≠ 0 :=
80   (OddPhase.fixedPointFree_iff_det_ne_zero (movingAction (g i))).mp
81     (component_fixedPointFree G g e he hf i)
82 
83 omit [Fintype ι] [∀ i, FiniteDimensional (ZMod p) (V i)] in
84 /-- The finite product law is valid when the family is empty. -/
85 theorem empty [IsEmpty ι] (G : X ≃ₗ[ZMod p] X)
86     (e : X ≃ₗ[ZMod p] (∀ i, V i)) : MovingPhase.phase G = 1 := by
87   have : Subsingleton X := e.injective.subsingleton
88   exact OddPhase.phase_zero_space (movingAction G)
89 
90 omit [Fintype ι] [∀ i, FiniteDimensional (ZMod p) (V i)] in
91 /-- A summand with zero moving space contributes exactly one. -/
92 theorem zero_moving_factor (i : ι) (g : V i ≃ₗ[ZMod p] V i)
93     [Subsingleton (moving g)] : MovingPhase.phase g = 1 :=
94   OddPhase.phase_zero_space (movingAction g)
95 
96 section Internal
97 variable [FiniteDimensional (ZMod p) X]
98 
99 /-- The actual internal decomposition is equivariant in the inverse direction. -/
100 theorem internal_intertwines (G : X ≃ₗ[ZMod p] X)
101     (S : ι → Submodule (ZMod p) X) (hS : DirectSum.IsInternal S)
102     (hs : ∀ i, ∀ x ∈ S i, G x ∈ S i) (x : X) :
103     (OrthogonalPhase.decomposition S hS).symm (G x) =
104       LinearEquiv.piCongrRight (OrthogonalPhase.restricted G S hs)
105         ((OrthogonalPhase.decomposition S hS).symm x) := by
106   apply (OrthogonalPhase.decomposition S hS).injective
107   rw [LinearEquiv.apply_symm_apply, OrthogonalPhase.intertwines,
108     LinearEquiv.apply_symm_apply]
109 
110 omit [FiniteDimensional (ZMod p) X] in
111 /-- Orthogonality proves the actual internal decomposition's form identity. -/
112 theorem internal_form (b : LinearMap.BilinForm (ZMod p) X)
113     (S : ι → Submodule (ZMod p) X) (hS : DirectSum.IsInternal S)
114     (ho : ∀ i j, i ≠ j → ∀ x ∈ S i, ∀ y ∈ S j, b x y = 0)
115     (x y : ∀ i, S i) :
116     b (OrthogonalPhase.decomposition S hS x) (OrthogonalPhase.decomposition S hS y) =
117       ∑ i, b.restrict (S i) (x i) (y i) := by
118   simp only [OrthogonalPhase.decomposition_sum, map_sum, LinearMap.sum_apply]
119   apply Finset.sum_congr rfl
120   intro i _
121   exact Finset.sum_eq_single i (fun j _ hji => ho j i hji _ (x j).property
122     _ (y i).property) (fun hi => (hi (Finset.mem_univ i)).elim)
123 
124 /-- The constructed total moving equivalence preserves the actual orthogonal
125 sum of the moving forms; neither forms nor action covariance are abstract placeholders. -/
126 theorem internal_moving_form (G : X ≃ₗ[ZMod p] X)
127     (b : LinearMap.BilinForm (ZMod p) X)
128     (S : ι → Submodule (ZMod p) X) (hS : DirectSum.IsInternal S)
129     (ho : ∀ i j, i ≠ j → ∀ x ∈ S i, ∀ y ∈ S j, b x y = 0)
130     (hs : ∀ i, ∀ x ∈ S i, G x ∈ S i) (x y : moving G) :
131     movingForm G b x y = ∑ i,
132       movingForm (OrthogonalPhase.restricted G S hs i) (b.restrict (S i))
133         (BreakMoving.equiv G (OrthogonalPhase.restricted G S hs)
134           (OrthogonalPhase.decomposition S hS).symm (internal_intertwines G S hS hs) x i)
135         (BreakMoving.equiv G (OrthogonalPhase.restricted G S hs)
136           (OrthogonalPhase.decomposition S hS).symm (internal_intertwines G S hS hs) y i) := by
137   apply BreakMoving.equiv_preserves G (OrthogonalPhase.restricted G S hs)
138     (OrthogonalPhase.decomposition S hS).symm (internal_intertwines G S hS hs) b
139     (fun i => b.restrict (S i))
140   intro u v
141   simpa only [LinearEquiv.apply_symm_apply] using internal_form b S hS ho
142     ((OrthogonalPhase.decomposition S hS).symm u) ((OrthogonalPhase.decomposition S hS).symm v)
143 
144 /-- Source 15.3, odd branch: the actual finite internal orthogonal decomposition,
145 its restricted actions, and fixed-point-freeness on the total moving image imply
146 the Definition 12.7 moving-phase product. Empty families and zero summands are allowed. -/
147 theorem source (hp : p ≠ 2) (b : LinearMap.BilinForm (ZMod p) X)
148     (ha : b.IsAlt) (hn : b.Nondegenerate) (G : X ≃ₗ[ZMod p] X)
149     (hb : ∀ x y, b (G x) (G y) = b x y)
150     (S : ι → Submodule (ZMod p) X) (hS : DirectSum.IsInternal S)
151     (ho : ∀ i j, i ≠ j → ∀ x ∈ S i, ∀ y ∈ S j, b x y = 0)
152     (hs : ∀ i, ∀ x ∈ S i, G x ∈ S i)
153     (hf : OddPhase.FixedPointFree (movingAction G)) :
154     MovingPhase.phase G = ∏ i, MovingPhase.phase (OrthogonalPhase.restricted G S hs i) := by
155   exact product hp G (OrthogonalPhase.restricted G S hs)
156     (OrthogonalPhase.decomposition S hS).symm (internal_intertwines G S hS hs)
157     (fun i => b.restrict (S i))
158     (fun i => OrthogonalSummands.restricted_isAlt b ha (S i))
159     (fun i => OrthogonalSummands.restricted_form_nondegenerate b hn S
160       hS.submodule_iSup_eq_top ho i)
161     (fun i => OrthogonalSummands.restrictionEquiv_form b G hb (S i) (hs i)) hf
162 
163 end Internal
164 end PaperXI.BreakOddPhase

Back to source controls