HyperbolicDeterminant.lean

1 import PaperXI.HyperbolicSpace
2 import Mathlib.LinearAlgebra.Determinant
3 
4 /-! Determinants of the literal inverse-dual and hyperbolic difference maps.
5 All identities are established for the actual endomorphisms. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.HyperbolicDeterminant
9 
10 variable {k U : Type*} [Field k] [AddCommGroup U] [Module k U]
11 
12 /-- The inverse difference factors through the original difference. -/
13 theorem inverse_difference (a : U ≃ₗ[k] U) :
14     a.symm.toLinearMap - 1 = (-1 : k) • (a.symm.toLinearMap * (a.toLinearMap - 1)) := by
15   apply LinearMap.ext
16   intro u
17   change a.symm u - u = (-1 : k) • a.symm (a u - u)
18   rw [map_sub, a.symm_apply_apply, neg_one_smul, neg_sub]
19 
20 /-- The inverse-dual difference is exactly the dual of the inverse difference. -/
21 theorem dual_difference (a : U ≃ₗ[k] U) :
22     a.symm.dualMap.toLinearMap - 1 = (a.symm.toLinearMap - 1).dualMap := by
23   apply LinearMap.ext
24   intro l
25   apply LinearMap.ext
26   intro u
27   change l (a.symm u) - l u = l (a.symm u - u)
28   rw [map_sub]
29 
30 variable [FiniteDimensional k U]
31 
32 /-- The inverse-dual determinant identity in source 12.8. -/
33 theorem dual_difference_det (a : U ≃ₗ[k] U) :
34     LinearMap.det (a.symm.dualMap.toLinearMap - 1) =
35       (-1 : k) ^ Module.finrank k U * (LinearMap.det a.toLinearMap)⁻¹ *
36         LinearMap.det (a.toLinearMap - 1) := by
37   rw [dual_difference, LinearMap.det_dualMap, inverse_difference, LinearMap.det_smul,
38     map_mul, LinearEquiv.det_coe_symm]
39   ring
40 
41 omit [FiniteDimensional k U] in
42 /-- The actual hyperbolic difference is a block product of the two differences. -/
43 theorem action_difference (a : U ≃ₗ[k] U) :
44     (HyperbolicSpace.action a).toLinearMap - 1 =
45       (a.toLinearMap - 1).prodMap (a.symm.dualMap.toLinearMap - 1) := by
46   apply LinearMap.ext
47   intro x
48   apply Prod.ext <;> rfl
49 
50 /-- The full determinant is the stated sign times determinant inverse times a square. -/
51 theorem total_difference_det (a : U ≃ₗ[k] U) :
52     LinearMap.det ((HyperbolicSpace.action a).toLinearMap - 1) =
53       (-1 : k) ^ Module.finrank k U * (LinearMap.det a.toLinearMap)⁻¹ *
54         LinearMap.det (a.toLinearMap - 1) ^ 2 := by
55   rw [action_difference, LinearMap.det_prodMap, dual_difference_det]
56   ring
57 
58 /-- The hyperbolic action itself has determinant one. -/
59 theorem action_det (a : U ≃ₗ[k] U) : LinearMap.det (HyperbolicSpace.action a).toLinearMap = 1 := by
60   change LinearMap.det (a.toLinearMap.prodMap a.symm.dualMap.toLinearMap) = 1
61   rw [LinearMap.det_prodMap]
62   change LinearMap.det a.toLinearMap * LinearMap.det a.symm.toLinearMap.dualMap = 1
63   rw [LinearMap.det_dualMap]
64   exact a.det_mul_det_symm
65 
66 end PaperXI.HyperbolicDeterminant

Back to source controls