Homogeneous-coordinate characters of the projective-space fan

The character of the ratio of homogeneous coordinates X_j / X_k pairs with the ray indexed by l as δ_{jl} - δ_{kl}. On the maximal cone omitting k, these characters, for j ≠ k, freely generate the dual semigroup. Thus its monoid algebra is the polynomial coordinate ring of the standard projective chart X_k ≠ 0, with these characters as its coordinate monomials.

The explicit semigroup equivalence computes the exponent of each ratio by pairing with the corresponding ray. It supplies homogeneous coordinates for affine complex points without choosing a second lattice basis. The character addition law gives the change of ratios X_j / X_l = (X_j / X_k) * (X_k / X_l) on overlaps. The real-linear extension of the ratio character cuts out the intersection of two maximal cones, so face localization identifies the overlap of the affine charts by the nonvanishing of that ratio.

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.projectiveSpaceRatioCharacter {N : Type u_1} {ι : Type u_3} [AddCommGroup N] (b : Module.Basis ι ℤ N) (j k : Option ι) : N →+ ℤ

The integral character of the homogeneous-coordinate ratio X_j / X_k. The index none labels the extra ray, the negative sum of the basis vectors.

@[simp]

theorem TauCeti.Toric.projectiveSpaceRatioCharacter_apply_generator {N : Type u_1} {ι : Type u_3} [AddCommGroup N] [Fintype ι] (b : Module.Basis ι ℤ N) (j k l : Option ι) : (projectiveSpaceRatioCharacter b j k) (projectiveSpaceGenerator b l) = (if j = l then 1 else 0) - if k = l then 1 else 0

A homogeneous-coordinate ratio pairs with the ray generators by the difference of two Kronecker deltas.

@[simp]

theorem TauCeti.Toric.projectiveSpaceRatioCharacter_self {N : Type u_1} {ι : Type u_3} [AddCommGroup N] (b : Module.Basis ι ℤ N) (k : Option ι) : projectiveSpaceRatioCharacter b k k = 0

theorem TauCeti.Toric.projectiveSpaceRatioCharacter_add {N : Type u_1} {ι : Type u_3} [AddCommGroup N] (b : Module.Basis ι ℤ N) (j k l : Option ι) : projectiveSpaceRatioCharacter b j k + projectiveSpaceRatioCharacter b k l = projectiveSpaceRatioCharacter b j l

Multiplication of homogeneous-coordinate ratios is addition of their integral characters.

@[simp]

theorem TauCeti.Toric.projectiveSpaceRatioCharacter_some_none {N : Type u_1} {ι : Type u_3} [AddCommGroup N] (b : Module.Basis ι ℤ N) (j : ι) : projectiveSpaceRatioCharacter b (some j) none = (b.coord j).toAddMonoidHom

The ratio X_j / X_none is the coordinate character of the basis vector b j.

@[simp]

theorem TauCeti.Toric.mem_dualSemigroup_projectiveSpaceCone {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) (S : Set (Option ι)) (m : N →+ ℤ) : m ∈ dualSemigroup hi (projectiveSpaceCone b i S) ↔ ∀ j ∈ S, 0 ≤ m (projectiveSpaceGenerator b j)

Pairing a character with the generators of a projective-space cone tests exactly the inequalities defining its dual semigroup.

theorem TauCeti.Toric.projectiveSpaceRatioCharacter_mem_dualSemigroup {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) (j k : Option ι) {S : Set (Option ι)} (hk : k ∉ S) : projectiveSpaceRatioCharacter b j k ∈ dualSemigroup hi (projectiveSpaceCone b i S)

A homogeneous ratio is regular on a projective cone whenever its denominator ray is omitted. The numerator is allowed to be the denominator, giving the zero character.

theorem TauCeti.Toric.projectiveSpaceCone_inf_ker_ratioCharacter {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 l : Option ι) : projectiveSpaceCone b i {k}ᶜ ⊓ ↑(LinearMap.ker (hi.realCharacter (projectiveSpaceRatioCharacter b l k))) = projectiveSpaceCone b i {k}ᶜ ⊓ projectiveSpaceCone b i {l}ᶜ

The real-linear extension of the ratio character cuts out the intersection of the two maximal cones. The affine chart of this face is the overlap of the projective charts.

theorem TauCeti.Toric.projectiveSpaceCharacter_ext {N : Type u_1} {ι : Type u_3} [AddCommGroup N] [Fintype ι] (b : Module.Basis ι ℤ N) (k : Option ι) {m m' : N →+ ℤ} (h : ∀ (j : Option ι), j ≠ k → m (projectiveSpaceGenerator b j) = m' (projectiveSpaceGenerator b j)) : m = m'

A character is determined by its pairings with all projective-space rays but one.

noncomputable def TauCeti.Toric.projectiveSpaceChartCharacter {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 ι) (j : { j : Option ι // j ≠ k }) : ↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))

The coordinate character X_j / X_k of the maximal projective chart omitting k.

@[simp]

theorem TauCeti.Toric.coe_projectiveSpaceChartCharacter {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 ι) (j : { j : Option ι // j ≠ k }) : ↑(projectiveSpaceChartCharacter b hi k j) = projectiveSpaceRatioCharacter b (↑j) k

noncomputable def TauCeti.Toric.projectiveSpaceDualSemigroupEquiv {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 ι) : ↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ)) ≃+ ({ j : Option ι // j ≠ k } → ℕ)

The dual semigroup of the maximal projective-space cone omitting k is freely generated by the ratios X_j / X_k, for j ≠ k. Exponents are the pairings with the corresponding rays.

@[simp]

theorem TauCeti.Toric.projectiveSpaceDualSemigroupEquiv_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 ι) (m : ↥(dualSemigroup hi (projectiveSpaceCone b i {k}ᶜ))) (j : { j : Option ι // j ≠ k }) : (projectiveSpaceDualSemigroupEquiv b hi k) m j = (↑m (projectiveSpaceGenerator b ↑j)).toNat

The exponent of a ratio is the nonnegative pairing with its ray.

@[simp]

theorem TauCeti.Toric.projectiveSpaceDualSemigroupEquiv_symm_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 ι) (a : { j : Option ι // j ≠ k } → ℕ) : (projectiveSpaceDualSemigroupEquiv b hi k).symm a = ∑ j : { j : Option ι // j ≠ k }, a j • projectiveSpaceChartCharacter b hi k j

The inverse exponent map forms the corresponding sum of homogeneous-coordinate characters.

@[simp]

theorem TauCeti.Toric.projectiveSpaceDualSemigroupEquiv_chartCharacter {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 ι) (j : { j : Option ι // j ≠ k }) : (projectiveSpaceDualSemigroupEquiv b hi k) (projectiveSpaceChartCharacter b hi k j) = Pi.single j 1

Each ratio character is a standard free generator of the dual semigroup.