MonodromyKernels.lean

1 import PaperX.MonodromyData
2 
3 set_option autoImplicit false
4 noncomputable section
5 namespace PaperX.MonodromyKernels
6 open scoped BigOperators
7 open PaperX.CarrierSummands PaperX.CarrierPolynomials PaperX.MonodromyData
8 
9 variable {K : Type*} [Field K] {q : Kˣ}
10 variable {I : Type*} [Fintype I] {W : I → Type*}
11 variable [∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)]
12 
13 /-- An independently defined kernel is exactly the product of constituent kernels. -/
14 def kernelCopiesEquiv (D : ∀ i, Datum q (W i)) (m : I → ℕ) :
15     LinearMap.ker (copiesDatum D m).N ≃ₗ[K]
16       Copies (fun i => LinearMap.ker (D i).N) m where
17   toFun x i k := ⟨x.val i k, congrFun (congrFun x.property i) k⟩
18   invFun x := ⟨fun i k => (x i k).val, by
19     funext i k
20     exact (x i k).property⟩
21   left_inv x := by apply Subtype.ext; rfl
22   right_inv x := rfl
23   map_add' x y := rfl
24   map_smul' a x := rfl
25 
26 theorem kernel_equivariant (D : ∀ i, Datum q (W i)) (m : I → ℕ)
27     (x : LinearMap.ker (copiesDatum D m).N) :
28     kernelCopiesEquiv D m (kernelF (copiesDatum D m) x) =
29       (LinearEquiv.piCongrRight (fun i => LinearEquiv.piCongrRight
30         (fun _ : Fin (m i) => kernelF (D i)))) (kernelCopiesEquiv D m x) := rfl
31 
32 theorem kernel_conjugate (D : ∀ i, Datum q (W i)) (m : I → ℕ) :
33     (kernelCopiesEquiv D m).conj (kernelF (copiesDatum D m)).toLinearMap =
34       piEnd (fun i => piEnd (fun _ : Fin (m i) => (kernelF (D i)).toLinearMap)) := by
35   apply LinearMap.ext
36   intro x
37   rfl
38 
39 variable [∀ i, FiniteDimensional K (W i)]
40 
41 theorem kernel_charpoly_product (D : ∀ i, Datum q (W i)) (m : I → ℕ) :
42     kernelCharpoly (copiesDatum D m) = ∏ i, kernelCharpoly (D i) ^ m i := by
43   unfold kernelCharpoly
44   rw [← LinearEquiv.charpoly_conj (kernelCopiesEquiv D m), kernel_conjugate,
45     charpoly_piEnd]
46   apply Finset.prod_congr rfl
47   intro i _
48   rw [charpoly_piEnd]
49   simp
50 
51 theorem kernel_dimension_sum (D : ∀ i, Datum q (W i)) (m : I → ℕ) :
52     Module.finrank K (LinearMap.ker (copiesDatum D m).N) =
53       ∑ i, m i * Module.finrank K (LinearMap.ker (D i).N) := by
54   rw [(kernelCopiesEquiv D m).finrank_eq, copies_finrank]
55 
56 theorem kernel_trace_sum (D : ∀ i, Datum q (W i)) (m : I → ℕ) :
57     LinearMap.trace K _ (kernelF (copiesDatum D m)).toLinearMap =
58       ∑ i, (m i : K) * LinearMap.trace K _ (kernelF (D i)).toLinearMap := by
59   rw [← LinearMap.trace_conj' _ (kernelCopiesEquiv D m), kernel_conjugate,
60     trace_piEnd]
61   apply Finset.sum_congr rfl
62   intro i _
63   rw [trace_piEnd]
64   simp
65 
66 /-- Coefficient comparison concerns the actual kernel polynomial here. -/
67 theorem common_kernel_polynomial {E : Type*} [CommRing E] (σ : E →+* K)
68     (D : ∀ i, Datum q (W i)) (m : I → ℕ) (P : I → Polynomial E)
69     (hP : ∀ i, kernelCharpoly (D i) = (P i).map σ) :
70     kernelCharpoly (copiesDatum D m) = (∏ i, P i ^ m i).map σ := by
71   rw [kernel_charpoly_product]
72   simp [hP, Polynomial.map_prod]
73 
74 end PaperX.MonodromyKernels

Back to source controls