The standard complex manifold structure on complex projective space

The homogeneous-ratio charts on the circle quotient of the unit sphere form the standard complex atlas on ComplexProjectiveSpace n. Their transition maps are ratios of affine coordinate functions with a nonzero denominator, hence holomorphic. This construction uses only the sphere quotient and its explicit homogeneous-coordinate charts.

These charts provide the usual complex structure with which to compare realizations of the projective-space fan.

References

• D. Cox, J. Little and H. Schenck, Toric Varieties, §§3.1 and 3.4.

@[instance_reducible]

noncomputable instance TauCeti.ComplexProjectiveSpace.instChartedSpace {n : ℕ} : ChartedSpace (Fin n → ℂ) (ComplexProjectiveSpace n)

The standard atlas consists of the n + 1 homogeneous-ratio charts.

@[simp]

theorem TauCeti.ComplexProjectiveSpace.mem_atlas_iff {n : ℕ} (e : OpenPartialHomeomorph (ComplexProjectiveSpace n) (Fin n → ℂ)) : e ∈ atlas (Fin n → ℂ) (ComplexProjectiveSpace n) ↔ ∃ (k : Fin (n + 1)), affineChart k = e

Membership in the standard projective atlas means being a homogeneous-ratio chart.

theorem TauCeti.ComplexProjectiveSpace.contDiffOn_affineChart_transition {n : ℕ} (k l : Fin (n + 1)) (r : WithTop ℕ∞) : ContDiffOn ℂ r (↑((affineChart k).symm.trans (affineChart l))) ((affineChart k).symm.trans (affineChart l)).source

Homogeneous-ratio transitions are holomorphic wherever the new denominator is nonzero.

instance TauCeti.ComplexProjectiveSpace.instIsManifold {n : ℕ} (r : WithTop ℕ∞) : IsManifold (modelWithCornersSelf ℂ (Fin n → ℂ)) r (ComplexProjectiveSpace n)

Complex projective space with its standard homogeneous-coordinate atlas is a complex manifold, at every differentiability order.

theorem TauCeti.ComplexProjectiveSpace.contMDiffOn_affineChart {n : ℕ} (k : Fin (n + 1)) (r : WithTop ℕ∞) : ContMDiffOn (modelWithCornersSelf ℂ (Fin n → ℂ)) (modelWithCornersSelf ℂ (Fin n → ℂ)) r (↑(affineChart k)) (affineOpen k)

Each homogeneous-ratio chart is holomorphic on its affine open.

theorem TauCeti.ComplexProjectiveSpace.contMDiff_affineChart_symm {n : ℕ} (k : Fin (n + 1)) (r : WithTop ℕ∞) : ContMDiff (modelWithCornersSelf ℂ (Fin n → ℂ)) (modelWithCornersSelf ℂ (Fin n → ℂ)) r ↑(affineChart k).symm

The inverse of each homogeneous-ratio chart is holomorphic.