A transvection in a $K$-vector space $V$ is a linear map $T(f,v)$ of the form $x\mapsto x + f(x) v$, where $f\in V^*$ is a linear form and $v\in V$ is a vector such that $f(v)=0$. It is known that such a linear map is invertible, with inverse given by $f$ and $-v$. More precisely, one has $T(f,0)=\mathrm{id}$ and $T(f,v+w)=T(f,v)\circ T(f,w)$. In finite dimension, these maps have determinant $1$ and it is known that they generate the special linear group $\mathrm{SL}(V)$, the group of linear automorphisms of determinant $1$.
When I started formalizing in Lean the theory of the special linear group, the question raised itself of the appropriate generality for such results. In particular, what happens when one replaces the field $K$ with a ring $R$ and the $K$-vector space $V$ with an $R$-module?
The definition of the transvections still makes sense. If $f\colon M\to R$ is $R$-linear and $v\in M$, then the map $T(f,v)$ defined by $x\mapsto x+f(x) v$ is linear. When $f=0$ or $v=0$, this map is the identity. Moreover, if $v,w\in V$ are such that $f(v)=f(w)=0$, then $$ T(f,v) \circ T(f,w) (x)=T(f,v)(x+f(x)w)=x+f(x)w + f(x+f(x)w)v = x + f(x)(v+w),$$ so that $T(f,v)\circ T(f,w) = T(f, v+w)$. This implies that the map $v\mapsto T(f,v)$ is a morphism from the additive group of $V$ to the multiplicative monoid $\mathrm{End}(M)$ of $R$-endomorphisms of $M$. In particular, it lands into the group $\mathrm{GL}(M)$ of linear automorphisms of $M$.
Now assume that $M$ is a free $R$-module of finite rank, that is, has a finite basis $(b_1,\dots,b_n)$. This allows to define the determinant of an element of $\mathrm{End}(M)$, as the determinant of the associated matrix in the given basis, and one can ask about the determinant of these transvections. The following is not so surprising, but I couldn't find it in the literature.
Theorem. — For every $f\in M^*$ and $v\in M$ such that $f(v)=0$, one has $\det(T(f,v))=1$.
How can one prove such a result? The special case where $R$ is an integral domain is simpler, and is actually a step in the proof.
Proposition. — The theorem holds when $R$ is an integral domain.
Proof. — I can give two proofs of that result. The simplest one consists in considering the field of fractions $K$ of the integral domain $R$ and remarking that the matrix of the transvection $T(f,v)$ is also the matrix of a transvection in the $K$-vector space $V=K\otimes_R M$. In fact, if one identifies $M$ with $R^n$ by way of the matrix $b$, the linear form $f$ is a row vector in $R^n$, the vector $v$ is a column vector in $R^n$, satisfying $\sum f_j v_j=0$, the vector space $V$ is simply $K^n$, so that the matrix of $T(f,v)$ is also the matrix of a transvection in $V$. Its determinant is $1$, because of the case of fields, so that the determinant of $T(f,v)$ is $1$.
To be complete, let us explain the case of fields. The fact is that one choose an appropriate basis $(b_1,\dots,b_n)$ of $V$ such that $b_1=v$, $(b_1,\dots,b_{n-1})$ is a basis of $\ker(f)$ and $b_n$ is chosen such that $f(b_n)=1$. In that basis, the vector $v$ has coordinates $(1,0,\dots,0)$; the linear form $f$ is given by $f(x_1,\dots,x_n)=x_n$ and the linear map $T(f,v)$ is given by $(x_1,\dots,x_n)\mapsto (x_1+x_n,x_2,\dots,x_n)$. Its matrix is lower triangular, with only ones on the diagonal, hence its determinant is $1$.
Here is a second proof, more elaborate, but quite amusing. Since the determinant is multiplicative, the map $v\mapsto \det(T(f,v))$ is a group morphism from the submodule $\ker(f)$ to $R^\times$. To upgrade this result, one may consider an indeterminate $X$ and consider the transvection $T(f, Xv)$ of the $R[X]$-module $R[X]\otimes M$ deduced from $M$ by base change. This replaces the ring $R$ with the ring $R[X]$ and the determinant $D(X)=\det(T(f,Xv))$ is an invertible element of $R[X]$. A classical theorem describes such polynomials: their constant coefficient is invertible, and all other elements have to be nilpotent. Since $R$ is an integral domain, it has no nilpotent element, so that $D(X)$ is constant, invertible. One has $D(0)=\det(T(f,0))=\det(\mathrm{id})=1$, hence $D(X)=1$. Setting $X=1$, one gets $\det(T(f,v))=1$.
However, this second proof does not seem to generalize about the general case. On the other hand, a standard trick in algebra allows us to reduce to this case, namely, by reducing to the generic case. To explain this more easily, let us consider that $M=R^n$, where the linear form $f$ has coordinates $(f_1,\dots,f_n)$ and the vector $v$ has coordinates $(v_1,\dots,v_n)$. The relation $f(v)=0$ means that $\sum_{i=1}^n f_i v_i=0$, leading to the consideration of the ring $S=\mathbf Z[X_1,\dots,X_n,Y_1,\dots,Y_n]/\langle\sum X_i Y_i\rangle$ of polynomials with integer coefficients in $2n$ indeterminates quotiented out by the relation $\sum X_i Y_i=0$.
Proposition. — For $n\geq 2$, the ring $S=\mathbf Z[X_1,\dots,X_n,Y_1,\dots,Y_n]/\langle\sum X_i Y_i\rangle$ is an integral domain.
Proof. — Since $\mathbf Z$ is a unique factorization domain (UFD), a theorem of Gauss asserts that the polynomial ring $\mathbf Z[X_1,\dots,X_n,Y_1,\dots,Y_n]$ is again a UFD. Consequently, we have to prove that the polynomial $\sum_{i=1}^n X_i Y_i$ is irreducible if $n\geq 2$. Let us consider this ring as a ring of polynomials in the variable $Y_n$ with coefficients in the ring $S'=\mathbf Z[X_1,\dots,X_n,Y_1,\dots,Y_{n-1}]$ in $2n-1$ indeterminates. The proof of Gauss's theorem also establishes that the irreducible elemements of $S=S'[Y_n]$ are either the irreducible elements of $S'$, or the elements of $S'[Y_n]$ which are irreducible as polynomials in $K'[Y_n]$ ($K'$ being the field of fractions of $S'$) and such that the gcd of their coefficients is $1$. Our polynomial of interest is $X_n\cdot Y_n + \sum_{i=1}^{n-1} X_i Y_i$. It has degree $1$ in $Y_n$, hence is irreducible as a polynomial in $K'[Y_n]$. The gcd of its coefficients is $\gcd(X_n,\sum_{i=1}^{n-1}X_i Y_i)$. It divides $X_n$, so is either $\pm1$ or $\pm X_n$, and since $X_n$ doesn't divide $\sum_{i=1}^{n-1}X_i Y_i $, the gcd is equal to $1$, as claimed.
We can now conclude the proof of the theorem when $n\geq 2$. Indeed, the case of integral domains implies that the determinant of the generic transvection $T(X,Y)$ in $S^n$ is equal to $1$. Moreover, there is a (unique) ring morphism $\phi\colon \mathbf Z[X_1,\dots,X_n,Y_1,\dots,Y_n]/\langle \sum X_iY_i\rangle$ that maps $X_i$ to $f_i$ and $Y_i$ to $v_i$ for every $i$. Applying $\phi$ to the coefficients of the matrix $T(X,Y)$, one gets the matrix $T(f,v)$, so that $\det(T(f,v))=\phi(\det(T(X,Y)))=\phi(1)=1$.
When $n\leq 1$, the module $M$ is generated by one element $e$, and the condition $f(v)=0$ implies that $f(x)v=0$ for every $x\in M$, so that $T(f,v)=\mathrm{id}$. Consequently, $\det(T(f,v))=1$.
