CommutativeLogarithm.lean

1 import PaperX.NilpotentSeries
2 import PaperX.FiniteLogarithm
3 
4 set_option autoImplicit false
5 
6 namespace PaperX.CommutativeLogarithm
7 
8 open PaperX.NilpotentSeries
9 open scoped BigOperators
10 
11 variable {A : Type*} [CommRing A] [Algebra ℚ A]
12 
13 theorem eval_log {u : A} (hu : IsNilpotent (u - 1)) :
14     eval (u - 1) (PowerSeries.log A) = FiniteLogarithm.log u := by
15   obtain ⟨k, hk⟩ := hu
16   rw [eval_eq_sum hk, FiniteLogarithm.log_eq_sum hk]
17   apply Finset.sum_congr rfl
18   intro n _
19   by_cases hn : n = 0
20   · subst n
21     simp
22   · simp [PowerSeries.coeff_log, hn, Algebra.smul_def]
23 
24 theorem subst_log {u : A} (hu : IsNilpotent (u - 1)) :
25     (PowerSeries.log A).subst (PowerSeries.C (u - 1)) =
26       PowerSeries.C (FiniteLogarithm.log u) := by
27   rw [subst_C_eq_C_eval hu, eval_log hu]
28 
29 theorem subst_exp {a : A} (ha : IsNilpotent a) :
30     (PowerSeries.exp A).subst (PowerSeries.C a) = PowerSeries.C (IsNilpotent.exp a) := by
31   rw [subst_C_eq_C_eval ha, eval_exp ha]
32 
33 /-- The finite logarithm recovers a nilpotent element with no bound on its nilpotency class. -/
34 theorem log_exp {a : A} (ha : IsNilpotent a) :
35     FiniteLogarithm.log (IsNilpotent.exp a) = a := by
36   have h := PowerSeries.subst_comp_subst_apply
37     (PowerSeries.HasSubst.exp_sub_one (A := A)) (hasSubst_C ha) (PowerSeries.log A)
38   rw [PowerSeries.subst_log_exp_sub_one, PowerSeries.subst_X (hasSubst_C ha),
39     PowerSeries.subst_sub (hasSubst_C ha), subst_exp ha] at h
40   have hone : (1 : PowerSeries A).subst (PowerSeries.C a) = 1 := by
41     rw [← PowerSeries.coe_substAlgHom (hasSubst_C ha), map_one]
42   rw [hone, ← map_one PowerSeries.C, ← map_sub, subst_log ha.isNilpotent_exp_sub_one] at h
43   exact (PowerSeries.C_injective h).symm
44 
45 /-- Exponentiation recovers every unipotent element from its finite logarithm. -/
46 theorem exp_log {u : A} (hu : IsNilpotent (u - 1)) :
47     IsNilpotent.exp (FiniteLogarithm.log u) = u := by
48   have h := PowerSeries.subst_comp_subst_apply
49     (PowerSeries.HasSubst.log (A := A)) (hasSubst_C hu) (PowerSeries.exp A)
50   rw [PowerSeries.subst_exp_log, PowerSeries.subst_add (hasSubst_C hu),
51     PowerSeries.subst_X (hasSubst_C hu), subst_log hu] at h
52   have hone : (1 : PowerSeries A).subst (PowerSeries.C (u - 1)) = 1 := by
53     rw [← PowerSeries.coe_substAlgHom (hasSubst_C hu), map_one]
54   rw [hone, subst_exp (FiniteLogarithm.isNilpotent_log hu)] at h
55   have hc := congrArg (PowerSeries.constantCoeff (R := A)) h
56   simpa using hc.symm
57 
58 end PaperX.CommutativeLogarithm

Back to source controls