The toric scheme of the fan of projective space is Proj

Let b be an integral basis of the lattice N, indexed by ι, and let X_j, for j : Option ι, be the homogeneous coordinates of projective space Proj ℂ[X_j], the projective spectrum of the symmetric algebra of Option ι → ℂ. The coordinate X_j corresponds to the ray generator of the fan of projective space indexed by j. This file identifies the toric scheme of that fan, TauCeti.Toric.Fan.algebraicRealization, with Proj ℂ[X_j] over Spec ℂ.

On the affine chart of a cone contained in the maximal cone omitting the ray k, the ratio X_j / X_k is the monomial of the character TauCeti.Toric.projectiveSpaceRatioCharacter. These monomials are homogeneous coordinates normalized by X_k = 1, so they define a morphism from the chart to the standard open D₊(X_k) of Proj. Changing the normalizing coordinate rescales the homogeneous coordinates by a unit, so the morphism does not depend on k, and it is compatible with restriction to faces. The morphisms therefore glue to a morphism from the toric scheme.

On the maximal cone omitting k, the ratios X_j / X_k, for j ≠ k, freely generate the dual semigroup (TauCeti.Toric.projectiveSpaceDualSemigroupEquiv), so the coordinate ring of its chart is the degree-zero part of the localization of ℂ[X_j] away from X_k, and its chart maps isomorphically onto D₊(X_k). Over D₊(X_l), the chart of the maximal cone omitting k is the locus where X_l / X_k does not vanish, which is the chart of the common face of the two maximal cones. Hence the glued morphism is injective, so it is an open immersion, and it is surjective because the opens D₊(X_k) cover Proj.

Main declarations

• TauCeti.Toric.projectiveSpaceHomogeneousCoordinates: the homogeneous coordinates on the chart of a cone contained in the maximal cone omitting k, normalized by X_k = 1.
• TauCeti.Toric.projectiveSpaceAwayEquiv: the ring of the standard chart D₊(X_k) is the coordinate ring of the maximal cone omitting k.
• TauCeti.Toric.projectiveSpaceChartToProj: the morphism from the chart of a cone to Proj, independent of the normalizing coordinate by TauCeti.Toric.projectiveSpaceChartToProj_eq; for a maximal cone it is an open immersion onto D₊(X_k) (TauCeti.Toric.opensRange_projectiveSpaceChartToProj).
• TauCeti.Toric.Fan.projectiveSpaceToProj: the morphism from the toric scheme of the fan of projective space to Proj ℂ[X_j], computed on charts by TauCeti.Toric.Fan.affineToricChartι_comp_projectiveSpaceToProj, a morphism over Spec ℂ (TauCeti.Toric.Fan.isOver_projectiveSpaceToProj).
• TauCeti.Toric.Fan.isIso_projectiveSpaceToProj: this morphism is an isomorphism.

References

• W. Fulton, Introduction to Toric Varieties, §1.4.
• D. Cox, J. Little and H. Schenck, Toric Varieties, §3.1.
• R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977, Proposition II.2.5.

Ratios of homogeneous coordinates

noncomputable def TauCeti.Toric.projectiveSpaceRatioMonomial {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) {σ : PointedCone ℝ V} {k : Option ι} (hσ : σ ≤ projectiveSpaceCone b i {k}ᶜ) (j : Option ι) : affineCoordinateRing hi σ

The monomial of the homogeneous-coordinate ratio X_j / X_k on the affine chart of a cone contained in the maximal cone omitting the ray k.

theorem TauCeti.Toric.projectiveSpaceRatioMonomial_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} {σ : PointedCone ℝ V} {k : Option ι} (hσ : σ ≤ projectiveSpaceCone b i {k}ᶜ) (j : Option ι) : projectiveSpaceRatioMonomial b hi hσ j = MonoidAlgebra.single (Multiplicative.ofAdd ⟨projectiveSpaceRatioCharacter b j k, ⋯⟩) 1

The ratio monomial X_j / X_k is the monomial of the ratio character.

@[simp]

theorem TauCeti.Toric.projectiveSpaceRatioMonomial_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} {σ : PointedCone ℝ V} {k : Option ι} (hσ : σ ≤ projectiveSpaceCone b i {k}ᶜ) : projectiveSpaceRatioMonomial b hi hσ k = 1

The ratio X_k / X_k is 1.

theorem TauCeti.Toric.projectiveSpaceRatioMonomial_mul {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} {σ : PointedCone ℝ V} {k l : Option ι} (hk : σ ≤ projectiveSpaceCone b i {k}ᶜ) (hl : σ ≤ projectiveSpaceCone b i {l}ᶜ) (j : Option ι) : projectiveSpaceRatioMonomial b hi hl k * projectiveSpaceRatioMonomial b hi hk j = projectiveSpaceRatioMonomial b hi hl j

The ratio monomials multiply as the ratios do: (X_k / X_l) (X_j / X_k) = X_j / X_l.

theorem TauCeti.Toric.isUnit_projectiveSpaceRatioMonomial {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} {σ : PointedCone ℝ V} {k l : Option ι} (hk : σ ≤ projectiveSpaceCone b i {k}ᶜ) (hl : σ ≤ projectiveSpaceCone b i {l}ᶜ) : IsUnit (projectiveSpaceRatioMonomial b hi hk l)

On a cone contained in the maximal cones omitting k and l, the ratio X_l / X_k is a unit.

@[simp]

theorem TauCeti.Toric.faceAffineCoordinateRingMap_projectiveSpaceRatioMonomial {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} {σ τ : PointedCone ℝ V} {k : Option ι} (hτσ : τ.IsFaceOf σ) (hσ : σ ≤ projectiveSpaceCone b i {k}ᶜ) (j : Option ι) : (faceAffineCoordinateRingMap hi hτσ) (projectiveSpaceRatioMonomial b hi hσ j) = projectiveSpaceRatioMonomial b hi ⋯ j

Restricting a ratio monomial to a face gives the same ratio monomial.

Homogeneous coordinates on the affine charts

noncomputable def TauCeti.Toric.projectiveSpaceHomogeneousCoordinates {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) {σ : PointedCone ℝ V} {k : Option ι} (hσ : σ ≤ projectiveSpaceCone b i {k}ᶜ) : SymmetricAlgebra ℂ (Option ι → ℂ) →ₐ[ℂ] affineCoordinateRing hi σ

The homogeneous coordinates on the affine chart of a cone contained in the maximal cone omitting the ray k, normalized by X_k = 1: the coordinate X_j is the monomial of the ratio X_j / X_k.

@[simp]

theorem TauCeti.Toric.projectiveSpaceHomogeneousCoordinates_coord {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} {σ : PointedCone ℝ V} [DecidableEq ι] {k : Option ι} (hσ : σ ≤ projectiveSpaceCone b i {k}ᶜ) (j : Option ι) : (projectiveSpaceHomogeneousCoordinates b hi hσ) ((SymmetricAlgebra.ι ℂ (Option ι → ℂ)) (Pi.single j 1)) = projectiveSpaceRatioMonomial b hi hσ j

The homogeneous coordinate X_j is the monomial of the ratio X_j / X_k.

theorem TauCeti.Toric.isUnit_projectiveSpaceHomogeneousCoordinates_coord {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} {σ : PointedCone ℝ V} [DecidableEq ι] {k l : Option ι} (hk : σ ≤ projectiveSpaceCone b i {k}ᶜ) (hl : σ ≤ projectiveSpaceCone b i {l}ᶜ) : IsUnit ((projectiveSpaceHomogeneousCoordinates b hi hk) ((SymmetricAlgebra.ι ℂ (Option ι → ℂ)) (Pi.single l 1)))

On a cone contained in the maximal cone omitting l, the homogeneous coordinate X_l is invertible.

theorem TauCeti.Toric.projectiveSpaceHomogeneousCoordinates_ι_eq_mul {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} {σ : PointedCone ℝ V} {k l : Option ι} (hk : σ ≤ projectiveSpaceCone b i {k}ᶜ) (hl : σ ≤ projectiveSpaceCone b i {l}ᶜ) (m : Option ι → ℂ) : (projectiveSpaceHomogeneousCoordinates b hi hl) ((SymmetricAlgebra.ι ℂ (Option ι → ℂ)) m) = projectiveSpaceRatioMonomial b hi hl k * (projectiveSpaceHomogeneousCoordinates b hi hk) ((SymmetricAlgebra.ι ℂ (Option ι → ℂ)) m)

Changing the normalizing coordinate from X_k to X_l multiplies the linear homogeneous coordinates by the ratio X_k / X_l.

theorem TauCeti.Toric.projectiveSpaceHomogeneousCoordinates_eq_pow_mul {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} {σ : PointedCone ℝ V} {k l : Option ι} (hk : σ ≤ projectiveSpaceCone b i {k}ᶜ) (hl : σ ≤ projectiveSpaceCone b i {l}ᶜ) {n : ℕ} {a : SymmetricAlgebra ℂ (Option ι → ℂ)} (ha : a ∈ SymmetricAlgebra.homogeneousSubmodule ℂ (Option ι → ℂ) n) : (projectiveSpaceHomogeneousCoordinates b hi hl) a = projectiveSpaceRatioMonomial b hi hl k ^ n * (projectiveSpaceHomogeneousCoordinates b hi hk) a

Changing the normalizing coordinate from X_k to X_l multiplies the homogeneous polynomials of degree n by the n-th power of the ratio X_k / X_l.

@[simp]

theorem TauCeti.Toric.faceAffineCoordinateRingMap_comp_projectiveSpaceHomogeneousCoordinates {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} {σ τ : PointedCone ℝ V} {k : Option ι} (hτσ : τ.IsFaceOf σ) (hσ : σ ≤ projectiveSpaceCone b i {k}ᶜ) : (faceAffineCoordinateRingMap hi hτσ).comp (projectiveSpaceHomogeneousCoordinates b hi hσ) = projectiveSpaceHomogeneousCoordinates b hi ⋯

Restricting the homogeneous coordinates of a chart to a face gives the homogeneous coordinates of the face.

The chart of a maximal cone

noncomputable def TauCeti.Toric.projectiveSpaceAwayEquiv {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) [DecidableEq ι] (k : Option ι) : HomogeneousLocalization.Away (SymmetricAlgebra.homogeneousSubmodule ℂ (Option ι → ℂ)) ((SymmetricAlgebra.ι ℂ (Option ι → ℂ)) (Pi.single k 1)) ≃ₐ[ℂ] affineCoordinateRing hi (projectiveSpaceCone b i {k}ᶜ)

The affine chart of the maximal cone omitting k is the standard chart D₊(X_k) of projective space: the ring of D₊(X_k), the degree-zero part of the localization of the homogeneous coordinate ring away from X_k, is the coordinate ring of the cone. A fraction a / X_kⁿ goes to the value of a at the homogeneous coordinates with X_k = 1.

@[simp]

theorem TauCeti.Toric.projectiveSpaceAwayEquiv_mk {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) [DecidableEq ι] (k : Option ι) {n : ℕ} {a : SymmetricAlgebra ℂ (Option ι → ℂ)} (ha : a ∈ SymmetricAlgebra.homogeneousSubmodule ℂ (Option ι → ℂ) (n • 1)) : (projectiveSpaceAwayEquiv b hi k) (HomogeneousLocalization.Away.mk (SymmetricAlgebra.homogeneousSubmodule ℂ (Option ι → ℂ)) ⋯ n a ha) = (projectiveSpaceHomogeneousCoordinates b hi ⋯) a

The isomorphism projectiveSpaceAwayEquiv sends a / X_kⁿ to the value of a at the homogeneous coordinates with X_k = 1.

theorem TauCeti.Toric.projectiveSpaceAwayEquiv_toRingHom {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) [DecidableEq ι] (k : Option ι) : (↑(projectiveSpaceAwayEquiv b hi k)).toRingHom = HomogeneousLocalization.Away.lift (SymmetricAlgebra.homogeneousSubmodule ℂ (Option ι → ℂ)) (projectiveSpaceHomogeneousCoordinates b hi ⋯).toRingHom ⋯

The isomorphism projectiveSpaceAwayEquiv is the homomorphism Away.lift induced by the homogeneous coordinates with X_k = 1.

@[simp]

theorem TauCeti.Toric.projectiveSpaceAwayEquiv_symm_projectiveSpaceRatioMonomial {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) [DecidableEq ι] (k j : Option ι) : (projectiveSpaceAwayEquiv b hi k).symm (projectiveSpaceRatioMonomial b hi ⋯ j) = HomogeneousLocalization.Away.mk (SymmetricAlgebra.homogeneousSubmodule ℂ (Option ι → ℂ)) ⋯ 1 ((SymmetricAlgebra.ι ℂ (Option ι → ℂ)) (Pi.single j 1)) ⋯

The inverse of projectiveSpaceAwayEquiv sends the monomial of the ratio X_j / X_k to the fraction X_j / X_k.

The morphism to Proj

noncomputable def TauCeti.Toric.projectiveSpaceChartToProj {N ι : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) {σ : PointedCone ℝ V} {k : Option ι} (hσ : σ ≤ projectiveSpaceCone b i {k}ᶜ) : affineToricScheme hi σ ⟶ AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule ℂ (Option ι → ℂ))

The morphism from the affine toric scheme of a cone contained in the maximal cone omitting k to projective space Proj ℂ[X_j]: the point with the homogeneous coordinates of the chart, read on the standard chart D₊(X_k). By projectiveSpaceChartToProj_eq it does not depend on k.

theorem TauCeti.Toric.projectiveSpaceChartToProj_eq {N ι : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] [DecidableEq ι] {b : Module.Basis ι ℤ N} {i : N →+ V} {hi : IsIntegralLattice i} {σ : PointedCone ℝ V} {k l : Option ι} (hk : σ ≤ projectiveSpaceCone b i {k}ᶜ) (hl : σ ≤ projectiveSpaceCone b i {l}ᶜ) : projectiveSpaceChartToProj b hi hk = projectiveSpaceChartToProj b hi hl

The morphism projectiveSpaceChartToProj does not depend on the normalizing coordinate.

@[simp]

theorem TauCeti.Toric.faceAffineToricSchemeMap_comp_projectiveSpaceChartToProj {N ι : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] [DecidableEq ι] {b : Module.Basis ι ℤ N} {i : N →+ V} {hi : IsIntegralLattice i} {σ τ : PointedCone ℝ V} {k : Option ι} (hτσ : τ.IsFaceOf σ) (hσ : σ ≤ projectiveSpaceCone b i {k}ᶜ) : CategoryTheory.CategoryStruct.comp (faceAffineToricSchemeMap hi hτσ) (projectiveSpaceChartToProj b hi hσ) = projectiveSpaceChartToProj b hi ⋯

Restricting projectiveSpaceChartToProj to the chart of a face gives the morphism of the face.

@[simp]

theorem TauCeti.Toric.faceAffineToricSchemeMap_comp_projectiveSpaceChartToProj_assoc {N ι : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] [DecidableEq ι] {b : Module.Basis ι ℤ N} {i : N →+ V} {hi : IsIntegralLattice i} {σ τ : PointedCone ℝ V} {k : Option ι} (hτσ : τ.IsFaceOf σ) (hσ : σ ≤ projectiveSpaceCone b i {k}ᶜ) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule ℂ (Option ι → ℂ)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (faceAffineToricSchemeMap hi hτσ) (CategoryTheory.CategoryStruct.comp (projectiveSpaceChartToProj b hi hσ) h) = CategoryTheory.CategoryStruct.comp (projectiveSpaceChartToProj b hi ⋯) h

Restricting projectiveSpaceChartToProj to the chart of a face gives the morphism of the face.

theorem TauCeti.Toric.projectiveSpaceChartToProj_self {N ι : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] [DecidableEq ι] {b : Module.Basis ι ℤ N} {i : N →+ V} {hi : IsIntegralLattice i} (k : Option ι) : projectiveSpaceChartToProj b hi ⋯ = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (↑(projectiveSpaceAwayEquiv b hi k)).toRingHom)) (AlgebraicGeometry.Proj.awayι (SymmetricAlgebra.homogeneousSubmodule ℂ (Option ι → ℂ)) ((SymmetricAlgebra.ι ℂ (Option ι → ℂ)) (Pi.single k 1)) ⋯ ⋯)

On the chart of the maximal cone omitting k, the morphism to Proj is the spectrum of the isomorphism projectiveSpaceAwayEquiv followed by the standard chart D₊(X_k).

instance TauCeti.Toric.isOpenImmersion_projectiveSpaceChartToProj {N ι : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] [DecidableEq ι] {b : Module.Basis ι ℤ N} {i : N →+ V} {hi : IsIntegralLattice i} (k : Option ι) : AlgebraicGeometry.IsOpenImmersion (projectiveSpaceChartToProj b hi ⋯)

The affine chart of the maximal cone omitting k is an open subscheme of projective space.

theorem TauCeti.Toric.opensRange_projectiveSpaceChartToProj {N ι : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] [DecidableEq ι] {b : Module.Basis ι ℤ N} {i : N →+ V} {hi : IsIntegralLattice i} (k : Option ι) : AlgebraicGeometry.Scheme.Hom.opensRange (projectiveSpaceChartToProj b hi ⋯) = AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule ℂ (Option ι → ℂ)) ((SymmetricAlgebra.ι ℂ (Option ι → ℂ)) (Pi.single k 1))

The affine chart of the maximal cone omitting k is the standard open D₊(X_k) of projective space.

theorem TauCeti.Toric.projectiveSpaceChartToProj_preimage_basicOpen {N ι : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] [DecidableEq ι] {b : Module.Basis ι ℤ N} {i : N →+ V} {hi : IsIntegralLattice i} (k l : Option ι) : (TopologicalSpace.Opens.map (projectiveSpaceChartToProj b hi ⋯).base).obj (AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule ℂ (Option ι → ℂ)) ((SymmetricAlgebra.ι ℂ (Option ι → ℂ)) (Pi.single l 1))) = PrimeSpectrum.basicOpen (projectiveSpaceRatioMonomial b hi ⋯ l)

In the chart of the maximal cone omitting k, the standard open D₊(X_l) of projective space is the locus where the ratio X_l / X_k does not vanish.

The toric scheme of the fan of projective space

noncomputable def TauCeti.Toric.Fan.projectiveSpaceToProj {N ι : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℤ N) {i : N →+ V} (hi : IsIntegralLattice i) : (projectiveSpace b hi).algebraicRealization ⟶ AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule ℂ (Option ι → ℂ))

The morphism from the toric scheme of the fan of projective space to projective space Proj ℂ[X_j], given on the chart of each cone by its homogeneous coordinates.

theorem TauCeti.Toric.Fan.affineToricChartι_comp_projectiveSpaceToProj {N ι : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] [DecidableEq ι] {b : Module.Basis ι ℤ N} {i : N →+ V} {hi : IsIntegralLattice i} (σ : ↑(projectiveSpace b hi).cones) {k : Option ι} (hσ : ↑σ ≤ projectiveSpaceCone b i {k}ᶜ) : CategoryTheory.CategoryStruct.comp ((projectiveSpace b hi).affineToricChartι σ) (projectiveSpaceToProj b hi) = projectiveSpaceChartToProj b hi hσ

On the chart of a cone contained in the maximal cone omitting k, the morphism to Proj is given by the homogeneous coordinates normalized by X_k = 1.

theorem TauCeti.Toric.Fan.affineToricChartι_comp_projectiveSpaceToProj_assoc {N ι : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] [DecidableEq ι] {b : Module.Basis ι ℤ N} {i : N →+ V} {hi : IsIntegralLattice i} (σ : ↑(projectiveSpace b hi).cones) {k : Option ι} (hσ : ↑σ ≤ projectiveSpaceCone b i {k}ᶜ) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule ℂ (Option ι → ℂ)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((projectiveSpace b hi).affineToricChartι σ) (CategoryTheory.CategoryStruct.comp (projectiveSpaceToProj b hi) h) = CategoryTheory.CategoryStruct.comp (projectiveSpaceChartToProj b hi hσ) h

On the chart of a cone contained in the maximal cone omitting k, the morphism to Proj is given by the homogeneous coordinates normalized by X_k = 1.

instance TauCeti.Toric.Fan.isOver_projectiveSpaceToProj {N ι : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] [DecidableEq ι] {b : Module.Basis ι ℤ N} {i : N →+ V} {hi : IsIntegralLattice i} : AlgebraicGeometry.Scheme.Hom.IsOver (projectiveSpaceToProj b hi) (AlgebraicGeometry.Spec ↧ℂ)

The morphism from the toric scheme of the fan of projective space to Proj is a morphism over Spec ℂ.

instance TauCeti.Toric.Fan.isOpenImmersion_projectiveSpaceToProj {N ι : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] [DecidableEq ι] {b : Module.Basis ι ℤ N} {i : N →+ V} {hi : IsIntegralLattice i} : AlgebraicGeometry.IsOpenImmersion (projectiveSpaceToProj b hi)

The morphism from the toric scheme of the fan of projective space to Proj is an open immersion: it is injective, and an open immersion on the chart of every maximal cone.

instance TauCeti.Toric.Fan.isIso_projectiveSpaceToProj {N ι : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] [DecidableEq ι] {b : Module.Basis ι ℤ N} {i : N →+ V} {hi : IsIntegralLattice i} : CategoryTheory.IsIso (projectiveSpaceToProj b hi)

The toric scheme of the fan of projective space is projective space Proj ℂ[X_j].