MonodromyData.lean

1 import PaperX.CarrierPolynomials
2 import Mathlib.RingTheory.Nilpotent.Basic
3 
4 /-! Algebraic monodromy pairs with the explicit convention F N F⁻¹ = q N.
5 F is an actual linear automorphism and N an actual nilpotent endomorphism.
6 No arithmetic Weil-group realization or inertia action is inferred. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.MonodromyData
10 open scoped BigOperators
11 open PaperX.CarrierSummands PaperX.CarrierPolynomials
12 
13 variable {K : Type*} [Field K]
14 
15 structure Datum (q : Kˣ) (V : Type*) [AddCommGroup V] [Module K V] where
16   F : V ≃ₗ[K] V
17   N : Module.End K V
18   nilpotent : IsNilpotent N
19   relation : ∀ x, F (N x) = (q : K) • N (F x)
20 
21 variable {q : Kˣ} {V : Type*} [AddCommGroup V] [Module K V]
22 
23 /-- The conjugation convention is a consequence of the pointwise relation. -/
24 theorem conjugation (D : Datum q V) : D.F.conj D.N = (q : K) • D.N := by
25   apply LinearMap.ext
26   intro x
27   simpa using D.relation (D.F.symm x)
28 
29 theorem kernel_stable (D : Datum q V) {x : V} (hx : D.N x = 0) : D.N (D.F x) = 0 := by
30   have h := D.relation x
31   rw [hx, map_zero] at h
32   exact (smul_eq_zero.mp h.symm).resolve_left (Units.ne_zero q)
33 
34 theorem kernel_inverse_stable (D : Datum q V) {x : V} (hx : D.N x = 0) :
35     D.N (D.F.symm x) = 0 := by
36   apply D.F.injective
37   rw [D.relation, D.F.apply_symm_apply, hx, smul_zero, map_zero]
38 
39 /-- Actual induced automorphism of the independently defined kernel. -/
40 def kernelF (D : Datum q V) : LinearMap.ker D.N ≃ₗ[K] LinearMap.ker D.N where
41   toFun x := ⟨D.F x.val, kernel_stable D x.property⟩
42   invFun x := ⟨D.F.symm x.val, kernel_inverse_stable D x.property⟩
43   left_inv x := by apply Subtype.ext; exact D.F.symm_apply_apply x.val
44   right_inv x := by apply Subtype.ext; exact D.F.apply_symm_apply x.val
45   map_add' x y := by apply Subtype.ext; exact map_add D.F x.val y.val
46   map_smul' a x := by apply Subtype.ext; exact map_smul D.F a x.val
47 
48 @[simp] theorem kernelF_val (D : Datum q V) (x : LinearMap.ker D.N) :
49     (kernelF D x).val = D.F x.val := rfl
50 
51 def kernelCharpoly [FiniteDimensional K V] (D : Datum q V) : Polynomial K :=
52   (kernelF D).toLinearMap.charpoly
53 
54 variable {I : Type*} {W : I → Type*}
55 variable [∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)]
56 
57 def copiesN (N : ∀ i, Module.End K (W i)) (m : I → ℕ) :
58     Module.End K (Copies W m) := piEnd (fun i => piEnd (fun _ : Fin (m i) => N i))
59 
60 @[simp] theorem copiesN_apply (N : ∀ i, Module.End K (W i)) (m : I → ℕ)
61     (x : Copies W m) (i : I) (k : Fin (m i)) : copiesN N m x i k = N i (x i k) := rfl
62 
63 theorem copiesN_pow_apply (N : ∀ i, Module.End K (W i)) (m : I → ℕ) (n : ℕ)
64     (x : Copies W m) (i : I) (k : Fin (m i)) :
65     (copiesN N m ^ n) x i k = (N i ^ n) (x i k) := by
66   induction n generalizing x with
67   | zero => rfl
68   | succ n ih =>
69       simp only [pow_succ, Module.End.mul_apply, copiesN_apply, ih]
70 
71 theorem copiesN_nilpotent [Fintype I] (N : ∀ i, Module.End K (W i))
72     (hN : ∀ i, IsNilpotent (N i)) (m : I → ℕ) : IsNilpotent (copiesN N m) := by
73   classical
74   choose n hn using hN
75   refine ⟨∑ i, n i, ?_⟩
76   apply LinearMap.ext
77   intro x
78   funext i k
79   rw [copiesN_pow_apply]
80   have hle : n i ≤ ∑ j, n j := Finset.single_le_sum (fun j _ => Nat.zero_le (n j)) (Finset.mem_univ i)
81   rw [pow_eq_zero_of_le hle (hn i)]
82   rfl
83 
84 def copiesF (D : ∀ i, Datum q (W i)) (m : I → ℕ) : Copies W m ≃ₗ[K] Copies W m :=
85   LinearEquiv.piCongrRight (fun i => LinearEquiv.piCongrRight (fun _ : Fin (m i) => (D i).F))
86 
87 @[simp] theorem copiesF_apply (D : ∀ i, Datum q (W i)) (m : I → ℕ)
88     (x : Copies W m) (i : I) (k : Fin (m i)) : copiesF D m x i k = (D i).F (x i k) := rfl
89 
90 /-- Every constituent is supplied; the sum's nilpotence is proved from theirs. -/
91 def copiesDatum [Fintype I] (D : ∀ i, Datum q (W i)) (m : I → ℕ) : Datum q (Copies W m) where
92   F := copiesF D m
93   N := copiesN (fun i => (D i).N) m
94   nilpotent := copiesN_nilpotent _ (fun i => (D i).nilpotent) m
95   relation x := by funext i k; exact (D i).relation (x i k)
96 
97 theorem inclusion_intertwines_N (N : ∀ i, Module.End K (W i))
98     {m c : I → ℕ} (h : ∀ i, m i ≤ c i) (x : Copies W m) :
99     inclusion (R := K) h (copiesN N m x) = copiesN N c (inclusion (R := K) h x) := by
100   funext i k
101   dsimp [inclusion]
102   split <;> simp
103 
104 theorem retraction_intertwines_N (N : ∀ i, Module.End K (W i))
105     {m c : I → ℕ} (h : ∀ i, m i ≤ c i) (x : Copies W c) :
106     retraction (R := K) h (copiesN N c x) = copiesN N m (retraction (R := K) h x) := rfl
107 
108 theorem inclusion_intertwines_F (D : ∀ i, Datum q (W i))
109     {m c : I → ℕ} (h : ∀ i, m i ≤ c i) (x : Copies W m) :
110     inclusion (R := K) h (copiesF D m x) = copiesF D c (inclusion (R := K) h x) := by
111   funext i k
112   dsimp [inclusion]
113   split <;> simp
114 
115 theorem retraction_intertwines_F (D : ∀ i, Datum q (W i))
116     {m c : I → ℕ} (h : ∀ i, m i ≤ c i) (x : Copies W c) :
117     retraction (R := K) h (copiesF D c x) = copiesF D m (retraction (R := K) h x) := rfl
118 
119 end PaperX.MonodromyData

Back to source controls