given some DE \(Df=0\), have a \(k\) vector space of solutions \(s_1,\ldots,s_n\), where
\(n_i = \mathrm{ord}(s_i) > \mathrm{ord}(s_{i-1}) = n_{i-1}\)
\(M_{ij} = (D^{n_i} s_j)(0)\) is upper triangular, we want it be matrix with values in \(K[[t]]\),
by construction, \(\det M\) is a unit in \(K[[t]]\)
we can get a DE of order \(n_n+1\) annihilating \(s_1,\ldots,s_n\), and its leading term is invertible in \(K[[t]]\)
Consider \(D^{n_i}\)
Let’s think of flat connections \(D v = \Lambda v\), \(\Lambda_0 = 1\) \(\Lambda_1 = \Lambda\) \(\Lambda_{n+1} = D\Lambda_n + \Lambda_n \Lambda\)
we have \(D^n v = \Lambda_n v\), we obtain a \(K(t)\)-linear relation between \(n+1\) vectors \(v, Dv, \ldots, D^{n}v\) , and we can extract the first row
\[ D^i v_1 = \sum_j (\Lambda_i)_{1j} v_j \]
we construct an \((n+1)\times n\) matrix \(M = (\Lambda_i)_{1j}\) by noting that \(v_1 \wedge Dv_1 \wedge \ldots \wedge D^{n}v_1=0\), which expands to
\(S=\{m_0,\dots,m_n\}\) is nice if the matrices \(M_i\) obtained from it, satisfy \[v_t(\det(M_n)) \le v_t(\det(M_i)).\]
If \(S_0=\{0,1,\dots,n\}\) is not nice, then there is some \(i\) such that \(N = v_t(\det(M_n)) > v_t(\det(M_i))\).
Consider \(S_1=\{0,1,\dots,i-1, i+1,\dots,n,n+1\}\), then
\[ M_n(S_1) = M_i(S_0) \]
\[ \det(M_n(S_1)) = \det(M_i(S_0)) \le N-1 = v_t(\det(M_n(S_0))) - 1 \]
so this inductive process stops in \(N\) steps, we should be able to arrive at a nice \(S'\) with \(\max S' \le n + N\).
Two strategies
Inductive arguments, by relaxing degrees and make \(S\) larger we might be able to satisfy \(p\)-adic niceness
If there exists a subconnection W (i.e. a proper sub-bundle with connection) inside V such that v was a section of W, then det(Mi)=0 for all choices of S,i.
\(\left(\frac{d}{dt}\right)^k v \in W\) for all k.
Assume v generates V (i.e. there doesn’t exist a subconnection W with this property).
Flat connection on a scheme over Zp.
Could be subconnections on the special fibre which don’t come from subconnections on the generic fibre.
\(val_p (det(Mn)) >val_p (det(Mi))\) for some i<n