Projective space as an analytic manifold

For a nontrivially normed field 𝕜, the standard affine charts Projectivization.affineOpenPartialHomeomorph i identify the open sets U_i = {[v] | v i ≠ 0} of the projective space ℙ 𝕜 (Fin (n + 1) → 𝕜), with its quotient topology, with the affine space Fin n → 𝕜. Their transition maps divide the homogeneous coordinates Fin.insertNth i 1 z by one of their entries, so they are analytic where defined. Hence these n + 1 charts form an atlas making projective space a manifold modelled on 𝓘(𝕜, Fin n → 𝕜) at every order of smoothness r, including the analytic order ω.

Over ℂ this is the standard complex manifold structure on complex projective space ℂℙⁿ, and over ℝ the standard smooth structure on real projective space ℝℙⁿ.

Main declarations

• Projectivization.instChartedSpace: the atlas of standard affine charts.
• Projectivization.contDiffOn_affineChart_symm_trans: the transition maps are C^r for every r.
• Projectivization.instIsManifold: projective space is a C^r manifold for every r.
• Projectivization.instIsManifoldReal: over a normed ℝ-algebra, such as ℂ, it is also a real C^r manifold with the same charts.
• Projectivization.affineOpenPartialHomeomorph_mem_maximalAtlas: the affine charts lie in the maximal atlas of either manifold structure.
• Projectivization.contMDiffOn_affineChart and Projectivization.contMDiff_affineChart_symm: the affine charts and their inverses are C^r maps.
• Projectivization.contMDiff_of_contDiffOn_mk: a function on projective space given by a C^r function of the nonzero homogeneous coordinates is C^r.

References

• P. Griffiths and J. Harris, Principles of Algebraic Geometry, Chapter 0, §1.
• The atlas range affineOpenPartialHomeomorph, the choice of chartAt through exists_mem_affineOpen, and the proof of the manifold instance by isManifold_of_contDiffOn are adapted from the sphere-quotient construction of TauCeti.ComplexProjectiveSpace in TauCeti.Geometry.Manifold.Instances.ComplexProjectiveSpace.

@[instance_reducible]

noncomputable instance Projectivization.instChartedSpace {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} : ChartedSpace (Fin n → 𝕜) (Projectivization 𝕜 (Fin (n + 1) → 𝕜))

The atlas of projective space consisting of its n + 1 standard affine charts.

theorem Projectivization.mem_atlas_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} (e : OpenPartialHomeomorph (Projectivization 𝕜 (Fin (n + 1) → 𝕜)) (Fin n → 𝕜)) : e ∈ atlas (Fin n → 𝕜) (Projectivization 𝕜 (Fin (n + 1) → 𝕜)) ↔ ∃ (i : Fin (n + 1)), affineOpenPartialHomeomorph i = e

The charts of the atlas of projective space are exactly its standard affine charts.

theorem Projectivization.affineOpenPartialHomeomorph_mem_atlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} (i : Fin (n + 1)) : affineOpenPartialHomeomorph i ∈ atlas (Fin n → 𝕜) (Projectivization 𝕜 (Fin (n + 1) → 𝕜))

Each standard affine chart belongs to the atlas of projective space.

theorem Projectivization.contDiffOn_affineChart_symm_trans {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} (i j : Fin (n + 1)) (r : WithTop ℕ∞) : ContDiffOn 𝕜 r (↑((affineChart i).symm.trans (affineChart j))) ((affineChart i).symm.trans (affineChart j)).source

The transition maps between the standard affine charts of projective space are C^r for every r, including the analytic order ω.

instance Projectivization.instIsManifold {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} (r : WithTop ℕ∞) : IsManifold (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) r (Projectivization 𝕜 (Fin (n + 1) → 𝕜))

Projective space over a nontrivially normed field, with its standard affine charts, is a C^r manifold for every r; for r = ω it is an analytic manifold. Over ℂ this is the standard complex manifold structure on ℂℙⁿ.

instance Projectivization.instIsManifoldReal {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} [NormedAlgebra ℝ 𝕜] (r : WithTop ℕ∞) : IsManifold (modelWithCornersSelf ℝ (Fin n → 𝕜)) r (Projectivization 𝕜 (Fin (n + 1) → 𝕜))

Projective space over a normed ℝ-algebra 𝕜 is, with the same affine charts, a real C^r manifold for every r. Over ℂ this is the underlying real smooth structure of ℂℙⁿ, modelled on 𝓘(ℝ, Fin n → ℂ).

theorem Projectivization.affineOpenPartialHomeomorph_mem_maximalAtlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedSpace 𝕜' (Fin n → 𝕜)] {I : ModelWithCorners 𝕜' (Fin n → 𝕜) (Fin n → 𝕜)} {r : WithTop ℕ∞} [IsManifold I r (Projectivization 𝕜 (Fin (n + 1) → 𝕜))] (i : Fin (n + 1)) : affineOpenPartialHomeomorph i ∈ IsManifold.maximalAtlas I r (Projectivization 𝕜 (Fin (n + 1) → 𝕜))

Each standard affine chart lies in the maximal atlas of any C^r manifold structure on projective space built on its atlas, such as 𝓘(𝕜, Fin n → 𝕜) or, over a normed ℝ-algebra, 𝓘(ℝ, Fin n → 𝕜).

theorem Projectivization.affineOpenPartialHomeomorph_extend_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedSpace 𝕜' (Fin n → 𝕜)] (i : Fin (n + 1)) (x : Projectivization 𝕜 (Fin (n + 1) → 𝕜)) : ↑((affineOpenPartialHomeomorph i).extend (modelWithCornersSelf 𝕜' (Fin n → 𝕜))) x = ↑(affineChart i) x

For a trivial model 𝓘(𝕜', Fin n → 𝕜), the extended standard affine chart of i is the affine chart itself.

theorem Projectivization.affineOpenPartialHomeomorph_extend_mk_single {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedSpace 𝕜' (Fin n → 𝕜)] (i : Fin (n + 1)) : ↑((affineOpenPartialHomeomorph i).extend (modelWithCornersSelf 𝕜' (Fin n → 𝕜))) (mk 𝕜 (Pi.single i 1) ⋯) = 0

For a trivial model 𝓘(𝕜', Fin n → 𝕜), the extended standard affine chart of i sends the coordinate point [eᵢ] to 0.

theorem Projectivization.contMDiffOn_affineChart {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} (i : Fin (n + 1)) (r : WithTop ℕ∞) : ContMDiffOn (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) r (↑(affineChart i)) (affineOpen i)

Each standard affine chart of projective space is a C^r map on its domain.

theorem Projectivization.contMDiff_affineChart_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} (i : Fin (n + 1)) (r : WithTop ℕ∞) : ContMDiff (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) r ↑(affineChart i).symm

The inverse z ↦ [Fin.insertNth i 1 z] of each standard affine chart of projective space is a C^r map.

theorem Projectivization.contMDiff_of_contDiffOn_mk {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : Projectivization 𝕜 (Fin (n + 1) → 𝕜) → E} {F : (Fin (n + 1) → 𝕜) → E} {r : WithTop ℕ∞} (hF : ContDiffOn 𝕜 r F {v : Fin (n + 1) → 𝕜 | v ≠ 0}) (hf : ∀ (v : Fin (n + 1) → 𝕜) (hv : v ≠ 0), f (mk 𝕜 v hv) = F v) : ContMDiff (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 E) r f

A function on projective space with values in a normed space, given in homogeneous coordinates by a function F which is C^r on the nonzero vectors, is C^r; for r = ω it is analytic. On the affine open at i it is z ↦ F (Fin.insertNth i 1 z) read in the chart at i.