Non-computational proof that $\det(A)$ is a unit in $R$ implies $A$ is a unit, for $A \in M_n(R)$. Quoting from Waterhouse's Introduction to Affine Group Schemes:
"...suppose we have a representable functor $G$ [from $k$-algebras to groups], and a map $\Delta: A \to A \otimes A$ giving a composition law on the $G(R)$... the units and inverses are uniquely determined and give natural maps, so by the Yoneda lemma there are uniquely determined (counit) $\epsilon$ and (coinverse) $S$ making $A$ a hopf algebra.
Consider for example $n \times n$ matrices with invertible determinant, represented by $k[X_{11}, \ldots, X_{nn}, 1 /\det]$. We might use a non-computational proof to show that such matrices are invertible and thus form a group. But then we have a group scheme, and hence $S$ exists. That is, we would know a priori that something like Cramer's rule must be true - there are polynomials in the $X_{ij}$ and $1/\det$ giving the entries of the inverse matrix."
Well - cool! But what non-computational proof?
I only know the one that constructs the inverse using adjugate matrics. Does anyone know a truly non-computational argument that proves $\det(A)$ invertible implies $A$ invertible?
 A: I thought of this one, though I'm curious to see if there are others.
Let $T:V\to V$ be a linear transformation between finite-dimensional spaces over $k$ with nonzero determinant.
By decomposing $V$ into the generalized eigenspaces for $T$, we may assume that $T$ has only one eigenvalue, $\lambda\neq 0$.
But then $\lambda I-T$ is nilpotent, which we can see this via the observation that any matrix is similar to an upper-triangular matrix.
So $(\lambda I-T)^m = 0$ for some $m$, giving us a polynomial $p(T)$ such that $\lambda^m I = Tp(T)$, and thus $T$ is invertible.

If we want to be really non-constructive, we can do the last step this way:
Let $R$ be the commutative ring with unity generated by $T$.  If $T$ were not invertible, it would be contained in some maximal ideal $\mathfrak{m}\subset R$.
But we have shown that $\lambda I - T$ is nilpotent, so it is contained in every maximal ideal.  Therefore $\lambda I\in \mathfrak{m}$, and $\lambda = 0$.

One more detail: technically this shows only that $T$ is invertible over $k[\lambda_1,\ldots , \lambda_k]$, not $k$.  We can fix this by, e.g. decomposing $T^{-1}$ over a basis for the field extension.
A: Elimination theory (aka projective schemes are proper) tells us that there is a polynomial in the entries of a matrix which can tell you if it is invertible or not. This is completely non constructive.
