felixwellen / synthetic-zariski

Latex documentation of our understanding of the synthetic /internal theory of the Zariski-Topos
MIT License
50 stars 5 forks source link

Finite affine schemes are projective #5

Closed felixwellen closed 6 months ago

felixwellen commented 12 months ago

Hugo suggested to me, it might be good to call an affine scheme $\mathrm{Spec} A$ finite, if A is a finite free R-module. So if $A=R^n$ is given, we can directly construct an embedding into $\mathrm{Spec}A\to \mathbb{P}^{n-1}$, by sending a homomorphism $R^n\to R$ to the vector given by the images of a standard basis $(e_i)_i$. The proposition $C$, to be in this subtype, is closed: For $[v]:\mathbb{P}^n$ let $\lambda_v=\sum \lambda_i v_i$, for $\lambda_i$ such that $\sum \lambda_i e_i=1$. Let $\varphi_v$ be the linear map sending $e_i$ to $v_i$. Then the conjunction of all $\lambda_v\cdot \varphi_v(e_i\cdot e_j)=\varphi_v(e_i)\cdot \varphi_v(e_j)$ is well-defined and closed and cuts out the $[v]$ such that $\varphi_v$ is an algebra homomorphism up to normalization.

felixwellen commented 11 months ago

With Hugo, we just figured out that the above doesn't work like claimed. The problem is, that in the above, the closed subset of $\mathbb{P}^{n-1}$ does also contain linear maps that do not map $1$ to $1$.

dwarn commented 11 months ago

I don't see the problem. Phrased differently, we consider the projective space $\mathbb PA^\star$ associated with the R-linear dual of $A$. This is $\mathbb P^{n-1}$ after choosing a basis of $A$. Given $[\varphi] : \mathbb PA^\star$ we consider the proposition $C([\varphi])$ that $\varphi(1) \varphi(xy) = \varphi(x) \varphi(y)$ for all $x, y : A$. This is well-defined and a closed proposition because it suffices to check it for basis elements of $A$. $C([\varphi])$ implies $\varphi(1) \ne 0$ because otherwise $\varphi(x)^2 = 0$ for all $x : A$ and then $\varphi$ is not-not zero (projective space contains only non-zero vectors). So $x \mapsto \varphi(x) / \varphi(1)$ determines a point of Spec A for $[\varphi] : \mathbb PA^\star$ such that $C([\varphi])$ holds (and one can go in the reverse direction, and verify that the two maps are inverse to each other).

felixwellen commented 11 months ago

Nice - thanks for refusing to see the problem non-existent problem ;-)

felixwellen commented 6 months ago

written down in "finite" -> closing.