Toric varieties

This file defines a toric variety over a ring R as a scheme X with a structure morphism to Spec R.

class AlgebraicGeometry.ToricVariety (R : CommRingCat) (σ : Type u) (X : Scheme) extends CategoryTheory.OverClass X (AlgebraicGeometry.Spec R), Mod_Class (𝔾ₘ[AlgebraicGeometry.Spec R, σ].asOver (AlgebraicGeometry.Spec R)) (X.asOver (AlgebraicGeometry.Spec R)) : Type u

A toric variety of dimension n over a ring R is a scheme X equipped with a dense embedding Tⁿ → X and an action T × X → X extending the standard action T × T → T.

• hom : X ⟶ AlgebraicGeometry.Spec R
• smul : CategoryTheory.MonoidalCategoryStruct.tensorObj (𝔾ₘ[AlgebraicGeometry.Spec R, σ].asOver (AlgebraicGeometry.Spec R)) (X.asOver (AlgebraicGeometry.Spec R)) ⟶ X.asOver (AlgebraicGeometry.Spec R)
• one_smul : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight Mon_Class.one (X.asOver (AlgebraicGeometry.Spec R))) smul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (X.asOver (AlgebraicGeometry.Spec R))).hom
• mul_smul : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight Mon_Class.mul (X.asOver (AlgebraicGeometry.Spec R))) smul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (𝔾ₘ[AlgebraicGeometry.Spec R, σ].asOver (AlgebraicGeometry.Spec R)) (𝔾ₘ[AlgebraicGeometry.Spec R, σ].asOver (AlgebraicGeometry.Spec R)) (X.asOver (AlgebraicGeometry.Spec R))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (𝔾ₘ[AlgebraicGeometry.Spec R, σ].asOver (AlgebraicGeometry.Spec R)) smul) smul)
• torusEmb : 𝔾ₘ[Spec R, σ].asOver (Spec R) ⟶ X.asOver (Spec R)

  The torus embedding.

• isOpenImmersion_torusEmb : IsOpenImmersion torusEmb.left

  The torus embedding is an open immersion.

• isDominant_torusEmb : IsDominant torusEmb.left

  The torus embedding is dominant.

• torusMul_comp_torusEmb : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id (𝔾ₘ[Spec R, σ].asOver (Spec R))) torusEmb) Mod_Class.smul = CategoryTheory.CategoryStruct.comp Mon_Class.mul torusEmb

  The torus action extends the torus multiplication morphism.

noncomputable instance AlgebraicGeometry.instToricVarietySplitTorusSpec {R : CommRingCat} (σ : Type u) : ToricVariety R σ 𝔾ₘ[Spec R, σ]

Equations

• One or more equations did not get rendered due to their size.