FiniteLogarithm.lean

1 import Mathlib.RingTheory.Nilpotent.Exp
2 
3 set_option autoImplicit false
4 
5 /-!
6 # A finite logarithm for unipotent elements
7 
8 The logarithm is evaluated as a finite rational polynomial in `u - 1`.
9 Its values away from unipotent elements are not assigned an interpretation.
10 -/
11 
12 namespace PaperX.FiniteLogarithm
13 
14 open Finset
15 
16 variable {A : Type*} [Ring A] [Algebra ℚ A]
17 
18 /-- The finite logarithm, with the zero coefficient at exponent zero included. -/
19 noncomputable def log (u : A) : A :=
20   ∑ j ∈ range (nilpotencyClass (u - 1)),
21     ((-1 : ℚ) ^ (j + 1) / (j : ℚ)) • (u - 1) ^ j
22 
23 /-- Any annihilating exponent gives the same finite logarithm. -/
24 theorem log_eq_sum {u : A} {d : ℕ} (hu : (u - 1) ^ d = 0) :
25     log u = ∑ j ∈ range d, ((-1 : ℚ) ^ (j + 1) / (j : ℚ)) • (u - 1) ^ j := by
26   have h₁ : (∑ j ∈ range d, ((-1 : ℚ) ^ (j + 1) / (j : ℚ)) • (u - 1) ^ j) =
27       (∑ j ∈ range (nilpotencyClass (u - 1)),
28         ((-1 : ℚ) ^ (j + 1) / (j : ℚ)) • (u - 1) ^ j) +
29       ∑ j ∈ Ico (nilpotencyClass (u - 1)) d,
30         ((-1 : ℚ) ^ (j + 1) / (j : ℚ)) • (u - 1) ^ j :=
31     (sum_range_add_sum_Ico _ (csInf_le' hu)).symm
32   have h₂ : (∑ j ∈ Ico (nilpotencyClass (u - 1)) d,
33       ((-1 : ℚ) ^ (j + 1) / (j : ℚ)) • (u - 1) ^ j) = 0 := by
34     exact sum_eq_zero fun _ hj => by
35       rw [pow_eq_zero_of_le (mem_Ico.1 hj).1 (pow_nilpotencyClass ⟨d, hu⟩), smul_zero]
36   dsimp [log]
37   rw [h₁, h₂, add_zero]
38 
39 @[simp]
40 theorem log_one : log (1 : A) = 0 := by
41   rw [log_eq_sum (d := 1) (by simp)]
42   simp
43 
44 /-- The finite logarithm of a unipotent element is nilpotent. -/
45 theorem isNilpotent_log {u : A} (hu : IsNilpotent (u - 1)) : IsNilpotent (log u) := by
46   rw [log]
47   apply Commute.isNilpotent_sum
48   · intro j _
49     by_cases hj : j = 0
50     · simp [hj]
51     · exact (IsNilpotent.pow_of_pos hu hj).smul _
52   · intro i j _ _
53     exact ((Commute.refl (u - 1)).pow_pow i j).smul_left _ |>.smul_right _
54 
55 /-- Ring maps preserve the finite logarithm on unipotent elements. -/
56 theorem map_log {B : Type*} [Ring B] [Algebra ℚ B] {u : A}
57     (hu : IsNilpotent (u - 1)) (f : A →+* B) : f (log u) = log (f u) := by
58   obtain ⟨d, hd⟩ := hu
59   have hd' : (f u - 1) ^ d = 0 := by
60     simpa only [map_pow, map_sub, map_one, map_zero] using congrArg f hd
61   simp [log_eq_sum hd, log_eq_sum hd', map_rat_smul]
62 
63 end PaperX.FiniteLogarithm

Back to source controls