Codimension of intersection Suppose $E$ is a vector space over a field of characteristic $0$. Let $E_1, F_1$ be subspaces of finite codimension and let $E_2, F_2$ be their respective complements, i.e., $E = E_1 \oplus E_2 = F_1 \oplus F_2$.$\DeclareMathOperator{\codim}{codim}$
I know that $\dim E_2 = \codim E_1$ and $\dim  F_2 = \codim F_1$ because $E_2 \cong E/E_1$ and $F_2 \cong E/F_1$.
But I don't know how to prove that $\codim (E_1 \cap F_1) \le \dim E_2 + \dim F_2$. I saw a proof that $\codim (E_1 \cap F_1)$ is finite but it used some fancy isomorphism theorem, so I think a more bare hands approach would be helpful. Thanks.
 A: Maybe there is some way for avoiding the homomorphism theorems, but they're so handy and powerful that it is better trying to understand them.
Consider the linear map
$$
f\colon E\to E/E_1\oplus E/F_1,\qquad f(v)=(v+E_1,v+F_1)
$$
The kernel of this map is $E_1\cap F_1$, so $f$ induces an injective linear map
$$
\tilde{f}\colon E/(E_1\cap F_1)\to E/E_1\oplus E/F_1
$$
In particular, the domain is finite dimensional and
$$
\dim E/(E_1\cap F_1)\le\dim(E/E_1\oplus E/F_1)=
\dim(E/E_1)+\dim(E/F_1)
$$
which is the same as saying that
$$\DeclareMathOperator{\codim}{codim}
\codim(E_1\cap F_1)\le\codim E_1+\codim F_1
$$
A: Hint:
Consider the diagram
\begin{matrix}
0&\!\!\!\longrightarrow \!\!\!&E_1\cap F_1&\!\!\!\longrightarrow \!\!\!&E_1\bigoplus F_1&\!\!\!\longrightarrow \!\!\!&E_1+F_1&\!\!\!\longrightarrow &\!\!\!0\\
& & && \phantom{i\oplus j}\downarrow i\oplus j&& \phantom{k}\downarrow k\\
0&\!\!\!\longrightarrow \!\!\!&\Delta E\!\!\!&\!\!\!\longrightarrow \!\!\!&E\bigoplus E&\!\!\!\longrightarrow \!\!\!&E&\!\!\!\longrightarrow &\!\!\!0
\end{matrix} 
where $\Delta E$ is the diagonal of $E\bigoplus E$, $i,j,k$ are the canonical injections, and the rightmost horizontal maps (from the direct sums) are $\; (x, y)\longmapsto x-y $.
You deduce first from this diagram there exists a map $f\colon E_1\cap F_1\longrightarrow \Delta E$ which makes the whole diagram commutative.
Apply the Snake's lemma to show $\operatorname{coker} f$ is (isomorphic to) a submodule of $E/E_1\bigoplus E/F_1$.
