Toric projective space is biholomorphic to complex projective space

The analytic realization of the standard projective-space fan carries the complex structure glued from its affine toric charts. Complex projective space, modelled as the circle quotient of the unit sphere, carries its standard atlas of homogeneous-ratio charts. This file shows that the homogeneous-coordinate comparison TauCeti.Toric.projectiveSpaceHomeomorph between them is a biholomorphism.

The two chart systems match up exactly. The maximal cone omitting the ray k corresponds to the affine open where the homogeneous coordinate k is nonzero, and on it the homogeneous ratios X_j / X_k of the comparison are the toric homogeneous coordinates, which evaluate characters (TauCeti.Toric.preimage_projectiveSpaceHomeomorph_affineOpen and TauCeti.Toric.ratio_projectiveSpaceHomeomorph_analyticAffineChartι). Both directions are therefore holomorphic chart by chart, for the complex structure of any extending basis on the toric charts.

Main declarations

• TauCeti.Toric.contMDiff_projectiveSpaceHomeomorph, TauCeti.Toric.contMDiff_projectiveSpaceHomeomorph_symm: the comparison and its inverse are holomorphic.
• TauCeti.Toric.projectiveSpaceDiffeomorph: the comparison as a biholomorphism.

References

• W. Fulton, Introduction to Toric Varieties, §1.4.
• D. Cox, J. Little and H. Schenck, Toric Varieties, §§3.1 and 3.4.

theorem TauCeti.Toric.contMDiff_projectiveSpaceHomeomorph {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Module.Basis (Fin n) ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (r : WithTop ℕ∞) : have x := (Fan.projectiveSpace b hi).analyticChartedSpace ⋯; ContMDiff (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N) → ℂ)) (modelWithCornersSelf ℂ (Fin n → ℂ)) r ⇑(projectiveSpaceHomeomorph b hi)

The comparison from toric projective space to the sphere quotient is holomorphic.

theorem TauCeti.Toric.contMDiff_projectiveSpaceHomeomorph_symm {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Module.Basis (Fin n) ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (r : WithTop ℕ∞) : have x := (Fan.projectiveSpace b hi).analyticChartedSpace ⋯; ContMDiff (modelWithCornersSelf ℂ (Fin n → ℂ)) (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N) → ℂ)) r ⇑(projectiveSpaceHomeomorph b hi).symm

The inverse comparison from the sphere quotient to toric projective space is holomorphic.

noncomputable def TauCeti.Toric.projectiveSpaceDiffeomorph {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Module.Basis (Fin n) ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (r : WithTop ℕ∞) : have x := (Fan.projectiveSpace b hi).analyticChartedSpace ⋯; Diffeomorph (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N) → ℂ)) (modelWithCornersSelf ℂ (Fin n → ℂ)) (↑((Fan.projectiveSpace b hi).analyticRealization ⋯)) (ComplexProjectiveSpace n) r

Homogeneous coordinates identify the analytic realization of the standard projective-space fan biholomorphically with complex projective space, the circle quotient of the unit sphere with its standard homogeneous-ratio atlas.

@[simp]

theorem TauCeti.Toric.coe_projectiveSpaceDiffeomorph {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Module.Basis (Fin n) ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (r : WithTop ℕ∞) : ⇑(projectiveSpaceDiffeomorph b hi r) = ⇑(projectiveSpaceHomeomorph b hi)

The projective-space biholomorphism is the homogeneous-coordinate comparison.

@[simp]

theorem TauCeti.Toric.coe_projectiveSpaceDiffeomorph_symm {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Module.Basis (Fin n) ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (r : WithTop ℕ∞) : ⇑(Diffeomorph.symm (projectiveSpaceDiffeomorph b hi r)) = ⇑(projectiveSpaceHomeomorph b hi).symm

The inverse projective-space biholomorphism is the inverse homogeneous-coordinate comparison.