Quasi-finite locus under base change

Stream: maths

[Andrew Yang]

I would like to show that the quasi-finite locus of the base change of a morphism is the preimage of the quasi-finite locus of the original morphism. This boils down to the following algebraic statement:

Let $L/K$ be a field extension, $A$ be a $K$-algebra of finite type, $q \in \operatorname{Spec} A \otimes_K L$ lying over $p \in \operatorname{Spec} A$, then $q$ is isolated iff $p$ is isolated.

I have a formalized proof of the following, which might be useful?

$p \in \operatorname{Spec} A$ is isolated iff $p$ is both maximal and minimal iff $A_p$ is $K$-finite.

The proof on stacks project (essentially stacks#00P4) uses a fair amout of dimension counting, which I hope could be avoided. It also uses the fact that $A \to A \otimes_K L$ satisfies the going down theorem, and I wonder if I can get this without showing that the map is flat?