MonodromyExamples.lean

1 import PaperX.SpecialMonodromy
2 
3 /-! Exact boundaries for algebraic monodromy pairs. No arithmetic realization is asserted. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperX.MonodromyExamples
7 open Polynomial
8 open PaperX.MonodromyData PaperX.SpecialMonodromy
9 
10 variable {K : Type*} [Field K] {q : Kˣ}
11 variable {V : Type*} [AddCommGroup V] [Module K V]
12 
13 /-- Keep the entire Frobenius automorphism, but set monodromy to zero. -/
14 def eraseN (D : Datum q V) : Datum q V where
15   F := D.F
16   N := 0
17   nilpotent := ⟨1, by simp⟩
18   relation x := by simp
19 
20 def zeroKernelEquiv (D : Datum q V) : LinearMap.ker (eraseN D).N ≃ₗ[K] V where
21   toFun x := x.val
22   invFun x := ⟨x, rfl⟩
23   left_inv _ :=  rfl
24   right_inv _ :=  rfl
25   map_add' _ _ := rfl
26   map_smul' _ _ := rfl
27 
28 theorem zero_kernel_conjugate (D : Datum q V) :
29     (zeroKernelEquiv D).conj (kernelF (eraseN D)).toLinearMap = D.F.toLinearMap := by
30   apply LinearMap.ext
31   intro x
32   rfl
33 
34 variable [FiniteDimensional K V]
35 
36 theorem zero_kernel_charpoly (D : Datum q V) :
37     kernelCharpoly (eraseN D) = D.F.toLinearMap.charpoly := by
38   unfold kernelCharpoly
39   rw [← LinearEquiv.charpoly_conj (zeroKernelEquiv D), zero_kernel_conjugate]
40 
41 omit [FiniteDimensional K V] in
42 theorem zero_kernel_dimension (D : Datum q V) :
43     Module.finrank K (LinearMap.ker (eraseN D).N) = Module.finrank K V :=
44   (zeroKernelEquiv D).finrank_eq
45 
46 /-- The same whole Frobenius polynomial does not determine the kernel polynomial. -/
47 theorem same_F_different_kernel (q a : Kˣ) (n : ℕ) (hn : 1 < n) :
48     (eraseN (specialDatum q a n)).F = (specialDatum q a n).F ∧
49     kernelCharpoly (eraseN (specialDatum q a n)) ≠
50       kernelCharpoly (specialDatum q a n) := by
51   refine ⟨rfl, ?_⟩
52   intro h
53   have hd := congrArg Polynomial.natDegree h
54   rw [zero_kernel_charpoly, special_kernel_charpoly q a n (by omega),
55     LinearMap.charpoly_natDegree, natDegree_X_sub_C] at hd
56   simp only [Module.finrank_fin_fun] at hd
57   omega
58 
59 def scaleTwo : ℚˣ := Units.mk0 2 (by norm_num)
60 
61 theorem length_three_kernel :
62     kernelCharpoly (specialDatum scaleTwo 1 3) = X - 1 := by
63   rw [special_kernel_charpoly scaleTwo 1 3 (by decide)]
64   simp
65 
66 theorem length_three_dimensions :
67     Module.finrank ℚ (LinearMap.ker (specialDatum scaleTwo 1 3).N) = 1 ∧
68     Module.finrank ℚ (LinearMap.ker (eraseN (specialDatum scaleTwo 1 3)).N) = 3 := by
69   constructor
70   · exact special_kernel_dimension scaleTwo 1 3 (by decide)
71   · rw [zero_kernel_dimension]
72     simp
73 
74 theorem length_three_boundary :
75     (eraseN (specialDatum scaleTwo 1 3)).F.toLinearMap.charpoly =
76       (specialDatum scaleTwo 1 3).F.toLinearMap.charpoly ∧
77     kernelCharpoly (eraseN (specialDatum scaleTwo 1 3)) ≠
78       kernelCharpoly (specialDatum scaleTwo 1 3) :=
79   ⟨rfl, (same_F_different_kernel scaleTwo 1 3 (by decide)).2⟩
80 
81 end PaperX.MonodromyExamples

Back to source controls