Homogeneous-ratio transitions for toric projective space

The maximal charts of the projective-space fan cover its analytic realization. A point in the chart normalized by X_k = 1 lies in the chart of l precisely when X_l is nonzero. On this overlap, its coordinates normalized by X_l = 1 are X_j / X_l, including at coordinate hyperplanes. Equality in the actual fan gluing is characterized by these equations.

The computations use the existing face-localization maps and the intersection-cone gluing relation. They identify the standard affine projective transition functions without introducing a second quotient or assuming that every homogeneous coordinate is nonzero.

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.exists_projectiveSpaceMaximalCone_chart {N V : Type u} {ι : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] (b : Module.Basis ι ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (p : ↑((Fan.projectiveSpace b hi).analyticRealization ⋯)) : ∃ (k : Option ι) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))), (CategoryTheory.ConcreteCategory.hom ((Fan.projectiveSpace b hi).analyticAffineChartι ⋯ (Fan.projectiveSpaceMaximalCone b hi k))) x = p

Every point of toric projective space is represented in a maximal cone chart. This includes dimension zero, when there is a single chart and no nonconstant affine coordinate.

theorem TauCeti.Toric.projectiveSpace_chart_mem_range_iff {N V : Type u} {ι : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] (b : Module.Basis ι ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (k l : Option ι) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) : (CategoryTheory.ConcreteCategory.hom ((Fan.projectiveSpace b hi).analyticAffineChartι ⋯ (Fan.projectiveSpaceMaximalCone b hi k))) x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom ((Fan.projectiveSpace b hi).analyticAffineChartι ⋯ (Fan.projectiveSpaceMaximalCone b hi l))) ↔ projectiveSpaceHomogeneousCoordinate b hi k x l ≠ 0

The overlap of two maximal projective charts is exactly the nonvanishing locus of the new normalizing coordinate. The statement also covers the self-overlap.

theorem TauCeti.Toric.projectiveSpace_chart_eq_iff {N V : Type u} {ι : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] (b : Module.Basis ι ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (k l : Option ι) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) (y : AffineSemigroupComplexPoint ↥(dualSemigroup hi (projectiveSpaceCone b i {l}ᶜ))) : (CategoryTheory.ConcreteCategory.hom ((Fan.projectiveSpace b hi).analyticAffineChartι ⋯ (Fan.projectiveSpaceMaximalCone b hi k))) x = (CategoryTheory.ConcreteCategory.hom ((Fan.projectiveSpace b hi).analyticAffineChartι ⋯ (Fan.projectiveSpaceMaximalCone b hi l))) y ↔ projectiveSpaceHomogeneousCoordinate b hi k x l ≠ 0 ∧ ∀ (j : Option ι), projectiveSpaceHomogeneousCoordinate b hi l y j = projectiveSpaceHomogeneousCoordinate b hi k x j / projectiveSpaceHomogeneousCoordinate b hi k x l

Two affine representatives determine the same point of toric projective space exactly when the new denominator is nonzero and all normalized coordinates satisfy the ratio formula. This is equality in the fan realization, including points on coordinate hyperplanes.