(Real and Complex) projective spaces

Stream: mathlib4

[metakuntyyy]

I want to learn something about projective spaces so I thought about defining the projective real line and proving that it's diffeomorphic/homeomorphic to the sphere.

I tried to find any instance of the real or complex projective space in mathlib but I couldn't find anything.

This is what I would like to start with

import Mathlib

def projectiveSpace (K : Type*) [DivisionRing K] (dim: ℕ) :=
  Projectivization K (Fin (dim + 1) → K)

instance (K : Type*) [DivisionRing K] (dim: ℕ) :
  TopologicalSpace (projectiveSpace K dim) := sorry

def homeomorphicRealProjectiveSpaceCircle : Homeomorph (projectiveSpace ℝ 1) Circle :=
  sorry

Does anyone have some suggestions? I'd like to formalise some results from Wikipedia articles
https://en.wikipedia.org/wiki/Complex_projective_space
https://en.wikipedia.org/wiki/Real_projective_space
https://en.wikipedia.org/wiki/Projective_space

Eventually I'd like to prove some properties about homogeneous polynomials by lifting them to projective spaces.

[Aaron Liu]

we probably have the stereographic projection

[metakuntyyy]

I think we do, and I also think there is a manifold structure on the spheres.

[Weiyi Wang]

Is the plan to define projective space using docs#Module.Grassmannian
?

[Weiyi Wang]

I am also doing some elementary geometry in projective space and for now I just defined an adhoc quotient for myself

[Michael Rothgang]

metakuntyyy said:

I think we do, and I also think there is a manifold structure on the spheres.

Indeed we do, see e.g. docs#stereographic' and docs#EuclideanSpace.instIsManifoldSphere.

[metakuntyyy]

Weiyi Wang said:

Is the plan to define projective space using docs#Module.Grassmannian
?

What would the definition then be?

import Mathlib

def ProjectiveSpaceGrassmanian (R : Type*) [CommRing R] (dim: ℕ) :=
  Module.Grassmannian R (Fin (dim+1) → R) 1

[Michael Rothgang]

See also previous zulip discussion: #maths > Projective Space

[metakuntyyy]

Ah I see, so @Kenny Lau is doing it in way more generality than I ever could.

[Kevin Buzzard]

There are two distinct questions --construction of the algebro-geometric projective space and the differential-geometric one. Neither implies the other (until we have the analyticification functor, and even then it will be some work proving that the analyticification of the algebro-geometric object is diffeomorphic to the differential geometic one). I think Kenny is concerned with the algebraic geometry construction.