Homogeneous coordinates on affine charts of toric projective space

The maximal cone omitting the ray k has a complex-point chart homeomorphic to ℂ^n. The coordinate indexed by j ≠ k is evaluation of the character of X_j / X_k. Conversely every character monomial is the product of these coordinates with exponents given by its pairings with the rays. This description holds on the whole affine chart, including its coordinate hyperplanes, and for any finite semigroup generating family. The identification is biholomorphic for the cone complex structure of any extending basis. Normalized homogeneous coordinates adjoin the constant normalizing coordinate one; they determine the affine point.

These explicit affine coordinates are needed to compare the gluing of the projective-space fan with the usual homogeneous-coordinate construction of complex projective space.

The homeomorphisms specialize TauCeti.Toric.regularAffinePointHomeomorph using the explicit homogeneous-coordinate splitting of the dual semigroup.

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.projectiveSpacePointHomeomorph {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] (b : Module.Basis ι ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (k : Option ι) {r : ℕ} (g : AddGeneratingFamily (↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) r) : AffineSemigroupComplexPoint ↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ)) ≃ₜ ({ j : Option ι // j ≠ k } → ℂ)

The complex-point chart omitting the ray k, in the homogeneous ratios X_j / X_k. The topology may be defined using any finite generating family of its dual semigroup.

@[simp]

theorem TauCeti.Toric.projectiveSpacePointHomeomorph_apply {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] (b : Module.Basis ι ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (k : Option ι) {r : ℕ} (g : AddGeneratingFamily (↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) r) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) (j : { j : Option ι // j ≠ k }) : (projectiveSpacePointHomeomorph b hi k g) x j = x (MonoidAlgebra.single (Multiplicative.ofAdd (projectiveSpaceChartCharacter b hi k j)) 1)

Each affine coordinate evaluates the monomial of the corresponding homogeneous ratio.

@[simp]

theorem TauCeti.Toric.projectiveSpacePointHomeomorph_symm_apply_single {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] (b : Module.Basis ι ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (k : Option ι) {r : ℕ} (g : AddGeneratingFamily (↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) r) (z : { j : Option ι // j ≠ k } → ℂ) (m : ↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) : have x := affinePointTopology g; ((projectiveSpacePointHomeomorph b hi k g).symm z) (MonoidAlgebra.single (Multiplicative.ofAdd m) 1) = ∏ j : { j : Option ι // j ≠ k }, z j ^ (↑m (projectiveSpaceGenerator b ↑j)).toNat

The point with prescribed homogeneous ratios evaluates every character by the associated ordinary monomial. All exponents are nonnegative; coordinates may vanish.

noncomputable def TauCeti.Toric.projectiveSpaceHomogeneousCoordinate {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] (b : Module.Basis ι ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (k : Option ι) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) (j : Option ι) : ℂ

Homogeneous coordinates of an affine point, normalized so that the coordinate of the omitted ray is one. The remaining coordinates can vanish.

theorem TauCeti.Toric.projectiveSpaceHomogeneousCoordinate_def {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] (b : Module.Basis ι ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (k : Option ι) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) (j : Option ι) : projectiveSpaceHomogeneousCoordinate b hi k x j = x (MonoidAlgebra.single (Multiplicative.ofAdd ⟨projectiveSpaceRatioCharacter b j k, ⋯⟩) 1)

A normalized homogeneous coordinate evaluates the corresponding ratio character.

@[simp]

theorem TauCeti.Toric.projectiveSpaceHomogeneousCoordinate_self {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] (b : Module.Basis ι ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (k : Option ι) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) : projectiveSpaceHomogeneousCoordinate b hi k x k = 1

The homogeneous coordinate used to normalize an affine chart is one.

theorem TauCeti.Toric.projectiveSpacePointHomeomorph_eq_homogeneousCoordinate {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] (b : Module.Basis ι ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (k : Option ι) {r : ℕ} (g : AddGeneratingFamily (↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) r) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) (j : { j : Option ι // j ≠ k }) : (projectiveSpacePointHomeomorph b hi k g) x j = projectiveSpaceHomogeneousCoordinate b hi k x ↑j

The affine coordinates are the homogeneous coordinates other than the normalizing one.

theorem TauCeti.Toric.projectiveSpaceHomogeneousCoordinate_injective {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] (b : Module.Basis ι ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (k : Option ι) : Function.Injective (projectiveSpaceHomogeneousCoordinate b hi k)

The normalized homogeneous coordinates determine an affine point.

noncomputable def TauCeti.Toric.projectiveSpacePointDiffeomorph {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] (b : Module.Basis ι ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (k : Option ι) {p q r : ℕ} {B : Module.Basis (ToricRay (projectiveSpaceCone b i {k}ᶜ) ⊕ Fin q) ℤ N} (hB : ∀ (ρ : ToricRay (projectiveSpaceCone b i {k}ᶜ)), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay (projectiveSpaceCone b i {k}ᶜ) ≃ Fin p) (g : AddGeneratingFamily (↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) r) (n : WithTop ℕ∞) : let x := affinePointTopology g; have x_1 := coneChartedSpace hi ⋯ hB κ g; Diffeomorph (modelWithCornersSelf ℂ ((Fin p → ℂ) × (Fin q → ℂ))) (modelWithCornersSelf ℂ ({ j : Option ι // j ≠ k } → ℂ)) (AffineSemigroupComplexPoint ↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) ({ j : Option ι // j ≠ k } → ℂ) n

Homogeneous ratios identify the maximal affine chart biholomorphically with complex affine space, for the regular-cone complex structure of any extending integral basis.

@[simp]

theorem TauCeti.Toric.projectiveSpacePointDiffeomorph_toHomeomorph {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] (b : Module.Basis ι ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) (k : Option ι) {p q r : ℕ} {B : Module.Basis (ToricRay (projectiveSpaceCone b i {k}ᶜ) ⊕ Fin q) ℤ N} (hB : ∀ (ρ : ToricRay (projectiveSpaceCone b i {k}ᶜ)), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay (projectiveSpaceCone b i {k}ᶜ) ≃ Fin p) (g : AddGeneratingFamily (↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) r) (n : WithTop ℕ∞) : have x := affinePointTopology g; have x := coneChartedSpace hi ⋯ hB κ g; Diffeomorph.toHomeomorph (projectiveSpacePointDiffeomorph b hi k hB κ g n) = projectiveSpacePointHomeomorph b hi k g

The biholomorphic homogeneous-coordinate chart has the specified underlying homeomorphism.