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} (n : ℕ) (X : CategoryTheory.Over (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.

• torusEmb : CategoryTheory.Over.mk ((Spec R).SplitTorus (ULift.{u, 0} (Fin n)) ↘ Spec R) ⟶ X

  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.

• torusAct : Action_Class (CategoryTheory.Over.mk ((Spec R).SplitTorus (ULift.{u, 0} (Fin n)) ↘ Spec R)) X

  The torus action on a toric variety.

• torusMul_comp_torusEmb : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.Over.mk ((Spec R).SplitTorus (ULift.{u, 0} (Fin n)) ↘ Spec R))) torusEmb) γ = CategoryTheory.CategoryStruct.comp Mon_Class.mul torusEmb

  The torus action extends the torus multiplication morphism.

noncomputable instance AlgebraicGeometry.instToricVarietyMkSchemeOverSplitTorusSpecULiftFinInferInstanceOverClass {R : CommRingCat} (n : ℕ) : ToricVariety n (CategoryTheory.Over.mk ((Spec R).SplitTorus (ULift.{u, 0} (Fin n)) ↘ Spec R))

Equations

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