NilpotentExponential.lean

1 import Mathlib.RingTheory.Nilpotent.Exp
2 import Mathlib.Algebra.Algebra.Rat
3 
4 /-! Finite nilpotent exponential algebra in characteristic zero. The rational
5 scalar action is derived from the original coefficient field, with no additional
6 scalar-compatibility hypothesis. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.NilpotentExponential
10 variable {K V W : Type*} [Field K] [CharZero K]
11   [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
12 
13 local instance : Module ℚ (Module.End K V) :=
14   Module.compHom (Module.End K V) (algebraMap ℚ K)
15 
16 def expN (N : Module.End K V) (t : K) : Module.End K V :=
17   IsNilpotent.exp (t • N)
18 
19 @[simp] theorem expN_zero (N : Module.End K V) : expN N 0 = 1 := by
20   simp [expN]
21 
22 theorem expN_add {N : Module.End K V} (hN : IsNilpotent N) (s t : K) :
23     expN N (s + t) = expN N s * expN N t := by
24   unfold expN
25   rw [add_smul]
26   apply IsNilpotent.exp_add_of_commute
27   · exact (Commute.refl N).smul_left s |>.smul_right t
28   · exact hN.smul s
29   · exact hN.smul t
30 
31 theorem expN_sum {N : Module.End K V} {d : ℕ} (hN : N ^ d = 0) (t : K) :
32     expN N t = ∑ j ∈ Finset.range d, (j.factorial : ℚ)⁻¹ • (t • N) ^ j := by
33   apply IsNilpotent.exp_eq_sum
34   simp [smul_pow, hN]
35 
36 theorem expN_intertwines {N : Module.End K V} {M : Module.End K W}
37     (hN : IsNilpotent N) (hM : IsNilpotent M)
38     (f : V →ₗ[K] W) (h : M ∘ₗ f = f ∘ₗ N) (t : K) :
39     expN M t ∘ₗ f = f ∘ₗ expN N t := by
40   let : Module ℚ V := Module.compHom V (algebraMap ℚ K)
41   let : Module ℚ W := Module.compHom W (algebraMap ℚ K)
42   apply Module.End.commute_exp_left_of_commute (hN.smul t) (hM.smul t)
43   ext x
44   simpa using congrArg (fun z => t • z) (LinearMap.congr_fun h x)
45 
46 @[simp] theorem expN_smul (N : Module.End K V) (a t : K) :
47     expN (a • N) t = expN N (t * a) := by
48   simp [expN, smul_smul]
49 
50 theorem expN_mul_neg {N : Module.End K V} (hN : IsNilpotent N) (t : K) :
51     expN N t * expN N (-t) = 1 := by
52   rw [← expN_add hN, add_neg_cancel, expN_zero]
53 
54 theorem expN_neg_mul {N : Module.End K V} (hN : IsNilpotent N) (t : K) :
55     expN N (-t) * expN N t = 1 := by
56   rw [← expN_add hN, neg_add_cancel, expN_zero]
57 
58 def expEquiv {N : Module.End K V} (hN : IsNilpotent N) (t : K) : V ≃ₗ[K] V where
59   toFun := expN N t
60   invFun := expN N (-t)
61   left_inv x := LinearMap.congr_fun (expN_neg_mul hN t) x
62   right_inv x := LinearMap.congr_fun (expN_mul_neg hN t) x
63   map_add' := (expN N t).map_add
64   map_smul' := (expN N t).map_smul
65 
66 theorem expN_identity_on_kernel {N : Module.End K V} (hN : IsNilpotent N)
67     (t : K) {x : V} (hx : N x = 0) : expN N t x = x := by
68   let : Module ℚ V := Module.compHom V (algebraMap ℚ K)
69   have hx' : ((t • N) ^ 1) • x = 0 := by simp [Module.End.smul_def, hx]
70   have h := IsNilpotent.exp_smul_eq_sum hx' (hN.smul t)
71   simpa [expN, Module.End.smul_def] using h
72 
73 /-- The construction is a finite polynomial over the original coefficient field. -/
74 theorem expN_polynomial {N : Module.End K V} {d : ℕ} (hN : N ^ d = 0) (t : K) :
75     expN N t = ∑ j ∈ Finset.range d, (t ^ j / (j.factorial : K)) • N ^ j := by
76   rw [expN_sum hN]
77   apply Finset.sum_congr rfl
78   intro j hj
79   change ((algebraMap ℚ K) ((j.factorial : ℚ)⁻¹)) • (t • N) ^ j = _
80   simp [smul_pow, smul_smul, div_eq_mul_inv, mul_comm]
81 
82 /-- Covariance with a scalar twist, in the order needed for reconstructing group actions. -/
83 theorem expN_covariance {N : Module.End K V} {M : Module.End K W}
84     (hN : IsNilpotent N) (hM : IsNilpotent M) (f : V →ₗ[K] W) (c : K)
85     (h : f ∘ₗ N = (c • M) ∘ₗ f) (t : K) :
86     f ∘ₗ expN N t = expN M (c * t) ∘ₗ f := by
87   have he := expN_intertwines hN (hM.smul c) f h.symm t
88   simpa [expN_smul, mul_comm] using he.symm
89 
90 end PaperX.NilpotentExponential

Back to source controls