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 (CommRingCat.of 𝕜)) : 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 (CommRingCat.of 𝕜)
• torus : Scheme

  The torus

• torusIsOver : (torus 𝕜 X).Over (Spec (CommRingCat.of 𝕜))
• grp_ClassTorus : Grp_Class ((torus 𝕜 X).asOver (Spec (CommRingCat.of 𝕜)))
• mod_ClassTorus : Mod_Class ((torus 𝕜 X).asOver (Spec (CommRingCat.of 𝕜))) (X.asOver (Spec (CommRingCat.of 𝕜)))
• torusIsTorusOver : Scheme.IsTorusOver 𝕜 (torus 𝕜 X)
• torusEmb : torus 𝕜 X ⟶ X

  The torus embedding

• isOver_torusEmb : Scheme.Hom.IsOver (torusEmb 𝕜 X) (Spec (CommRingCat.of 𝕜))
• 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 (CommRingCat.of 𝕜)))) (Scheme.Hom.asOver (torusEmb 𝕜 X) (Spec (CommRingCat.of 𝕜)))) Mod_Class.smul = CategoryTheory.CategoryStruct.comp Mon_Class.mul (Scheme.Hom.asOver (torusEmb 𝕜 X) (Spec (CommRingCat.of 𝕜)))

  The torus action extends the torus multiplication.

noncomputable instance AlgebraicGeometry.ToricVariety.inst {𝕜 : Type u} [Field 𝕜] {T : Scheme} [T.Over (Spec (CommRingCat.of 𝕜))] [Grp_Class (T.asOver (Spec (CommRingCat.of 𝕜)))] [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 (CommRingCat.of 𝕜))] [Grp_Class (T.asOver (Spec (CommRingCat.of 𝕜)))] [Scheme.IsTorusOver 𝕜 T] : torusEmb 𝕜 T = CategoryTheory.CategoryStruct.id T