Toric projective space and the sphere quotient

The analytic realization of the standard projective-space fan is homeomorphic to complex projective space, modelled by the circle quotient of the unit sphere. The comparison sends the chart normalized at k to its homogeneous-coordinate vector. Conversely, a unit vector whose kth coordinate is nonzero gives the affine ratios X_j / X_k. These formulas hold also on coordinate hyperplanes and in dimension zero.

The comparison uses the affine homogeneous-coordinate charts and their ratio transitions. The sphere quotient is TauCeti.ComplexProjectiveSpace, and normalization uses Mathlib's NormedSpace.normalize.

The comparison matches the toric charts with the standard affine opens of the sphere quotient: the maximal cone omitting the ray k corresponds to the affine open where X_k is nonzero, and on it the homogeneous ratios X_j / X_k are the toric homogeneous coordinates (TauCeti.Toric.preimage_projectiveSpaceHomeomorph_affineOpen, TauCeti.Toric.ratio_projectiveSpaceHomeomorph_analyticAffineChartι, TauCeti.Toric.affineChart_projectiveSpaceHomeomorph_analyticAffineChartι, and TauCeti.Toric.projectiveSpaceHomeomorph_symm_eq_of_mem_affineOpen).

References

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

noncomputable def TauCeti.Toric.projectiveSpaceHomogeneousVector {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Module.Basis (Fin n) ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (k : Option (Fin n)) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) : EuclideanSpace ℂ (Fin (n + 1))

The homogeneous coordinates of an affine toric projective chart, arranged as a vector in ℂⁿ⁺¹. The normalizing coordinate is one, so this vector never vanishes.

@[simp]

theorem TauCeti.Toric.projectiveSpaceHomogeneousVector_apply {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Module.Basis (Fin n) ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (k : Option (Fin n)) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) (j : Fin (n + 1)) : (projectiveSpaceHomogeneousVector b hi k x).ofLp j = projectiveSpaceHomogeneousCoordinate b hi k x ((finSuccEquiv n) j)

The vector coordinates are the normalized homogeneous coordinates of the affine point.

theorem TauCeti.Toric.projectiveSpaceHomogeneousVector_ne_zero {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Module.Basis (Fin n) ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (k : Option (Fin n)) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) : projectiveSpaceHomogeneousVector b hi k x ≠ 0

A normalized homogeneous-coordinate vector is nonzero.

noncomputable def TauCeti.Toric.projectiveSpaceHomeomorph {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Module.Basis (Fin n) ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) : ↑((Fan.projectiveSpace b hi).analyticRealization ⋯) ≃ₜ ComplexProjectiveSpace n

Homogeneous coordinates identify the analytic realization of the standard projective-space fan with complex projective space as the circle quotient of the unit sphere.

theorem TauCeti.Toric.projectiveSpaceHomeomorph_symm_mk {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Module.Basis (Fin n) ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (v : ↑(Metric.sphere 0 1)) (k : Option (Fin n)) (hk : (↑v).ofLp ((finSuccEquiv n).symm k) ≠ 0) : have x := affinePointTopology ((Fan.projectiveSpace b hi).analyticChartGenerators (Fan.projectiveSpaceMaximalCone b hi k)).snd; (projectiveSpaceHomeomorph b hi).symm (ComplexProjectiveSpace.mk n v) = (CategoryTheory.ConcreteCategory.hom ((Fan.projectiveSpace b hi).analyticAffineChartι ⋯ (Fan.projectiveSpaceMaximalCone b hi k))) ((projectiveSpacePointHomeomorph b hi k ((Fan.projectiveSpace b hi).analyticChartGenerators (Fan.projectiveSpaceMaximalCone b hi k)).snd).symm fun (j : { j : Option (Fin n) // j ≠ k }) => (↑v).ofLp ((finSuccEquiv n).symm ↑j) / (↑v).ofLp ((finSuccEquiv n).symm k))

A unit homogeneous vector whose normalizing coordinate is nonzero represents the affine point with the usual homogeneous ratios. The other coordinates are allowed to vanish.

theorem TauCeti.Toric.projectiveSpaceHomeomorph_apply_chart {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Module.Basis (Fin n) ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (k : Option (Fin n)) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) : (projectiveSpaceHomeomorph b hi) ((CategoryTheory.ConcreteCategory.hom ((Fan.projectiveSpace b hi).analyticAffineChartι ⋯ (Fan.projectiveSpaceMaximalCone b hi k))) x) = ComplexProjectiveSpace.mk n ⟨NormedSpace.normalize (projectiveSpaceHomogeneousVector b hi k x), ⋯⟩

On an affine chart, the comparison takes the class of the normalized homogeneous vector. In particular, normalization does not discard points on coordinate hyperplanes.

@[simp]

theorem TauCeti.Toric.ratio_projectiveSpaceHomeomorph_analyticAffineChartι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Module.Basis (Fin n) ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (k : Option (Fin n)) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) (j : Fin (n + 1)) : ComplexProjectiveSpace.ratio ((finSuccEquiv n).symm k) j ((projectiveSpaceHomeomorph b hi) ((CategoryTheory.ConcreteCategory.hom ((Fan.projectiveSpace b hi).analyticAffineChartι ⋯ (Fan.projectiveSpaceMaximalCone b hi k))) x)) = projectiveSpaceHomogeneousCoordinate b hi k x ((finSuccEquiv n) j)

On the toric chart of the maximal cone omitting k, the homogeneous ratios X_j / X_k of the comparison with the sphere quotient are the normalized toric homogeneous coordinates.

theorem TauCeti.Toric.affineChart_projectiveSpaceHomeomorph_analyticAffineChartι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Module.Basis (Fin n) ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (k : Option (Fin n)) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) : ↑(ComplexProjectiveSpace.affineChart ((finSuccEquiv n).symm k)) ((projectiveSpaceHomeomorph b hi) ((CategoryTheory.ConcreteCategory.hom ((Fan.projectiveSpace b hi).analyticAffineChartι ⋯ (Fan.projectiveSpaceMaximalCone b hi k))) x)) = fun (j : Fin n) => projectiveSpaceHomogeneousCoordinate b hi k x ((finSuccEquiv n) (((finSuccEquiv n).symm k).succAbove j))

On the toric chart of the maximal cone omitting k, the standard affine chart of the sphere quotient where X_k is nonzero reads the comparison as the toric homogeneous coordinates.

theorem TauCeti.Toric.preimage_projectiveSpaceHomeomorph_affineOpen {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Module.Basis (Fin n) ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (k : Option (Fin n)) : ⇑(projectiveSpaceHomeomorph b hi) ⁻¹' ComplexProjectiveSpace.affineOpen ((finSuccEquiv n).symm k) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom ((Fan.projectiveSpace b hi).analyticAffineChartι ⋯ (Fan.projectiveSpaceMaximalCone b hi k)))

The standard affine open of complex projective space where the homogeneous coordinate k is nonzero corresponds to the toric chart of the maximal cone omitting the ray k.

theorem TauCeti.Toric.projectiveSpaceHomeomorph_symm_eq_of_mem_affineOpen {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Module.Basis (Fin n) ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (k : Option (Fin n)) {p : ComplexProjectiveSpace n} (hp : p ∈ ComplexProjectiveSpace.affineOpen ((finSuccEquiv n).symm k)) : have x := affinePointTopology ((Fan.projectiveSpace b hi).analyticChartGenerators (Fan.projectiveSpaceMaximalCone b hi k)).snd; (projectiveSpaceHomeomorph b hi).symm p = (CategoryTheory.ConcreteCategory.hom ((Fan.projectiveSpace b hi).analyticAffineChartι ⋯ (Fan.projectiveSpaceMaximalCone b hi k))) ((projectiveSpacePointHomeomorph b hi k ((Fan.projectiveSpace b hi).analyticChartGenerators (Fan.projectiveSpaceMaximalCone b hi k)).snd).symm fun (j : { j : Option (Fin n) // j ≠ k }) => ComplexProjectiveSpace.ratio ((finSuccEquiv n).symm k) ((finSuccEquiv n).symm ↑j) p)

On the standard affine open where X_k is nonzero, the inverse comparison is the point of the toric chart of the maximal cone omitting k with toric coordinates the homogeneous ratios X_j / X_k.