UnipotentLogarithm.lean

1 import PaperX.NilpotentExponential
2 import Mathlib.Tactic.NormNum
3 
4 /-! Finite logarithmic recovery for nilpotence order at most three.
5 The exponential is Mathlib's actual nilpotent exponential. The logarithm
6 here is deliberately quadratic, and every inverse theorem states its
7 cubic nilpotence hypothesis explicitly. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperX.UnipotentLogarithm
11 
12 variable {A : Type*} [Ring A] [Module ℚ A]
13 
14 /-- Quadratic logarithm, meaningful as a complete logarithm when `(u-1)^3=0`. -/
15 def log₂ (u : A) : A := (u - 1) - (1 / 2 : ℚ) • (u - 1) ^ 2
16 
17 theorem exp_of_cube_zero {a : A} (ha : a ^ 3 = 0) :
18     IsNilpotent.exp a = 1 + a + (1 / 2 : ℚ) • a ^ 2 := by
19   rw [IsNilpotent.exp_eq_sum ha]
20   norm_num [Finset.sum_range_succ]
21 
22 theorem quadratic_square {a : A} (ha : a ^ 3 = 0) (c : ℚ) :
23     (a + c • a ^ 2) ^ 2 = a ^ 2 := by
24   have h₃ : a * a * a = 0 := by simpa only [pow_succ, pow_two, pow_zero, one_mul] using ha
25   have h₄ : (a * a) * (a * a) = 0 := by rw [← mul_assoc, h₃, zero_mul]
26   simp only [pow_two, add_mul, mul_add, smul_mul_assoc, mul_smul_comm]
27   rw [← mul_assoc a a a, h₃, h₄]
28   simp
29 
30 theorem quadratic_cube_zero {a : A} (ha : a ^ 3 = 0) (c : ℚ) :
31     (a + c • a ^ 2) ^ 3 = 0 := by
32   rw [pow_succ, quadratic_square ha]
33   have h₄ : a ^ 2 * a ^ 2 = 0 := by
34     rw [← pow_add]
35     exact pow_eq_zero_of_le (by decide) ha
36   rw [mul_add, ← pow_succ, ha, mul_smul_comm, h₄, smul_zero, zero_add]
37 
38 theorem exp_sub_one_cube_zero {a : A} (ha : a ^ 3 = 0) :
39     (IsNilpotent.exp a - 1) ^ 3 = 0 := by
40   rw [exp_of_cube_zero ha]
41   have h : 1 + a + (1 / 2 : ℚ) • a ^ 2 - 1 = a + (1 / 2 : ℚ) • a ^ 2 := by abel
42   rw [h]
43   exact quadratic_cube_zero ha _
44 
45 theorem log_exp {a : A} (ha : a ^ 3 = 0) : log₂ (IsNilpotent.exp a) = a := by
46   rw [log₂, exp_of_cube_zero ha]
47   have h : 1 + a + (1 / 2 : ℚ) • a ^ 2 - 1 = a + (1 / 2 : ℚ) • a ^ 2 := by abel
48   rw [h, quadratic_square ha]
49   exact add_sub_cancel_right _ _
50 
51 theorem log_cube_zero {u : A} (hu : (u - 1) ^ 3 = 0) : (log₂ u) ^ 3 = 0 := by
52   simpa only [log₂, sub_eq_add_neg, neg_smul] using quadratic_cube_zero hu (- (1 / 2 : ℚ))
53 
54 theorem exp_log {u : A} (hu : (u - 1) ^ 3 = 0) : IsNilpotent.exp (log₂ u) = u := by
55   rw [exp_of_cube_zero (log_cube_zero hu)]
56   have hs : (log₂ u) ^ 2 = (u - 1) ^ 2 := by
57     simpa only [log₂, sub_eq_add_neg, neg_smul] using quadratic_square hu (- (1 / 2 : ℚ))
58   rw [hs, log₂]
59   abel
60 
61 /-- The actual exponential and quadratic logarithm give a bijection on the stated loci. -/
62 def cubeEquiv : {a : A // a ^ 3 = 0} ≃ {u : A // (u - 1) ^ 3 = 0} where
63   toFun a := ⟨IsNilpotent.exp a, exp_sub_one_cube_zero a.property⟩
64   invFun u := ⟨log₂ u, log_cube_zero u.property⟩
65   left_inv a := Subtype.ext (log_exp a.property)
66   right_inv u := Subtype.ext (exp_log u.property)
67 
68 theorem exp_injective_on_cube_zero {a b : A} (ha : a ^ 3 = 0) (hb : b ^ 3 = 0)
69     (h : IsNilpotent.exp a = IsNilpotent.exp b) : a = b := by
70   have he := congrArg log₂ h
71   simpa only [log_exp ha, log_exp hb] using he
72 
73 section Linear
74 variable {K V W : Type*} [Field K] [CharZero K]
75   [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
76 local instance : Module ℚ (Module.End K V) :=
77   Module.compHom (Module.End K V) (algebraMap ℚ K)
78 open PaperX.NilpotentExponential
79 
80 /-- Normalize the logarithm of a unipotent sample at parameter `t`. -/
81 def recoverN (t : K) (U : Module.End K V) : Module.End K V := t⁻¹ • log₂ U
82 
83 omit [CharZero K] in
84 theorem smul_cube_zero {N : Module.End K V} (hN : N ^ 3 = 0) (t : K) :
85     (t • N) ^ 3 = 0 := by simp [smul_pow, hN]
86 
87 theorem recoverN_expN {N : Module.End K V} (hN : N ^ 3 = 0) {t : K} (ht : t ≠ 0) :
88     recoverN t (expN N t) = N := by
89   rw [recoverN, expN, log_exp (smul_cube_zero hN t)]
90   simp [smul_smul, ht]
91 
92 theorem log₂_field (U : Module.End K V) :
93     log₂ U = (U - 1) - (1 / 2 : K) • (U - 1) ^ 2 := by
94   change (U - 1) - ((algebraMap ℚ K) (1 / 2)) • (U - 1) ^ 2 = _
95   simp
96 
97 /-- Polynomial logarithms preserve actual linear intertwiners. -/
98 theorem log_intertwines (U : Module.End K V) (Z : Module.End K W)
99     (f : V →ₗ[K] W) (h : Z ∘ₗ f = f ∘ₗ U) :
100     log₂ Z ∘ₗ f = f ∘ₗ log₂ U := by
101   have h₁ : (Z - 1) ∘ₗ f = f ∘ₗ (U - 1) := by
102     simp only [LinearMap.sub_comp, LinearMap.comp_sub, Module.End.one_eq_id,
103       LinearMap.id_comp, LinearMap.comp_id, h]
104   have h₂ := Module.End.commute_pow_left_of_commute h₁ 2
105   simp only [log₂_field, LinearMap.sub_comp, LinearMap.comp_sub,
106     LinearMap.smul_comp, LinearMap.comp_smul, h₁, h₂]
107 
108 /-- One nonzero-parameter unipotent sample determines the monodromy operator
109 when both operators have nilpotence order at most three. -/
110 theorem expN_injective {N M : Module.End K V} (hN : N ^ 3 = 0) (hM : M ^ 3 = 0)
111     {t : K} (ht : t ≠ 0) (h : expN N t = expN M t) : N = M := by
112   have he := congrArg (recoverN t) h
113   simpa only [recoverN_expN hN ht, recoverN_expN hM ht] using he
114 
115 /-- At cubic nilpotence, a map intertwines monodromy exactly when it intertwines
116 one exponential sample with a nonzero common parameter. -/
117 theorem expN_intertwines_iff {N : Module.End K V} {M : Module.End K W}
118     (hN : N ^ 3 = 0) (hM : M ^ 3 = 0) (f : V →ₗ[K] W) {t : K} (ht : t ≠ 0) :
119     expN M t ∘ₗ f = f ∘ₗ expN N t ↔ M ∘ₗ f = f ∘ₗ N := by
120   constructor
121   · intro h
122     have hl := log_intertwines (expN N t) (expN M t) f h
123     rw [expN, expN, log_exp (smul_cube_zero hM t),
124       log_exp (smul_cube_zero hN t)] at hl
125     ext x
126     have hx := LinearMap.congr_fun hl x
127     apply smul_right_injective W ht
128     simpa using hx
129   · exact fun h => expN_intertwines ⟨3, hN⟩ ⟨3, hM⟩ f h t
130 
131 theorem recoverN_cube_zero {U : Module.End K V} (hU : (U - 1) ^ 3 = 0) (t : K) :
132     (recoverN t U) ^ 3 = 0 :=
133   smul_cube_zero (log_cube_zero hU) t⁻¹
134 
135 theorem expN_recoverN {U : Module.End K V} (hU : (U - 1) ^ 3 = 0)
136     {t : K} (ht : t ≠ 0) : expN (recoverN t U) t = U := by
137   unfold expN recoverN
138   simpa [smul_smul, ht] using exp_log hU
139 
140 /-- Fixed vectors of a linear operator are killed by its quadratic logarithm. -/
141 theorem log_kills_fixed {U : Module.End K V} {x : V} (hx : U x = x) :
142     log₂ U x = 0 := by
143   rw [log₂_field]
144   have h : (U - 1) x = 0 := by simp [hx]
145   simp [LinearMap.sub_apply, LinearMap.smul_apply, pow_two, Module.End.mul_apply, h]
146 
147 /-- For cubic nilpotence, one nonzero exponential sample has exactly the
148 monodromy kernel as its fixed space. -/
149 theorem expN_fixed_iff {N : Module.End K V} (hN : N ^ 3 = 0) {t : K} (ht : t ≠ 0)
150     (x : V) : expN N t x = x ↔ N x = 0 := by
151   constructor
152   · intro hx
153     have hl := log_kills_fixed hx
154     rw [expN, log_exp (smul_cube_zero hN t)] at hl
155     exact (smul_eq_zero.mp hl).resolve_left ht
156   · exact expN_identity_on_kernel ⟨3, hN⟩ t
157 
158 theorem kernel_expN_sub_one {N : Module.End K V} (hN : N ^ 3 = 0)
159     {t : K} (ht : t ≠ 0) : LinearMap.ker (expN N t - 1) = LinearMap.ker N := by
160   ext x
161   simp only [LinearMap.mem_ker, LinearMap.sub_apply, Module.End.one_apply, sub_eq_zero]
162   exact expN_fixed_iff hN ht x
163 end Linear
164 
165 end PaperX.UnipotentLogarithm

Back to source controls