Incidence proof that a cubic surface contains a line (source code)

= Incidence proof that a cubic surface contains a line

Cubic forms in four variables form $\mathbb P^{19}$. Lines form the four-dimensional <Grassmannian> $G=\operatorname{Gr}(2,4)$. The incidence pairs $(\ell,[F])$ with $F|_\ell=0$ form a projective-space bundle with fibre $\mathbb P^{15}$ over $G$, since restriction to a line imposes four independent linear conditions. Hence the incidence variety is irreducible of dimension 19. For $F=x_0^2x_2+x_1^2x_3$, a nearby line written $x_2=a_0x_0+a_1x_1$, $x_3=b_0x_0+b_1x_1$ lies on $F$ precisely when all four parameters vanish. This is an isolated point of that fibre. The <fiber dimension theorem> forces the image to have dimension 19, and projectivity makes the image closed. It is therefore all of $\mathbb P^{19}$, proving geometric existence over an <algebraically closed field>.