BreakMoving.lean

1 import PaperXI.MovingPhase
2 import PaperXI.OrthogonalPhase
3 
4 /-! Actual finite-family moving spaces. The maps below use the image of the
5 actual difference, not an independently supplied vector space of the same size. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.BreakMoving
9 open FixedMoving
10 open scoped BigOperators Classical
11 
12 variable {K ι : Type*} [Field K] {V : ι → Type*}
13 variable [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
14 
15 /-- The moving image of the componentwise action is the product of the actual
16 component moving images. Its inverse assembles witnesses for each difference. -/
17 def productEquiv (g : ∀ i, V i ≃ₗ[K] V i) :
18     moving (LinearEquiv.piCongrRight g) ≃ₗ[K] (∀ i, moving (g i)) where
19   toFun x i := ⟨x.val i, by
20     obtain ⟨y, hy⟩ := x.property
21     exact ⟨y i, congrFun hy i⟩⟩
22   invFun x := ⟨fun i => (x i).val, by
23     choose y hy using fun i => (mem_moving (g i) (x i)).mp (x i).property
24     exact ⟨y, funext hy⟩⟩
25   left_inv x := by apply Subtype.ext; rfl
26   right_inv x := by funext i; apply Subtype.ext; rfl
27   map_add' x y := by funext i; apply Subtype.ext; rfl
28   map_smul' c x := by funext i; apply Subtype.ext; rfl
29 
30 @[simp] theorem productEquiv_coe (g : ∀ i, V i ≃ₗ[K] V i)
31     (x : moving (LinearEquiv.piCongrRight g)) (i : ι) :
32     (productEquiv g x i : V i) = x.val i := rfl
33 
34 @[simp] theorem productEquiv_symm_coe (g : ∀ i, V i ≃ₗ[K] V i)
35     (x : ∀ i, moving (g i)) (i : ι) :
36     ((productEquiv g).symm x).val i = (x i : V i) := rfl
37 
38 /-- This comparison intertwines the actual restricted moving actions. -/
39 theorem productEquiv_intertwines (g : ∀ i, V i ≃ₗ[K] V i)
40     (x : moving (LinearEquiv.piCongrRight g)) :
41     productEquiv g (movingAction (LinearEquiv.piCongrRight g) x) =
42       LinearEquiv.piCongrRight (fun i => movingAction (g i)) (productEquiv g x) := by
43   funext i
44   apply Subtype.ext
45   rfl
46 
47 variable {X : Type*} [AddCommGroup X] [Module K X]
48 
49 /-- An actual ambient decomposition gives the moving decomposition by
50 restriction followed by the proved product-image comparison. -/
51 def equiv (G : X ≃ₗ[K] X) (g : ∀ i, V i ≃ₗ[K] V i)
52     (e : X ≃ₗ[K] (∀ i, V i))
53     (he : ∀ x, e (G x) = LinearEquiv.piCongrRight g (e x)) :
54     moving G ≃ₗ[K] (∀ i, moving (g i)) :=
55   (movingEquiv G (LinearEquiv.piCongrRight g) e he).trans (productEquiv g)
56 
57 @[simp] theorem equiv_coe (G : X ≃ₗ[K] X) (g : ∀ i, V i ≃ₗ[K] V i)
58     (e : X ≃ₗ[K] (∀ i, V i))
59     (he : ∀ x, e (G x) = LinearEquiv.piCongrRight g (e x))
60     (x : moving G) (i : ι) : (equiv G g e he x i : V i) = e x i := rfl
61 
62 theorem equiv_intertwines (G : X ≃ₗ[K] X) (g : ∀ i, V i ≃ₗ[K] V i)
63     (e : X ≃ₗ[K] (∀ i, V i))
64     (he : ∀ x, e (G x) = LinearEquiv.piCongrRight g (e x)) (x : moving G) :
65     equiv G g e he (movingAction G x) =
66       LinearEquiv.piCongrRight (fun i => movingAction (g i)) (equiv G g e he x) := by
67   funext i
68   apply Subtype.ext
69   exact congrFun (he x) i
70 
71 /-- Orthogonal form preservation restricts to the actual moving images. -/
72 theorem equiv_preserves [Fintype ι]
73     (G : X ≃ₗ[K] X) (g : ∀ i, V i ≃ₗ[K] V i)
74     (e : X ≃ₗ[K] (∀ i, V i))
75     (he : ∀ x, e (G x) = LinearEquiv.piCongrRight g (e x))
76     (b : LinearMap.BilinForm K X) (bs : ∀ i, LinearMap.BilinForm K (V i))
77     (hb : ∀ x y, b x y = ∑ i, bs i (e x i) (e y i)) (x y : moving G) :
78     movingForm G b x y =
79       ∑ i, movingForm (g i) (bs i) (equiv G g e he x i) (equiv G g e he y i) :=
80   hb x y
81 
82 section PrimeField
83 variable {p : ℕ} [Fact p.Prime]
84 variable {Y : Type*} [AddCommGroup Y] [Module (ZMod p) Y]
85 variable [FiniteDimensional (ZMod p) Y]
86 
87 /-- In finite dimension, the source's exact fixed-point-free moving condition
88 already implies the fixed/moving complement. No order assumption is added. -/
89 theorem isCompl_of_moving_fixedPointFree (G : Y ≃ₗ[ZMod p] Y)
90     (hf : OddPhase.FixedPointFree (movingAction G)) : IsCompl (fixed G) (moving G) := by
91   constructor
92   · apply disjoint_iff.mpr
93     apply bot_unique
94     intro x hx
95     change x = 0
96     have hx' : movingAction G ⟨x, hx.2⟩ = ⟨x, hx.2⟩ := by
97       apply Subtype.ext
98       exact (mem_fixed G x).mp hx.1
99     exact congrArg Subtype.val (hf ⟨x, hx.2⟩ hx')
100   · apply Submodule.codisjoint_iff_exists_add_eq.mpr
101     intro x
102     let dx : moving G := ⟨G x - x, ⟨x, rfl⟩⟩
103     obtain ⟨y, hy⟩ := ((OddPhase.fixedPointFree_iff_bijective (movingAction G)).mp hf).2 dx
104     have hy' : G (y : Y) - (y : Y) = G x - x := congrArg Subtype.val hy
105     refine ⟨x - (y : Y), (y : Y), ?_, y.property, sub_add_cancel x (y : Y)⟩
106     rw [mem_fixed, map_sub]
107     exact sub_eq_sub_iff_sub_eq_sub.mp hy'.symm
108 
109 theorem movingForm_nondegenerate (G : Y ≃ₗ[ZMod p] Y)
110     (hf : OddPhase.FixedPointFree (movingAction G))
111     (b : LinearMap.BilinForm (ZMod p) Y) (ha : b.IsAlt) (hn : b.Nondegenerate)
112     (hb : ∀ x y, b (G x) (G y) = b x y) : (movingForm G b).Nondegenerate :=
113   movingForm_nondegenerate_of_isCompl G b ha hn hb (isCompl_of_moving_fixedPointFree G hf)
114 
115 end PrimeField
116 end PaperXI.BreakMoving

Back to source controls