Toric varieties

This file defines a toric variety with torus T over a scheme S as a scheme X with an dominant open embedding T → X over S and an action T × X → X extending the multiplication on T.

class AlgebraicGeometry.ToricVariety (𝕜 : Type u) [Field 𝕜] (X : Scheme) extends CategoryTheory.OverClass X (AlgebraicGeometry.Spec { carrier := 𝕜, commRing := Field.toEuclideanDomain.toCommRing }) : Type (u + 1)

A toric variety over a scheme S is a scheme X equipped with a torus T, a dense embedding T → X and an action T × X → X extending the standard action T × T → T.

• hom : X ⟶ AlgebraicGeometry.Spec { carrier := 𝕜, commRing := Field.toEuclideanDomain.toCommRing }
• torus : Scheme

  The torus

• torusIsOver : (torus 𝕜 X).Over (Spec { carrier := 𝕜, commRing := Field.toEuclideanDomain.toCommRing })
• grpObjTorus : CategoryTheory.GrpObj ((torus 𝕜 X).asOver (Spec { carrier := 𝕜, commRing := Field.toEuclideanDomain.toCommRing }))
• modObjTorus : CategoryTheory.ModObj ((torus 𝕜 X).asOver (Spec { carrier := 𝕜, commRing := Field.toEuclideanDomain.toCommRing })) (X.asOver (Spec { carrier := 𝕜, commRing := Field.toEuclideanDomain.toCommRing }))
• torusIsTorusOver : Scheme.IsTorusOver 𝕜 (torus 𝕜 X)
• torusEmb : torus 𝕜 X ⟶ X

  The torus embedding

• isOver_torusEmb : Scheme.Hom.IsOver (torusEmb 𝕜 X) (Spec { carrier := 𝕜, commRing := Field.toEuclideanDomain.toCommRing })
• isOpenImmersion_torusEmb : IsOpenImmersion (torusEmb 𝕜 X)

  The torus embedding is an open immersion.

• isDominant_torusEmb : IsDominant (torusEmb 𝕜 X)

  The torus embedding is dominant.

• torusMul_comp_torusEmb : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id ((torus 𝕜 X).asOver (Spec { carrier := 𝕜, commRing := Field.toEuclideanDomain.toCommRing }))) (Scheme.Hom.asOver (torusEmb 𝕜 X) (Spec { carrier := 𝕜, commRing := Field.toEuclideanDomain.toCommRing }))) CategoryTheory.ModObj.smul = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (Scheme.Hom.asOver (torusEmb 𝕜 X) (Spec { carrier := 𝕜, commRing := Field.toEuclideanDomain.toCommRing }))

  The torus action extends the torus multiplication.

noncomputable instance AlgebraicGeometry.ToricVariety.inst {𝕜 : Type u} [Field 𝕜] {T : Scheme} [T.Over (Spec { carrier := 𝕜, commRing := Field.toEuclideanDomain.toCommRing })] [CategoryTheory.GrpObj (T.asOver (Spec { carrier := 𝕜, commRing := Field.toEuclideanDomain.toCommRing }))] [Scheme.IsTorusOver 𝕜 T] : ToricVariety 𝕜 T

A torus T is a toric variety over itself.

Equations

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

@[simp]

theorem AlgebraicGeometry.ToricVariety.torusEmb_self {𝕜 : Type u} [Field 𝕜] (T : Scheme) [T.Over (Spec { carrier := 𝕜, commRing := Field.toEuclideanDomain.toCommRing })] [CategoryTheory.GrpObj (T.asOver (Spec { carrier := 𝕜, commRing := Field.toEuclideanDomain.toCommRing }))] [Scheme.IsTorusOver 𝕜 T] : torusEmb 𝕜 T = CategoryTheory.CategoryStruct.id T