HyperbolicSpace.lean

1 import Mathlib.LinearAlgebra.Dual.Lemmas
2 import Mathlib.LinearAlgebra.BilinearForm.Properties
3 import Mathlib.LinearAlgebra.FiniteDimensional.Basic
4 import Mathlib.LinearAlgebra.Prod
5 import Mathlib.Tactic
6 
7 /-! The actual hyperbolic space U × U*, its evaluation form, and its
8 contragredient action. No bilinear form or action identities are assumed. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.HyperbolicSpace
12 
13 variable (k U : Type*) [Field k] [AddCommGroup U] [Module k U]
14 
15 /-- The actual hyperbolic carrier. -/
16 abbrev Space := U × Module.Dual k U
17 
18 /-- The evaluation form with the convention k(u) - l(v). -/
19 def form : LinearMap.BilinForm k (Space k U) where
20   toFun x :=
21     { toFun := fun y => y.2 x.1 - x.2 y.1
22       map_add' := by intro y z; simp; ring
23       map_smul' := by intro r y; simp; ring }
24   map_add' := by
25     intro x y
26     apply LinearMap.ext
27     intro z
28     change z.2 (x.1 + y.1) - (x.2 + y.2) z.1 =
29       (z.2 x.1 - x.2 z.1) + (z.2 y.1 - y.2 z.1)
30     simp only [map_add, LinearMap.add_apply]
31     ring
32   map_smul' := by
33     intro r x
34     apply LinearMap.ext
35     intro y
36     change y.2 (r • x.1) - (r • x.2) y.1 = r • (y.2 x.1 - x.2 y.1)
37     simp only [map_smul, LinearMap.smul_apply, smul_sub]
38 
39 @[simp] theorem form_apply (x y : Space k U) :
40     form k U x y = y.2 x.1 - x.2 y.1 := rfl
41 
42 /-- Alternation holds in every characteristic. -/
43 theorem form_isAlt : (form k U).IsAlt := by
44   intro x
45   simp
46 
47 /-- Evaluation separates vectors and functionals, giving actual nondegeneracy. -/
48 theorem form_nondegenerate : (form k U).Nondegenerate := by
49   constructor
50   · intro x hx
51     apply Prod.ext
52     · apply (Module.forall_dual_apply_eq_zero_iff k x.1).1
53       intro l
54       simpa using hx (0, l)
55     · apply LinearMap.ext
56       intro u
57       have h := hx (u, 0)
58       simpa using h
59   · intro x hx
60     apply Prod.ext
61     · apply (Module.forall_dual_apply_eq_zero_iff k x.1).1
62       intro l
63       have h := hx (0, l)
64       simpa using h
65     · apply LinearMap.ext
66       intro u
67       simpa using hx (u, 0)
68 
69 variable {k U}
70 
71 /-- The original action on U paired with its inverse dual action on U*. -/
72 def action (a : U ≃ₗ[k] U) : Space k U ≃ₗ[k] Space k U :=
73   a.prodCongr a.symm.dualMap
74 
75 @[simp] theorem action_apply (a : U ≃ₗ[k] U) (x : Space k U) :
76     action a x = (a x.1, a.symm.dualMap x.2) := rfl
77 
78 /-- The inverse dual is forced by preservation of the evaluation pairing. -/
79 theorem action_form (a : U ≃ₗ[k] U) (x y : Space k U) :
80     form k U (action a x) (action a y) = form k U x y := by
81   simp [form_apply, LinearEquiv.dualMap_apply]
82 
83 /-- No nonzero fixed vector on U implies no nonzero fixed functional for
84 its inverse dual action. -/
85 theorem dual_fixedPointFree [FiniteDimensional k U] (a : U ≃ₗ[k] U)
86     (ha : ∀ u, a u = u → u = 0) (l : Module.Dual k U)
87     (hl : a.symm.dualMap l = l) : l = 0 := by
88   have hsurj : Function.Surjective (a.toLinearMap - 1 : Module.End k U) := by
89     apply LinearMap.surjective_of_injective
90     apply LinearMap.ker_eq_bot.mp
91     apply le_antisymm _ bot_le
92     intro u hu
93     change u = 0
94     change a u - u = 0 at hu
95     exact ha u (sub_eq_zero.mp hu)
96   apply LinearMap.ext
97   intro v
98   obtain ⟨u, hu⟩ := hsurj v
99   have hi := congrArg (fun f : Module.Dual k U => f (a u)) hl
100   change l (a.symm (a u)) = l (a u) at hi
101   rw [a.symm_apply_apply] at hi
102   rw [← hu]
103   change l (a u - u) = 0
104   rw [map_sub, ← hi, sub_self]
105 
106 /-- The actual hyperbolic action has no nonzero fixed vectors. -/
107 theorem action_fixedPointFree [FiniteDimensional k U] (a : U ≃ₗ[k] U)
108     (ha : ∀ u, a u = u → u = 0) (x : Space k U)
109     (hx : action a x = x) : x = 0 := by
110   apply Prod.ext
111   · exact ha x.1 (congrArg Prod.fst hx)
112   · exact dual_fixedPointFree a ha x.2 (congrArg Prod.snd hx)
113 
114 /-- The hyperbolic dimension is twice the original dimension, including U=0. -/
115 theorem finrank [FiniteDimensional k U] :
116     Module.finrank k (Space k U) = 2 * Module.finrank k U := by
117   rw [Module.finrank_prod, Subspace.dual_finrank_eq]
118   omega
119 
120 end PaperXI.HyperbolicSpace

Back to source controls