NilpotentLogarithm.lean

1 import PaperX.CommutativeLogarithm
2 import Mathlib.RingTheory.Adjoin.Polynomial.Basic
3 
4 /-! The finite logarithm in an arbitrary rational algebra. Each inverse
5 identity is proved inside the commutative subalgebra generated by one element,
6 then transported into the ambient ring. The ambient ring need not commute. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.NilpotentLogarithm
10 open PaperX.FiniteLogarithm
11 
12 variable {A : Type*} [Ring A] [Algebra ℚ A]
13 
14 theorem log_exp {a : A} (ha : IsNilpotent a) : log (IsNilpotent.exp a) = a := by
15   let S := Algebra.adjoin ℚ ({a} : Set A)
16   let b : S := ⟨a, Algebra.subset_adjoin rfl⟩
17   let f : S →+* A := S.val.toRingHom
18   have hb : IsNilpotent b := by
19     obtain ⟨d, hd⟩ := ha
20     refine ⟨d, ?_⟩
21     apply Subtype.ext
22     exact hd
23   calc
24     log (IsNilpotent.exp a) = f (log (IsNilpotent.exp b)) := by
25       rw [map_log (IsNilpotent.isNilpotent_exp_sub_one hb) f,
26         IsNilpotent.map_exp hb f]
27       rfl
28     _ = f b := congrArg f (PaperX.CommutativeLogarithm.log_exp hb)
29     _ = a := rfl
30 
31 theorem exp_log {u : A} (hu : IsNilpotent (u - 1)) :
32     IsNilpotent.exp (log u) = u := by
33   let S := Algebra.adjoin ℚ ({u - 1} : Set A)
34   let b : S := ⟨u - 1, Algebra.subset_adjoin rfl⟩
35   let v : S := 1 + b
36   let f : S →+* A := S.val.toRingHom
37   have hb : IsNilpotent b := by
38     obtain ⟨d, hd⟩ := hu
39     refine ⟨d, ?_⟩
40     apply Subtype.ext
41     exact hd
42   have hv : IsNilpotent (v - 1) := by
43     simpa only [v, add_sub_cancel_left] using hb
44   have hfv : f v = u := by
45     change 1 + (u - 1) = u
46     abel
47   calc
48     IsNilpotent.exp (log u) = f (IsNilpotent.exp (log v)) := by
49       rw [IsNilpotent.map_exp (isNilpotent_log hv) f, map_log hv f, hfv]
50     _ = f v := congrArg f (PaperX.CommutativeLogarithm.exp_log hv)
51     _ = u := hfv
52 
53 /-- Exponential and logarithm are actual inverse functions on the full
54 nilpotent and unipotent loci, with no fixed nilpotency bound. -/
55 def nilpotentEquiv : {a : A // IsNilpotent a} ≃ {u : A // IsNilpotent (u - 1)} where
56   toFun a := ⟨IsNilpotent.exp a, IsNilpotent.isNilpotent_exp_sub_one a.property⟩
57   invFun u := ⟨log u, isNilpotent_log u.property⟩
58   left_inv a := Subtype.ext (log_exp a.property)
59   right_inv u := Subtype.ext (exp_log u.property)
60 
61 theorem exp_injective {a b : A} (ha : IsNilpotent a) (hb : IsNilpotent b)
62     (h : IsNilpotent.exp a = IsNilpotent.exp b) : a = b := by
63   have he := congrArg log h
64   simpa only [log_exp ha, log_exp hb] using he
65 
66 theorem log_injective {u v : A} (hu : IsNilpotent (u - 1)) (hv : IsNilpotent (v - 1))
67     (h : log u = log v) : u = v := by
68   have he := congrArg IsNilpotent.exp h
69   simpa only [exp_log hu, exp_log hv] using he
70 
71 end PaperX.NilpotentLogarithm

Back to source controls