Minimal tangent dimension and homogeneous regularity

Since $X$ is an irreducible classical variety over the algebraically closed field $k$, it is nonempty, because irreducible means nonempty [F3]. Its affine models have reduced coordinate rings [F14], so $X$ is a reduced classical finite-type space over $k$ and the classical suppliers [F4], [F5], [F7] apply to it, while [F8] applies to the reduced finite-type spectra of its affine coordinate rings; in particular $X$ is its own unique irreducible component [F10], and the field $k$ is perfect [F9]. Fix a closed point $x$ of $X$. Because the only irreducible component of $X$ is $X$ itself [F10], [F3] and [F4] give ${\dim }_{x}X=\dim X$, and then [F7] gives ${\dim }_k{T}_{x}X\ge {\dim }_{x}X=\dim X$. Apply [F8] to the spectrum of any nonempty affine model chart. Its regular locus is open and nonempty, so [F15] supplies a closed, hence classical, point there whose local ring is regular by [F5]. At such a point [F6] gives ${\dim }_k{T}_{x}X=\dim {\mathcal{O}}_{X,x}$, while [F4] with [F3] gives $\dim {\mathcal{O}}_{X,x}={\dim }_{x}X=\dim X$; hence ${\dim }_k{T}_{x}X=\dim X$ for every closed point $x\in X_{\mathrm{r}\mathrm{e}\mathrm{g}}$.

Let $\sigma$ be an automorphism of the classical variety $X$, that is, an isomorphism of locally ringed spaces over $k$ with inverse ${\sigma }^{-1}$. At every closed point $x$ the induced stalk map of [F12], ${\sigma }_x^{\mathrm{♯}}:{\mathcal{O}}_{X,\sigma (x)}\to {\mathcal{O}}_{X,x}$, is a local ring homomorphism, and the stalk maps of $\sigma$ and ${\sigma }^{-1}$ are mutually inverse isomorphisms of local rings, so ${\mathcal{O}}_{X,\sigma (x)}$ is a regular local ring if and only if ${\mathcal{O}}_{X,x}$ is; hence $\sigma (X_{\mathrm{r}\mathrm{e}\mathrm{g}})=X_{\mathrm{r}\mathrm{e}\mathrm{g}}$. Likewise, since ${\sigma }^{-1}\circ \sigma ={\mathrm{id}}_X$ and $\sigma \circ {\sigma }^{-1}={\mathrm{id}}_X$, the functoriality of the differential [F11] applied to these two composites gives $d_{\sigma (x)}({\sigma }^{-1})\circ d_x\sigma =d_x({\mathrm{id}}_X)={\mathrm{id}}_{T_{x}X}$ and $d_x\sigma \circ d_{\sigma (x)}({\sigma }^{-1})={\mathrm{id}}_{T_{\sigma (x)}X}$, so $d_x\sigma$ is an isomorphism and ${\dim }_k{T}_{\sigma (x)}X={\dim }_k{T}_{x}X$ for every closed point $x$.

By the affine application of [F8] and [F15] in step 1.1 there is a classical closed point $x_0\in X_{\mathrm{r}\mathrm{e}\mathrm{g}}$; by step 1.1 its tangent dimension equals $\dim X$, and by step 1.1 again every closed point has tangent dimension at least $\dim X$. Hence the minimum of ${\dim }_k{T}_{x}X$ over the closed points of $X$ is attained and $\dim X={\min }_{x\in X}{\dim }_k{T}_{x}X$. Comparing step 1.1 with the criterion of [F5] and the definition of ${\dim }_{x}X$ in [F3] shows in addition that a closed point $x$ attains the minimum exactly when ${\dim }_k{T}_{x}X={\dim }_{x}X$, that is, exactly when $x\in X_{\mathrm{r}\mathrm{e}\mathrm{g}}$.

Now let $X$ be a nonempty reduced classical finite-type space over $k$ whose automorphism group $G$ acts transitively on its classical point set. Take a nonempty affine model with reduced finite-type coordinate ring $A$ [F2, F14]. By [F8] and [F9] the regular locus of $\mathrm{Spec}A$ is a nonempty open subset, so [F15] gives a classical closed point $x_0$ there with a regular local ring. By step 1.2, for every classical point $y$ an automorphism taking $x_0$ to $y$ identifies their local rings; thus every classical closed point is regular. Now take any point $z$ of the scheme model, represented by a prime $\mathfrak{p}$ in an affine chart $\mathrm{Spec}A$. Applying [F15] to the nonempty closed subset $V(\mathfrak{p})$ gives a maximal ideal $\mathfrak{m}\supseteq \mathfrak{p}$, hence a classical closed point. Its local ring $A_{\mathfrak{m}}$ is regular; [F16] then makes $A_{\mathfrak{p}}=(A_{\mathfrak{m}}{)}_{\mathfrak{p}{A}_{\mathfrak{m}}}$ regular. Since $z$ was arbitrary, every scheme point is regular, so the classical space and its scheme model are regular in the sense of [F5].

By definition [F5] the variety $X$ is regular when every point of it is regular, that is, when $X_{\mathrm{r}\mathrm{e}\mathrm{g}}=X$; every point of a classical variety is a closed point [F2]. If $X$ is regular, step 1.1 applies at every closed point and gives ${\dim }_k{T}_{x}X=\dim X$, so the function $x\mapsto {\dim }_k{T}_{x}X$ is constant. Conversely, suppose ${\dim }_k{T}_{x}X=c$ for every closed point; then $c$ is the minimum computed in step 2.1, so $c=\dim X$, and step 1.1 with [F3] gives ${\dim }_k{T}_{x}X=\dim X={\dim }_{x}X$ for every closed point $x$; by [F5] each such $x$ lies in $X_{\mathrm{r}\mathrm{e}\mathrm{g}}$, so $X_{\mathrm{r}\mathrm{e}\mathrm{g}}=X$ and $X$ is regular. This proves both directions of the equivalence.

Boundary and scope dispositions. Empty: an irreducible classical variety is nonempty by convention [F3], so the minimum of step 2.1 is taken over a nonempty set, and for the general claim the empty reduced space is excluded by hypothesis, the assertion being vacuous for it. Zero and one: at a point with ${\dim }_{x}X=0$ the criterion [F5] reads "$x$ regular if and only if ${\dim }_k{T}_{x}X=0$", so the zero-dimensional case is covered by the criterion without modification, and in the one-dimensional case the minimum of step 2.1 has the value one, attained at the regular points. Degenerate: reducedness is genuinely needed for the transitive claim, since a nonreduced local ring is not a regular local ring while the one-point nonreduced space $\mathrm{Spec}k[ϵ]\mathrm{/}({ϵ}^2)$ has a transitive automorphism group on its single point; for such a space the regular locus can be empty, so the supplier [F8] cannot be applied. Endpoints: the minimum of step 2.1 is attained exactly at the regular points, and the constant value of step 3.1 is exactly $\dim X$. Choice: AC is declared in [F1] and is used only through the AC-assuming suppliers [F4], [F5], [F7], [F8], [F10], [F15] and [F16], each cited at the step that uses it, while the automorphism arguments of steps 1.2 and 2.2 make no choice. Biconditional directions: step 3.1 proves both directions of the regularity-constancy equivalence, using step 1.1 in the forward direction and the minimum of step 2.1 in the reverse direction, and the criterion [F5] is instantiated in step 3.1 in the direction "tangent dimension equal to local dimension implies regular" while its defining content, regularity of the local ring, is what defines $X_{\mathrm{r}\mathrm{e}\mathrm{g}}$ in step 1.1.