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 (CategoryTheory.Over.mk ((AlgebraicGeometry.Spec R).SplitTorus σ ↘ AlgebraicGeometry.Spec R)) (CategoryTheory.Over.mk (X ↘ 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 (CategoryTheory.Over.mk ((AlgebraicGeometry.Spec R).SplitTorus σ ↘ AlgebraicGeometry.Spec R)) (CategoryTheory.Over.mk (X ↘ AlgebraicGeometry.Spec R)) ⟶ CategoryTheory.Over.mk (X ↘ AlgebraicGeometry.Spec R)
• one_smul : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight Mon_Class.one (CategoryTheory.Over.mk (X ↘ AlgebraicGeometry.Spec R))) smul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.Over.mk (X ↘ AlgebraicGeometry.Spec R))).hom
• mul_smul : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight Mon_Class.mul (CategoryTheory.Over.mk (X ↘ AlgebraicGeometry.Spec R))) smul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.Over.mk ((AlgebraicGeometry.Spec R).SplitTorus σ ↘ AlgebraicGeometry.Spec R)) (CategoryTheory.Over.mk ((AlgebraicGeometry.Spec R).SplitTorus σ ↘ AlgebraicGeometry.Spec R)) (CategoryTheory.Over.mk (X ↘ AlgebraicGeometry.Spec R))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.Over.mk ((AlgebraicGeometry.Spec R).SplitTorus σ ↘ AlgebraicGeometry.Spec R)) smul) smul)
• torusEmb : CategoryTheory.Over.mk ((Spec R).SplitTorus σ ↘ Spec R) ⟶ CategoryTheory.Over.mk (X ↘ 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 (CategoryTheory.Over.mk ((Spec R).SplitTorus σ ↘ Spec R))) torusEmb) Mod_Class.smul = CategoryTheory.CategoryStruct.comp Mon_Class.mul torusEmb

  The torus action extends the torus multiplication morphism.

noncomputable instance AlgebraicGeometry.instToricVarietyLeftSchemeDiscretePUnitMkOverSplitTorusSpecInferInstanceOverClass {R : CommRingCat} (σ : Type u) : ToricVariety R σ (CategoryTheory.Over.mk ((Spec R).SplitTorus σ ↘ Spec R)).left

Equations

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