Projective spaces

Stream: maths

[Adam Topaz]

Hi all,

I made a new PR with the definition of the projectivization of a vector space in #12438

It is tagged as RFC, because I would really like to hear your comments! This is only an initial PR, with the definition of projectivization K V, and some other very trivial basics (like constructing elements of the projectivization, maps between projective spaces associated to injective (semi)linear maps, etc.).

If you see anything glaring that's missing and should be added to this PR, please do let me know!

Eventually, I will like to work toward a proof of the fundamental theorem of projective geometry (and I may supervise an undergrad project this summer with this goal). Some other interesting future projects could be to construct the manifold structure in the case of projective spaces over $\mathbb{R}$ or $\mathbb{C}$, and/or to identify the points of the scheme-theoretic projective space (once it's defined) with this "classical" one.

[Riccardo Brasca]

Is it worth to do at least the basic definitions over a ring? Considering multiplication by a unit.

[Adam Topaz]

I thought about that, but I'm not convinced! Note that $\mathbb{P}^n(R)$ is not the naive thing when $R$ is not a field. (Here by $\mathbb{P}^n$ I mean $Proj \mathbb{Z}[T_0,\ldots,T_n]$, of course!)

[Riccardo Brasca]

Yes, in general they are different, but sometimes the two are related, right? For example if any projective module is free, a point of the true projective space should gives a point of the naive one if I am not confused

[Adam Topaz]

Yeah that's right.

[Adam Topaz]

Okay, maybe it is worthwhile to try to generalize a bit at this point.

[Riccardo Brasca]

If the generalization is essentially painless I would say "why not", but I totally agree to assume field if working over a ring causes problems.

[Riccardo Brasca]

Mmh, the natural condition would be to take n elements that generate the whole ring, and this already looks complicated

[Eric Wieser]

Riccardo Brasca said:

Considering multiplication by a unit.

I said the same thing in the PR - it makes some of the field cases easier to prove too