Existence and uniqueness of the abstract residue map res_V: Omega^1_{K/k} -> k

(Setup) By [F4] one has $E=E_1+E_2$, so every $f\in K$, viewed in $E$, can be written $f=f_1+f_2$ with $f_1\in E_1$ and $f_2\in E_2$, i.e. every $f$ has a lift $f_1\in E_1$ with $f_1\equiv f(\mathrm{m}\mathrm{o}\mathrm{d}{E}_2)$; and for lifts $f_1,g_1\in E_1$ of $f,g$ the commutator $[f_1,g_1]$ lies in $E_1$ because $E_1$ is a two-sided ideal, while $[f_1,g_1]\equiv [f,g]=0(\mathrm{m}\mathrm{o}\mathrm{d}{E}_2)$ because $E_2$ is a two-sided ideal and elements of $K$ commute; hence $[f_1,g_1]\in E_1\cap E_2=E_0$ and ${\mathrm{Tr}}_V([f_1,g_1])$ is defined by [F4].

(Independence of the lift of the first argument) If $f_1,f_1^{\mathrm{\prime }}\in E_1$ both lift $f$ and $g_1\in E_1$, then ${\mathrm{Tr}}_V([f_1^{\mathrm{\prime }},g_1])-{\mathrm{Tr}}_V([f_1,g_1])={\mathrm{Tr}}_V([f_1^{\mathrm{\prime }}-f_1,g_1])=0$, because $f_1^{\mathrm{\prime }}-f_1\in E_2$, $g_1\in E_1$, and the commutator of an element of $E_1$ with an element of $E_2$ lies in $E_0$ with zero trace by [F5]; the same computation with the roles of the arguments exchanged shows independence of the lift of the second argument.

(Well-definedness of $r$) Define $r(f,g):={\mathrm{Tr}}_V([f_1,g_1])$ for lifts $f_1,g_1\in E_1$; step 2.1 shows $r$ is well defined. Moreover, if $(f_1,g_1)$ is any pair satisfying the hypotheses of the statement, say with $f_1\in E_1$, and $g_1^{\mathrm{\prime }\mathrm{\prime }}\in E_1$ is a lift of $g$, then ${\mathrm{Tr}}_V([f_1,g_1])={\mathrm{Tr}}_V([f_1,g_1^{\mathrm{\prime }\mathrm{\prime }}])=r(f,g)$, the first equality because $g_1^{\mathrm{\prime }\mathrm{\prime }}-g_1\in E_2$ and $f_1\in E_1$ and the second by step 2.1; the case $g_1\in E_1$ is symmetric.

($k$-bilinearity) $r$ is $k$-bilinear: for lifts $f_1,f_1^{\mathrm{\prime }},g_1\in E_1$ the sums and scalar multiples $f_1+f_1^{\mathrm{\prime }}$ and $\lambda f_1$ are again lifts in $E_1$, and ${\mathrm{Tr}}_V([f_1+f_1^{\mathrm{\prime }},g_1])={\mathrm{Tr}}_V([f_1,g_1])+{\mathrm{Tr}}_V([f_1^{\mathrm{\prime }},g_1])$, ${\mathrm{Tr}}_V([\lambda f_1,g_1])=\lambda {\mathrm{Tr}}_V([f_1,g_1])$ because ${\mathrm{Tr}}_V$ is $k$-linear on the finite potent subspace $E_0$, and the second argument is treated identically.

(The Leibniz relation) For $f,g,h\in K$ choose lifts $f_1,g_1,h_1\in E_1$; then $g_1{h}_1$, $f_1{g}_1$ and $h_1{f}_1$ are lifts in $E_1$ of $gh$, $fg$ and $fh$ (products of elements of the ideal $E_1$ are in $E_1$, and products of elements congruent to $f,g,h$ modulo $E_2$ are congruent modulo $E_2$), and the identity $[f_1,g_1{h}_1]-[f_1{g}_1,h_1]-[h_1{f}_1,g_1]=0$, which holds in any associative algebra by cancellation of $f_1{g}_1{h}_1$, gives $r(f,gh)=r(fg,h)+r(fh,g)$.

(Descent to ${\mathrm{\Omega }}_{K\mathrm{/}k}^1$) Let $T$ be the quotient of the free $k$-vector space on symbols $f\otimes g$ ($f,g\in K$) by all bilinearity relations and the Leibniz relations $f\otimes gh-fg\otimes h-fh\otimes g$. Give $T$ the $K$-module action $a\cdot (f\otimes g)=(af)\otimes g$. This action is well defined on the quotient: it preserves each bilinearity relation, and sends a Leibniz relation to $(af)\otimes gh-(af)g\otimes h-(af)h\otimes g$, again a Leibniz relation. Steps 4.1 and 5.1 make $f\otimes g\mapsto r(f,g)$ a well-defined $k$-linear map ${\rho }_T\text{\hspace{0.17em}⁣}:T\to k$. The assignment $D_T(g)=1\otimes g$ is a $k$-derivation $K\to T$: additivity and $k$-homogeneity follow from bilinearity, and the Leibniz relation with first factor $1$ gives $D_T(gh)=g{D}_T(h)+h{D}_T(g)$. The relation with $f=g=h=1$ gives $1\otimes 1=0$, so $D_T(\lambda )=1\otimes \lambda =\lambda (1\otimes 1)=0$ for every $\lambda \in k$. By [F7], there is a unique $K$-linear map $\eta \text{\hspace{0.17em}⁣}:{\mathrm{\Omega }}_{K\mathrm{/}k}^1\to T$ with $\eta (\mathrm{d}g)=1\otimes g$. Conversely, $\mu (f\otimes g)=f\mathrm{d}g$ defines a $K$-linear map $\mu \text{\hspace{0.17em}⁣}:T\to {\mathrm{\Omega }}_{K\mathrm{/}k}^1$ because $\mathrm{d}$ satisfies the Leibniz rule [F6]. These maps are inverse: $\mu \eta$ is the identity on the generators $\mathrm{d}g$, while $\eta \mu (f\otimes g)=f\cdot (1\otimes g)=f\otimes g$ on every generator of $T$. Hence $\eta$ identifies ${\mathrm{\Omega }}_{K\mathrm{/}k}^1$ with $T$.

(The residue map) Define ${\mathrm{res}}_V={\rho }_T\circ \eta \text{\hspace{0.17em}⁣}:{\mathrm{\Omega }}_{K\mathrm{/}k}^1\to k$, using the isomorphism $\eta$ of step 6.1. It is $k$-linear and satisfies ${\mathrm{res}}_V(f\mathrm{d}g)=r(f,g)={\mathrm{Tr}}_V([f_1,g_1])$ for all lifts $f_1,g_1\in E_1$ of $f,g$, and by step 3.1 also for every pair $f_1,g_1\in E$ satisfying the hypotheses of the statement.

(Uniqueness) If a $k$-linear map ${\mathrm{res}}^{\mathrm{\prime }}\text{\hspace{0.17em}⁣}:{\mathrm{\Omega }}_{K\mathrm{/}k}^1\to k$ satisfies the displayed formula for all admissible pairs, then ${\mathrm{res}}^{\mathrm{\prime }}$ and ${\mathrm{res}}_V$ agree on every element $f\mathrm{d}g$; since these elements generate ${\mathrm{\Omega }}_{K\mathrm{/}k}^1$ as a $K$-module by step 6.1, and hence as a $k$-vector space, ${\mathrm{res}}^{\mathrm{\prime }}={\mathrm{res}}_V$.

The map ${\mathrm{res}}_V$ therefore exists with the required values on all pairs of lifts satisfying the stated congruences and the condition $f_1\in E_1$ or $g_1\in E_1$ by steps 1.1, 3.1 and 7.1, and it is unique in the sense of step 8.1; the Axiom of Choice enters only through the cited suppliers, and no further choice is made.