Synthetic Proj construction?

[xuanruiqi]

It would be good to have a synthetic version of the Proj construction, as it would be useful for constructing projective schemes.

[felixwellen]

Yes that would be nice. Also to have a correspondence of schemes of the form $\mathrm{Proj}(S)$ to closed subsets of $\mathbb{P}^n$ as defined in foundations, "6 Projective Space". Maybe some of the things @mnieper wrote in random facts under "2 Homogeneity" can be used. Note that - as far as I know - it is also still open if every closed subset of $\mathbb P^n$ is a common zero set of homogeneous polynomials.

[iblech]

We at least have Definition 18.13 of my thesis. I don't know whether the description can be simplified.

[xuanruiqi]

Thanks @iblech! I think that should work. Sorry if this is a stupid question, but what kind of quotient did you mean by the slash in Def. 18.13?

[iblech]

When now rereading that passage, I also noticed that I should have been clearer!

I was referring to a version of the usual rescaling relation: Homomorphisms $\alpha,\beta : A \to R[T]$ are equivalent iff there is an invertible number $\lambda : R$ such that for all natural numbers $n$ and all homogeneous elements $x$ of degree $n$, $\alpha(x) = \lambda^n \beta(x)$.

[felixwellen]

Maybe the question was also what quotients are in the internal language? I know how to answer that in HoTT: We would use a set-quotient (6.10 in the HoTT-book).

[iblech]

Ah, yes! In my thesis I was working in the internal universe of the 1-topos, so everything was set-truncated, so yes, in the context of HoTT I mean the set quotient.

[xuanruiqi]

Thanks for clarifying! Yes, everything here seem to be sets at least as far as I know of

[mnieper]

Now that the winter term is coming to an end and I have some time, I am going to revisit this again.

[mnieper]

There is already some stuff in the branch called "projectivity". I still have to write a number of sections.

[xuanruiqi]

Thanks! Let's talk about this in Gothenburg.