LogarithmicRecovery.lean

1 import PaperX.NilpotentLogarithm
2 import PaperX.NilpotentExponential
3 
4 /-! General logarithmic extraction from an actual unipotent sample.
5 The coefficient field has characteristic zero. Nilpotence may have any finite
6 order, and the underlying vector spaces need not be finite dimensional. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.LogarithmicRecovery
10 
11 open PaperX.FiniteLogarithm PaperX.NilpotentLogarithm
12 open PaperX.NilpotentExponential
13 
14 variable {K V W : Type*} [Field K] [CharZero K]
15   [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
16 
17 local instance : Algebra ℚ (Module.End K V) :=
18   Algebra.compHom (Module.End K V) (algebraMap ℚ K)
19 
20 /-- Normalize the finite logarithm by the supplied nonzero sample parameter. -/
21 def recoverN (t : K) (U : Module.End K V) : Module.End K V := t⁻¹ • log U
22 
23 theorem recoverN_expN {N : Module.End K V} (hN : IsNilpotent N)
24     {t : K} (ht : t ≠ 0) : recoverN t (expN N t) = N := by
25   rw [recoverN, expN, log_exp (hN.smul t)]
26   simp [smul_smul, ht]
27 
28 /-- The logarithm is a finite polynomial over the original coefficient field. -/
29 theorem log_polynomial {U : Module.End K V} {d : ℕ} (hU : (U - 1) ^ d = 0) :
30     log U = ∑ j ∈ Finset.range d, ((-1 : K) ^ (j + 1) / (j : K)) • (U - 1) ^ j := by
31   rw [log_eq_sum hU]
32   apply Finset.sum_congr rfl
33   intro j hj
34   change ((algebraMap ℚ K) ((-1 : ℚ) ^ (j + 1) / (j : ℚ))) • (U - 1) ^ j = _
35   simp only [map_div₀, map_pow, map_neg, map_one, map_natCast]
36 
37 /-- A linear map intertwining unipotent operators also intertwines their
38 finite logarithms, even when their nilpotence orders differ. -/
39 theorem log_intertwines (U : Module.End K V) (Z : Module.End K W)
40     (hU : IsNilpotent (U - 1)) (hZ : IsNilpotent (Z - 1))
41     (f : V →ₗ[K] W) (h : Z ∘ₗ f = f ∘ₗ U) :
42     log Z ∘ₗ f = f ∘ₗ log U := by
43   obtain ⟨a, ha⟩ := hU
44   obtain ⟨b, hb⟩ := hZ
45   have h₁ : (Z - 1) ∘ₗ f = f ∘ₗ (U - 1) := by
46     simp only [LinearMap.sub_comp, LinearMap.comp_sub, Module.End.one_eq_id,
47       LinearMap.id_comp, LinearMap.comp_id, h]
48   rw [log_polynomial (pow_eq_zero_of_le (Nat.le_max_right a b) hb),
49     log_polynomial (pow_eq_zero_of_le (Nat.le_max_left a b) ha)]
50   ext x
51   simp only [LinearMap.comp_apply, LinearMap.sum_apply, LinearMap.smul_apply,
52     map_sum, map_smul]
53   apply Finset.sum_congr rfl
54   intro j hj
55   exact congrArg (fun y => ((-1 : K) ^ (j + 1) / (j : K)) • y)
56     (LinearMap.congr_fun (Module.End.commute_pow_left_of_commute h₁ j) x)
57 
58 /-- A single nonzero-parameter exponential sample determines an arbitrary
59 nilpotent monodromy operator. -/
60 theorem expN_injective {N M : Module.End K V} (hN : IsNilpotent N)
61     (hM : IsNilpotent M) {t : K} (ht : t ≠ 0)
62     (h : expN N t = expN M t) : N = M := by
63   have he := congrArg (recoverN t) h
64   simpa only [recoverN_expN hN ht, recoverN_expN hM ht] using he
65 
66 /-- Intertwining one common nonzero unipotent sample is equivalent to
67 intertwining the underlying nilpotent operators. -/
68 theorem expN_intertwines_iff {N : Module.End K V} {M : Module.End K W}
69     (hN : IsNilpotent N) (hM : IsNilpotent M) (f : V →ₗ[K] W)
70     {t : K} (ht : t ≠ 0) :
71     expN M t ∘ₗ f = f ∘ₗ expN N t ↔ M ∘ₗ f = f ∘ₗ N := by
72   constructor
73   · intro h
74     have hl := log_intertwines (expN N t) (expN M t)
75       (IsNilpotent.isNilpotent_exp_sub_one (hN.smul t))
76       (IsNilpotent.isNilpotent_exp_sub_one (hM.smul t)) f h
77     rw [expN, expN, log_exp (hM.smul t), log_exp (hN.smul t)] at hl
78     ext x
79     have hx := LinearMap.congr_fun hl x
80     apply smul_right_injective W ht
81     simpa using hx
82   · exact fun h => expN_intertwines hN hM f h t
83 
84 theorem recoverN_nilpotent {U : Module.End K V} (hU : IsNilpotent (U - 1)) (t : K) :
85     IsNilpotent (recoverN t U) := (isNilpotent_log hU).smul _
86 
87 theorem expN_recoverN {U : Module.End K V} (hU : IsNilpotent (U - 1))
88     {t : K} (ht : t ≠ 0) : expN (recoverN t U) t = U := by
89   unfold expN recoverN
90   simpa [smul_smul, ht] using exp_log hU
91 
92 /-- Fixed vectors of a unipotent operator are killed by its finite logarithm. -/
93 theorem log_kills_fixed {U : Module.End K V} (hU : IsNilpotent (U - 1))
94     {x : V} (hx : U x = x) : log U x = 0 := by
95   obtain ⟨d, hd⟩ := hU
96   rw [log_polynomial hd]
97   simp only [LinearMap.sum_apply, LinearMap.smul_apply]
98   apply Finset.sum_eq_zero
99   intro j hj
100   by_cases hzero : j = 0
101   · simp [hzero]
102   · obtain ⟨i, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hzero
103     have hz : (U - 1) x = 0 := by simp [hx]
104     rw [pow_succ (U - 1), Module.End.mul_apply, hz, map_zero, smul_zero]
105 
106 /-- One nonzero exponential sample has exactly the monodromy kernel as
107 its fixed space, for arbitrary finite nilpotence order. -/
108 theorem expN_fixed_iff {N : Module.End K V} (hN : IsNilpotent N)
109     {t : K} (ht : t ≠ 0) (x : V) : expN N t x = x ↔ N x = 0 := by
110   constructor
111   · intro hx
112     have hl := log_kills_fixed
113       (IsNilpotent.isNilpotent_exp_sub_one (hN.smul t)) hx
114     rw [log_exp (hN.smul t)] at hl
115     exact (smul_eq_zero.mp hl).resolve_left ht
116   · exact expN_identity_on_kernel hN t
117 
118 theorem kernel_expN_sub_one {N : Module.End K V} (hN : IsNilpotent N)
119     {t : K} (ht : t ≠ 0) : LinearMap.ker (expN N t - 1) = LinearMap.ker N := by
120   ext x
121   simp only [LinearMap.mem_ker, LinearMap.sub_apply, Module.End.one_apply, sub_eq_zero]
122   exact expN_fixed_iff hN ht x
123 
124 end PaperX.LogarithmicRecovery

Back to source controls