Dimension theory

[YaelDillies]

To state the product theorem, the Larsen-Pink inequality, etc... we need various basic results about the dimension of an algebraic variety, eg Lemma 6.2 in the notes says that if $V \subseteq \bar k^d$ is an irreducible subvariety and $P \in \bar k[X_1, \dots, X_d]$ does not vanish everywhere on $V$ then $\dim(V \cap V (P)) \le \dim(V) − 1$.

This is currently being developed for FLT by @erdOne.