Morphism from the projective space to `Spec(R) `

Stream: Is there code for X?

[Riccardo Brasca]

Do we have the canonical morphism Proj 𝒜 → Spec(𝒜 0) in some sense? I mean the structural morphism of the projective space. docs#AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec is quite close, but it's not exactly it. Thanks!

[Adam Topaz]

I don't know the actual answer, but I imagine that if you construct a docs#AlgebraicGeometry.Scheme.OpenCover by basic affine opens, you can use the result you mentioned (and compose with the map from degree zero elements) to obtain what you want

[Adam Topaz]

gluing could be done with AlgebraicGeometry.Scheme.OpenCover.glueMorphisms

[Adam Topaz]

I suppose this map could be constructed by hand as well on the level of topological spaces then locally ringed spaces,

[Riccardo Brasca]

Mmm, let me think about it. In my mental image this follows immediately by ΓSpec adjunction, but in mathlib the structure sheaf is a sheaf of rings, not a sheaf of blahblah-algebras.

[Adam Topaz]

sure, but then you would need to compute the global sections of proj, and I don't think that was done.

[Adam Topaz]

And yeah, this is just the plain proj construction, not the relative proj :-/

[Riccardo Brasca]

You don't really need to know what the global sections over the projective are, to give a morphism from X → Spec(R) is the same as to give R → Γ(X, F), where X is any scheme and F is the structure sheaf of X. So if the structure sheaf is a sheaf of R-algebras there is nothing to do. But indeed in mathlib this is not the case.

[Adam Topaz]

Yeah, ok. You at least need to k ow that a degree zero element gives rise to a global section.

[Adam Topaz]

The sheaf is defined essentially here: https://github.com/leanprover-community/mathlib4/blob/41eb6f94b1259c02e310381d93cf257d5049773c/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean#L179

I think constructing the map from the degree zero elements to the global sections shouldn't be that hard!

[Adam Topaz]

you just have to prove https://github.com/leanprover-community/mathlib4/blob/41eb6f94b1259c02e310381d93cf257d5049773c/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean#L74 for a degree zero element, which is easy!

[Riccardo Brasca]

Yes, this seems the easiest thing to do rather than gluing. I don't even know if we have the notion of sheaf of algebras, but sooner or later we should refactor the structure sheaf... anyway this is for a talk about what we have and what we want in mathlib, so I can just say we are missing this :D