FixedMoving.lean

1 import Mathlib.LinearAlgebra.BilinearForm.Orthogonal
2 import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
3 
4 /-! Actual fixed and moving subspaces, restricted symplectic forms and
5 the restricted moving automorphism. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.FixedMoving
9 
10 variable {F V : Type*} [Field F] [AddCommGroup V] [Module F V]
11 
12 /-- The actual fixed subspace of the given automorphism. -/
13 def fixed (g : V ≃ₗ[F] V) : Submodule F V := LinearMap.ker (g.toLinearMap - LinearMap.id)
14 
15 /-- The actual moving subspace, the image of `g - 1`. -/
16 def moving (g : V ≃ₗ[F] V) : Submodule F V := LinearMap.range (g.toLinearMap - LinearMap.id)
17 
18 @[simp] theorem mem_fixed (g : V ≃ₗ[F] V) (v : V) : v ∈ fixed g ↔ g v = v := by
19   simp [fixed, sub_eq_zero]
20 
21 theorem mem_moving (g : V ≃ₗ[F] V) (v : V) :
22     v ∈ moving g ↔ ∃ w : V, g w - w = v := Iff.rfl
23 
24 /-- A fixed vector is orthogonal to every actual moving vector. -/
25 theorem orthogonal (g : V ≃ₗ[F] V) (b : LinearMap.BilinForm F V)
26     (hg : ∀ x y, b (g x) (g y) = b x y)
27     {x y : V} (hx : x ∈ fixed g) (hy : y ∈ moving g) : b x y = 0 := by
28   obtain ⟨z, rfl⟩ := hy
29   have hfix : g x = x := (mem_fixed g x).mp hx
30   change b x (g z - z) = 0
31   rw [map_sub]
32   have h := hg x z
33   rw [hfix] at h
34   rw [h, sub_self]
35 
36 /-- Alternation gives orthogonality in the other order as well. -/
37 theorem orthogonal_reverse (g : V ≃ₗ[F] V) (b : LinearMap.BilinForm F V)
38     (hb : b.IsAlt) (hg : ∀ x y, b (g x) (g y) = b x y)
39     {x y : V} (hx : x ∈ moving g) (hy : y ∈ fixed g) : b x y = 0 := by
40   rw [← hb.neg_eq y x, orthogonal g b hg hy hx, neg_zero]
41 
42 /-- The actual form restricted to the fixed subspace. -/
43 def fixedForm (g : V ≃ₗ[F] V) (b : LinearMap.BilinForm F V) := b.restrict (fixed g)
44 
45 /-- The actual form restricted to the moving image. -/
46 def movingForm (g : V ≃ₗ[F] V) (b : LinearMap.BilinForm F V) := b.restrict (moving g)
47 
48 theorem fixedForm_alt (g : V ≃ₗ[F] V) (b : LinearMap.BilinForm F V) (hb : b.IsAlt) :
49     (fixedForm g b).IsAlt := fun x => hb x
50 
51 theorem movingForm_alt (g : V ≃ₗ[F] V) (b : LinearMap.BilinForm F V) (hb : b.IsAlt) :
52     (movingForm g b).IsAlt := fun x => hb x
53 
54 /-- Nondegeneracy transfers to either actual orthogonal direct summand. -/
55 theorem restrict_nondegenerate (b : LinearMap.BilinForm F V) (hb : b.Nondegenerate)
56     (P Q : Submodule F V) (hPQ : IsCompl P Q)
57     (ho : ∀ x ∈ P, ∀ y ∈ Q, b x y = 0)
58     (ho' : ∀ x ∈ Q, ∀ y ∈ P, b x y = 0) : (b.restrict P).Nondegenerate := by
59   constructor
60   · intro x hx
61     apply Subtype.ext
62     apply hb.1 x
63     intro v
64     obtain ⟨y, z, hy, hz, rfl⟩ := Submodule.codisjoint_iff_exists_add_eq.mp hPQ.codisjoint v
65     change b (x : V) (y + z) = 0
66     rw [map_add, ho x x.property z hz, add_zero]
67     exact hx ⟨y, hy⟩
68   · intro x hx
69     apply Subtype.ext
70     apply hb.2 x
71     intro v
72     obtain ⟨y, z, hy, hz, rfl⟩ := Submodule.codisjoint_iff_exists_add_eq.mp hPQ.codisjoint v
73     change b (y + z) (x : V) = 0
74     rw [map_add, LinearMap.add_apply, ho' z hz x x.property, add_zero]
75     exact hx ⟨y, hy⟩
76 
77 theorem movingForm_nondegenerate_of_isCompl (g : V ≃ₗ[F] V) (b : LinearMap.BilinForm F V)
78     (hb : b.IsAlt) (hbn : b.Nondegenerate) (hg : ∀ x y, b (g x) (g y) = b x y)
79     (hc : IsCompl (fixed g) (moving g)) : (movingForm g b).Nondegenerate :=
80   restrict_nondegenerate b hbn (moving g) (fixed g) hc.symm
81     (fun _ hx _ hy => orthogonal_reverse g b hb hg hx hy)
82     (fun _ hx _ hy => orthogonal g b hg hx hy)
83 
84 theorem fixedForm_nondegenerate_of_isCompl (g : V ≃ₗ[F] V) (b : LinearMap.BilinForm F V)
85     (hb : b.IsAlt) (hbn : b.Nondegenerate) (hg : ∀ x y, b (g x) (g y) = b x y)
86     (hc : IsCompl (fixed g) (moving g)) : (fixedForm g b).Nondegenerate :=
87   restrict_nondegenerate b hbn (fixed g) (moving g) hc
88     (fun _ hx _ hy => orthogonal g b hg hx hy)
89     (fun _ hx _ hy => orthogonal_reverse g b hb hg hx hy)
90 
91 theorem moving_stable (g : V ≃ₗ[F] V) {v : V} (hv : v ∈ moving g) : g v ∈ moving g := by
92   obtain ⟨w, rfl⟩ := hv
93   refine ⟨g w, ?_⟩
94   change g (g w) - g w = g (g w - w)
95   exact (map_sub g (g w) w).symm
96 
97 theorem moving_inverse_stable (g : V ≃ₗ[F] V) {v : V} (hv : v ∈ moving g) :
98     g.symm v ∈ moving g := by
99   obtain ⟨w, rfl⟩ := hv
100   refine ⟨g.symm w, ?_⟩
101   change g (g.symm w) - g.symm w = g.symm (g w - w)
102   simp
103 
104 /-- The actual restriction of `g` to its moving image, including its proved inverse. -/
105 def movingAction (g : V ≃ₗ[F] V) : moving g ≃ₗ[F] moving g where
106   toFun v := ⟨g v, moving_stable g v.property⟩
107   invFun v := ⟨g.symm v, moving_inverse_stable g v.property⟩
108   left_inv v := by apply Subtype.ext; exact g.symm_apply_apply v
109   right_inv v := by apply Subtype.ext; exact g.apply_symm_apply v
110   map_add' x y := by apply Subtype.ext; exact map_add g (x : V) (y : V)
111   map_smul' c x := by apply Subtype.ext; exact map_smul g c (x : V)
112 
113 @[simp] theorem movingAction_coe (g : V ≃ₗ[F] V) (v : moving g) :
114     (movingAction g v : V) = g v := rfl
115 
116 @[simp] theorem movingAction_symm_coe (g : V ≃ₗ[F] V) (v : moving g) :
117     ((movingAction g).symm v : V) = g.symm v := rfl
118 
119 theorem movingAction_preserves (g : V ≃ₗ[F] V) (b : LinearMap.BilinForm F V)
120     (hg : ∀ x y, b (g x) (g y) = b x y) (x y : moving g) :
121     movingForm g b (movingAction g x) (movingAction g y) = movingForm g b x y := hg x y
122 
123 /-- The actual restricted automorphism has no nonzero fixed vector in a direct decomposition. -/
124 theorem movingAction_fixedPointFree_of_isCompl (g : V ≃ₗ[F] V)
125     (hc : IsCompl (fixed g) (moving g)) (v : moving g) (hv : movingAction g v = v) : v = 0 := by
126   apply Subtype.ext
127   have hf : (v : V) ∈ fixed g := (mem_fixed g v).mpr (congrArg Subtype.val hv)
128   have hi : (v : V) ∈ fixed g ⊓ moving g := ⟨hf, v.property⟩
129   rw [hc.inf_eq_bot] at hi
130   exact hi
131 
132 /-- The restricted difference is injective by disjointness of the actual subspaces. -/
133 theorem moving_difference_injective (g : V ≃ₗ[F] V)
134     (hc : IsCompl (fixed g) (moving g)) :
135     Function.Injective ((movingAction g).toLinearMap - (LinearMap.id : Module.End F (moving g))) := by
136   apply LinearMap.ker_eq_bot.mp
137   apply bot_unique
138   intro v hv
139   change v = 0
140   apply movingAction_fixedPointFree_of_isCompl g hc v
141   change movingAction g v - v = 0 at hv
142   exact sub_eq_zero.mp hv
143 
144 /-- An actual linear equivalence for `g-1` on the moving image. -/
145 def movingDifferenceEquiv [FiniteDimensional F V] (g : V ≃ₗ[F] V)
146     (hc : IsCompl (fixed g) (moving g)) : moving g ≃ₗ[F] moving g :=
147   LinearEquiv.ofBijective ((movingAction g).toLinearMap - LinearMap.id)
148     ⟨moving_difference_injective g hc,
149       LinearMap.injective_iff_surjective.mp (moving_difference_injective g hc)⟩
150 
151 @[simp] theorem movingDifferenceEquiv_apply [FiniteDimensional F V]
152     (g : V ≃ₗ[F] V) (hc : IsCompl (fixed g) (moving g)) (v : moving g) :
153     movingDifferenceEquiv g hc v = movingAction g v - v := rfl
154 
155 section Transport
156 variable {V' : Type*} [AddCommGroup V'] [Module F V']
157 
158 /-- Conjugacy restricts to the actual moving images, with a constructed inverse. -/
159 def movingEquiv (g : V ≃ₗ[F] V) (g' : V' ≃ₗ[F] V') (e : V ≃ₗ[F] V')
160     (he : ∀ v, e (g v) = g' (e v)) : moving g ≃ₗ[F] moving g' where
161   toFun v := ⟨e v, by
162     obtain ⟨w, hw⟩ := v.property
163     refine ⟨e w, ?_⟩
164     change g' (e w) - e w = e v
165     rw [← he, ← map_sub]
166     exact congrArg e hw⟩
167   invFun v := ⟨e.symm v, by
168     obtain ⟨w, hw⟩ := v.property
169     refine ⟨e.symm w, ?_⟩
170     change g (e.symm w) - e.symm w = e.symm v
171     apply e.injective
172     rw [map_sub, he, e.apply_symm_apply, e.apply_symm_apply]
173     exact hw⟩
174   left_inv v := by apply Subtype.ext; exact e.symm_apply_apply v
175   right_inv v := by apply Subtype.ext; exact e.apply_symm_apply v
176   map_add' x y := by apply Subtype.ext; exact map_add e (x : V) (y : V)
177   map_smul' c x := by apply Subtype.ext; exact map_smul e c (x : V)
178 
179 @[simp] theorem movingEquiv_coe (g : V ≃ₗ[F] V) (g' : V' ≃ₗ[F] V') (e : V ≃ₗ[F] V')
180     (he : ∀ v, e (g v) = g' (e v)) (v : moving g) :
181     (movingEquiv g g' e he v : V') = e v := rfl
182 
183 /-- Restricted conjugacy intertwines the two actual restricted automorphisms. -/
184 theorem movingEquiv_intertwines (g : V ≃ₗ[F] V) (g' : V' ≃ₗ[F] V') (e : V ≃ₗ[F] V')
185     (he : ∀ v, e (g v) = g' (e v)) (v : moving g) :
186     movingEquiv g g' e he (movingAction g v) = movingAction g' (movingEquiv g g' e he v) := by
187   apply Subtype.ext
188   exact he v
189 
190 /-- An ambient symplectic conjugacy preserves the actual restricted moving forms. -/
191 theorem movingEquiv_preserves (g : V ≃ₗ[F] V) (g' : V' ≃ₗ[F] V') (e : V ≃ₗ[F] V')
192     (he : ∀ v, e (g v) = g' (e v)) (b : LinearMap.BilinForm F V)
193     (b' : LinearMap.BilinForm F V') (hb : ∀ x y, b' (e x) (e y) = b x y)
194     (x y : moving g) : movingForm g' b' (movingEquiv g g' e he x) (movingEquiv g g' e he y) =
195       movingForm g b x y := hb x y
196 
197 end Transport
198 end PaperXI.FixedMoving

Back to source controls