Schemes

[FredericPaugam]

If schemes are not implemented yet, i wanted to recommend you the reading of Demazure-Gabriel ``groupes algébriques'', because their presentation of schemes should be adapted to a cubical agda implementation (without choice). For example, they define explicitely the open subset $V(I)$ as a concrete subsheaf of $Spec(A)$, the sheaf of sets associated to $A$ by Yoneda for the standard open topology. It is not representable in general, but you may show it is a sheaf and clearly, it is covered by standard opens $D(f)$ corresponding to generators of $I$. Schemes are then sheaves on the Grothendieck standard open site covered by some $Spec(A)$s, and they inherit a Zariski topology. The structural sheaf on arbitrary opens (without points) comes from functions with values in the affine line. I saw you had the classical opens in the cubical library, so i hope this may be useful. Projective space and Grasmaniann are defined similarly by their points in EGAI. Remark that the etale topology is also very close (just take etale algebras over rational opens instead to define sheaves). A similar approach works for wide classes of rigid analytic and complex analytic spaces (using affinoid Banach algebras and their rational algebras). However, in the analytic situation, you need ind-objets and completed tensor products, which probably makes the implementation more complicated.

[mzeuner]

Thanks for your recommendation. There is indeed an ongoing effort to add schemes or at least affine schemes to the library.
The idea is to not only work without choice but follow an approach that is entirely constructive. The main inspiration being the following paper:
https://link.springer.com/article/10.1007/s10472-009-9160-7

As a consequence we can not describe the opens of Spec(A) as sets of prime ideals...
Skimming through the first chapter of Demazure-Gabriel, I can't see how to make that work constructively,
but maybe I'm missing something?

In any case, I would love to have a classical definition of the Zariski spectrum and the structure sheaf and prove it equivalent
to the constructive definition (using LEM). So it's definitely worthwhile to keep this approach in mind.

[FredericPaugam]

Sorry, i can't download the article. I was also meaning an entirely constructive approach (without LEM) in the very same spirit, without using prime ideal, but a functorial one. You only need to define the affine Zariski Grothendieck site (whose objects are rings with ring morphisms and whose coverings are given by morphisms to standard localizations $A\to A[f^{-1}]$), and sheaves on it to define general schemes. This is almost what you pointed as being constructive in your answer. An affine scheme is equivalent to a representable presheaf of sets $Spec(A):R\mapsto \Hom(A,R)$ (the functor of points), defined using Yoneda embedding. In Demazure-Gabriel's book, they define Zariski opens as subsheaves of that functor of point $V(I)$ given by morphisms to the given ring $R$ that make $I$ the generating ideal for the ring. All this can be done only using Yoneda without sheaves so you already have it (if you have the category of rings) in the cubical library.
I mean you have a notion of Zariski open $U=V(I)$ of an affine scheme $X=Spec(A)$ and you define $O(U):=Hom(U,A^1)$ in presheaves on rings. This is what i meant. You don't even need sheaves up to this point. The Zariski spectrum is not a set: it is a functor on rings/algebras. You can then define general schemes as sheaves on the Zariski site on rings (a constructively definable site, i think, because it uses the lattice of localizations; so you also almost already have all that) that may be covered by affine schemes. You can find such a ``classical'' definition of schemes in some notes of mine (taken from the references therein) ---Section 5.4--- and ---Appendix F--- of:
https://webusers.imj-prg.fr/~frederic.paugam/documents/enseignement/3MA270-Algebre-complements.pdf
Sorry for this tricky reference. There are some papers by Toen et al. that may be better and more complete references.
Maybe i am wrong in thinking that it can be made entirely constructively only using higher inductive types to define localizations as in the cubical library (part on the Zariski lattice). I would be interested to know if that's the case. The advantage of this functorial approach, as i said, is that it works for arbitrary schemes, and it is also adapted to the analytic setting (very similar method), also treated without usual points, but with generalized points with values in commutative Banach rings. It is also much more natural and concrete to treat affine schemes functorially (e.g. affine schemes have easy to compute points: they are given by the solutions of the given equations with values in the given ring) and many ideas of EGA by Dieudonné and Grothendieck are formulated using the functor of points approach (smooth, etale, unramified, projective, proper morphisms).

[FredericPaugam]

I found the reference on spectral schemes on the web and found it quite nice and concrete. The functorial approach also has some advantages, and seems to me quite adapted to HoTT because it is based on universal properties (of polynomials, localizations and ring quotients) and the recurrent use of Yoneda lemma. Moduli spaces (e.g., elliptic curves, that are 0-Picard group of themselves) are better implemented using their functors of points (this is one of the main motivations for using this functorial approach to algebraic geometry). However, one needs to have the category of rings, and various universal constructions done in it (polynomials, localizations, quotients). I am not sure that this is shorter to implement than the lattice approach because the categories of commutative rings and algebras are missing in the cubical library, for the moment (but i guess not for long). Actually, having categories for all the algebraic objects in place would be great. I am also not completely certain that this functorial algebraic geometry is totally (HoTT) constructive, but if it is the case, it seems worth relating the lattice approach to the functorial approach.

[mzeuner]

Thanks for your elaborations and pointers to relevant literature. I still don't understand the functorial approach well enough
to be able to say whether it is completely constructive or not. However, as far as I understand it can serve as the basis for a constructive synthetic approach and this is done in particular in Ingo Blechschmidt's thesis:
https://rawgit.com/iblech/internal-methods/master/notes.pdf

I think @felixwellen has formalized some of this work (in Cubical Agda), but I'm not sure if this is going to be merged with the library at some point.

In any case I definitely agree that it would be worthwhile having a formalization of the functorial approach (using LEM if needed) and compare that to the lattice theoretic approach. We have the category of commutative rings now and fitting all the
universal constructions into the category theoretic setting shouldn't be too hard. Another thing that needs to implemented as well are sites, and I'm not sure how straightforward that will be.

[felixwellen]

I like the approach of ``groupes algébriques'' a lot. As far as I remember, they still use constructive reasoning in their site of rings. But as Max pointed out, some things that look nice in the functorial approach also work in the synthetic apporach of Ingo Blechschmidt, which is less work to formalize - I guess by orders of magnitude. However, I'm not really far with that, but all my algebra-related contrubutions to the cubical library are aimed at this.
Coincidentally, I'm just in the process of going through my last attempt at presenting the synthetic approach. I'll add a pointer here, when I'm done.

[felixwellen]

I should add, that the synthetic approach might be something completely different than what you are looking for.

[FredericPaugam]

Thank you for pointing out this synthetic approach. I am not sure that it is directly related but i would be interested to see how it is implemented. There is a direct link between the lattice approach and the functorial approach, however, since Demazure-Gabriel's Zariski site (used in Section 3 of their book) is simply the site whose underlying category is the category of rings, and whose coverings are given by the standard Zariski coverings present in the lattice approach in the cubical library.

The first test result to prove constructively (i am new to agda so it is hard for me to implement this: i get into trouble with level computations) is the following: if A is a ring and Spec(A) denotes the (Yoneda) functor on rings given by
Spec(A)(R)=Hom(A,R),
one wants to show that if $R\to R[f_i^{-1}]$ is a Zariski standard covering of R (in rings, i.e., the ideal generated by the $f_i$'s is R), then we may compute the set $Spec(A)(R)$ as the kernel (limit) of the usual diagram of sets associated to the covering. See:

https://math.stackexchange.com/questions/4104988/zariski-site-is-subcanonical

This means that $Spec(A)$ is a sheaf of sets on the ``big standard Zariski site'' of rings. This site is expressed purely in ring terms, without reference to points, so i don't see why it is not constructive (we don't even need ideals at this point). The proof of Demazure-Gabriel for this indeed use classical schemes, but you may use your constructive version, i guess, or even express everything purely algebraically like in the above reference.

And then, schemes are more general sheaves of sets on this site (Zariski lattice on the category of rings) that are locally affine (here, you probably need to use ideals to define general Zariski open subsheaves of affine sheaves). The general notion of Grothendieck topology seems complicated because one needs sieves, i.e., ---sub---presheaves, i.e., to use parts of a set. But maybe the notion of pre-topology (that came first historically), i.e., usual site, is easier to work with in type theory. And the particular case of the Zariski lattice used for schemes is already implemented in the cubical library...

[FredericPaugam]

Incidentally, i just realized that the relation with the lattice approach is the following: one would like to prove from what is already in the cubical library that R->Spec(A)(R)=Hom(A,R) is a sheaf on the Zariski lattice of R for every ring R. And functors F:Rings->Sets that fulfill this last condition are algebraic sheaves, i.e., form the big Zariski topos. A sheaf X in the Zariski topos is a scheme if it is covered by affine opens subsheaves, and these two conditions (being open and being covered) may both be formulated using the Zariski lattice (following my notes), so constructively, i think.

[felixwellen]

Thank you for pointing out this synthetic approach. I am not sure that it is directly related but i would be interested to see how it is implemented. There is a direct link between the lattice approach and the functorial approach, however, since Demazure-Gabriel's Zariski site (used in Section 3 of their book) is simply the site whose underlying category is the category of rings, and whose coverings are given by the standard Zariski coverings present in the lattice approach in the cubical library.

The first test result to prove constructively (i am new to agda so it is hard for me to implement this: i get into trouble with level computations) is the following: if A is a ring and Spec(A) denotes the (Yoneda) functor on rings given by Spec(A)(R)=Hom(A,R), one wants to show that if $R\to R[f_i^{-1}]$ is a Zariski standard covering of R (in rings, i.e., the ideal generated by the $f_i$'s is R), then we may compute the set $Spec(A)(R)$ as the kernel (limit) of the usual diagram of sets associated to the covering. See:

https://math.stackexchange.com/questions/4104988/zariski-site-is-subcanonical

This means that $Spec(A)$ is a sheaf of sets on the ``big standard Zariski site'' of rings. This site is expressed purely in ring terms, without reference to points, so i don't see why it is not constructive (we don't even need ideals at this point). The proof of Demazure-Gabriel for this indeed use classical schemes, but you may use your constructive version, i guess, or even express everything purely algebraically like in the above reference.

And then, schemes are more general sheaves of sets on this site (Zariski lattice on the category of rings) that are locally affine (here, you probably need to use ideals to define general Zariski open subsheaves of affine sheaves). The general notion of Grothendieck topology seems complicated because one needs sieves, i.e., ---sub---presheaves, i.e., to use parts of a set. But maybe the notion of pre-topology (that came first historically), i.e., usual site, is easier to work with in type theory. And the particular case of the Zariski lattice used for schemes is already implemented in the cubical library...

I see what you mean, and yes, that should be constructive.

[felixwellen]

Incidentally, i just realized that the relation with the lattice approach is the following: one would like to prove from what is already in the cubical library that R->Spec(A)(R)=Hom(A,R) is a sheaf on the Zariski lattice of R for every ring R. And functors F:Rings->Sets that fulfill this last condition are algebraic sheaves, i.e., form the big Zariski topos. A sheaf X in the Zariski topos is a scheme if it is covered by affine opens subsheaves, and these two conditions (being open and being covered) may both be formulated using the Zariski lattice (following my notes), so constructively, i think.

I'm not sure I understand. Can you say what the sheaf on the Zariski lattice of R is exactly?

[FredericPaugam]

I mean that if A is fixed, the functor $Spec(A)=Hom(A,-):D(r)\mapsto Hom(A,R[r^{-1}])$ defined on generators $D(r)$ of the Zariski lattice of any ring $R$ should extend to a sheaf $Spec(A)=Hom(A,-)$ of sets on the Zariski distributive lattice of $R$ in the sense of definition 2 p 3 of the reference above ``Spectral schemes on ring lattices'' (see also Lemma 4 of loc. cit.). This should be related to showing that $Spec(A)$ is a sheaf of sets for the standard open Grothendieck topology on every ring $R$, as is briefly explained in the above stackexchange reference. If we only use standard opens, we don't even need the Zariski lattice here. However, its use (or at least the use of arbitrary open subfunctors $D(I)=D(a_1,\dots,a_n)$ of affine schemes) seems necessary to define general open subsheaves of Zariski sheaves of sets, i.e., to define arbitrary schemes.

[felixwellen]

Thank you for pointing out this synthetic approach. I am not sure that it is directly related but i would be interested to see how it is implemented.

There is a start now:
https://github.com/felixwellen/synthetic-geometry/tree/main/SyntheticGeometry