Affine toric schemes of cones

The affine toric scheme associated to a cone is the spectrum of the complex monoid algebra of its dual semigroup. A compatible map of lattices carrying one cone into another induces a map of dual semigroups in the opposite direction, hence a homomorphism of coordinate rings and, after applying Spec, a morphism of affine toric schemes in the original direction.

This file fixes those carriers and proves their identity and composition laws. No finite generation hypothesis is needed to form the monoid algebra or its spectrum. Finite generation of the dual semigroup is the separate input that will later show that this affine scheme is of finite type.

Main declarations

• TauCeti.Toric.affineCoordinateRing: the complex monoid algebra of a dual semigroup.
• TauCeti.Toric.affineToricScheme: its affine spectrum.
• TauCeti.Toric.affineCoordinateRingMap: the contravariant coordinate-ring map induced by a compatible map of lattice cones.
• TauCeti.Toric.affineToricSchemeMap: the resulting covariant morphism of affine schemes.

References

The construction follows §1.2 of W. Fulton, Introduction to Toric Varieties, and §§1.1–1.3 of D. Cox, J. Little and H. Schenck, Toric Varieties.

Coordinate rings

@[reducible, inline]

abbrev TauCeti.Toric.affineCoordinateRing {V : Type u_1} [AddCommGroup V] [Module ℝ V] {N : Type u_4} [AddCommGroup N] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) : Type u_4

The coordinate ring of the affine toric chart of a cone: the complex monoid algebra of its dual semigroup.

noncomputable def TauCeti.Toric.affineCoordinateRingMap {V : Type u_1} {V' : Type u_2} [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {σ : PointedCone ℝ V} {τ : PointedCone ℝ V'} {N : Type u_4} {N' : Type u_5} [AddCommGroup N] [AddCommGroup N'] {i : N →+ V} {i' : N' →+ V'} (hi : IsIntegralLattice i) (hi' : IsIntegralLattice i') (f : N →+ N') (g : V →ₗ[ℝ] V') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) : affineCoordinateRing hi' τ →ₐ[ℂ] affineCoordinateRing hi σ

A compatible map of lattices carrying σ into τ induces the homomorphism from the coordinate ring of τ to the coordinate ring of σ.

@[simp]

theorem TauCeti.Toric.affineCoordinateRingMap_single {V : Type u_1} {V' : Type u_2} [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {σ : PointedCone ℝ V} {τ : PointedCone ℝ V'} {N : Type u_4} {N' : Type u_5} [AddCommGroup N] [AddCommGroup N'] {i : N →+ V} {i' : N' →+ V'} (hi : IsIntegralLattice i) (hi' : IsIntegralLattice i') (f : N →+ N') (g : V →ₗ[ℝ] V') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) (m : ↥(dualSemigroup hi' τ)) (z : ℂ) : (affineCoordinateRingMap hi hi' f g hfg hστ) (MonoidAlgebra.single (Multiplicative.ofAdd m) z) = MonoidAlgebra.single (Multiplicative.ofAdd ((dualSemigroupMap hi hi' f g hfg hστ) m)) z

The coordinate-ring map sends the monomial of a character to the monomial of its pullback.

@[simp]

theorem TauCeti.Toric.affineCoordinateRingMap_id {V : Type u_1} [AddCommGroup V] [Module ℝ V] {N : Type u_4} [AddCommGroup N] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) : affineCoordinateRingMap hi hi (AddMonoidHom.id N) LinearMap.id ⋯ ⋯ = AlgHom.id ℂ (affineCoordinateRing hi σ)

The identity map of a lattice cone induces the identity of its coordinate ring.

@[simp]

theorem TauCeti.Toric.affineCoordinateRingMap_comp {V : Type u_1} {V' : Type u_2} {V'' : Type u_3} [AddCommGroup V] [AddCommGroup V'] [AddCommGroup V''] [Module ℝ V] [Module ℝ V'] [Module ℝ V''] {σ : PointedCone ℝ V} {τ : PointedCone ℝ V'} {υ : PointedCone ℝ V''} {N : Type u_4} {N' : Type u_5} {N'' : Type u_6} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] {i : N →+ V} {i' : N' →+ V'} {i'' : N'' →+ V''} (hi : IsIntegralLattice i) (hi' : IsIntegralLattice i') (hi'' : IsIntegralLattice i'') (f : N →+ N') (f' : N' →+ N'') (g : V →ₗ[ℝ] V') (g' : V' →ₗ[ℝ] V'') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hf'g' : ∀ (n : N'), g' (i' n) = i'' (f' n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) (hτυ : Set.MapsTo ⇑g' ↑τ ↑υ) : (affineCoordinateRingMap hi hi' f g hfg hστ).comp (affineCoordinateRingMap hi' hi'' f' g' hf'g' hτυ) = affineCoordinateRingMap hi hi'' (f'.comp f) (g' ∘ₗ g) ⋯ ⋯

Coordinate-ring maps reverse composition, as required by their contravariance in cones.

Affine spectra

@[reducible, inline]

noncomputable abbrev TauCeti.Toric.affineToricScheme {V : Type u_1} [AddCommGroup V] [Module ℝ V] {N : Type u} [AddCommGroup N] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) : AlgebraicGeometry.Scheme

The affine toric scheme associated to a cone is the spectrum of its complex monoid algebra.

noncomputable def TauCeti.Toric.affineToricSchemeMap {V : Type u_1} {V' : Type u_2} [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {σ : PointedCone ℝ V} {τ : PointedCone ℝ V'} {N N' : Type u} [AddCommGroup N] [AddCommGroup N'] {i : N →+ V} {i' : N' →+ V'} (hi : IsIntegralLattice i) (hi' : IsIntegralLattice i') (f : N →+ N') (g : V →ₗ[ℝ] V') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) : affineToricScheme hi σ ⟶ affineToricScheme hi' τ

A compatible map of lattice cones induces a morphism of their affine toric schemes.

theorem TauCeti.Toric.affineToricSchemeMap_def {V : Type u_1} {V' : Type u_2} [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {σ : PointedCone ℝ V} {τ : PointedCone ℝ V'} {N N' : Type u} [AddCommGroup N] [AddCommGroup N'] {i : N →+ V} {i' : N' →+ V'} (hi : IsIntegralLattice i) (hi' : IsIntegralLattice i') (f : N →+ N') (g : V →ₗ[ℝ] V') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) : affineToricSchemeMap hi hi' f g hfg hστ = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (affineCoordinateRingMap hi hi' f g hfg hστ).toRingHom)

The affine toric morphism is Spec of the induced coordinate-ring map.

@[simp]

theorem TauCeti.Toric.affineToricSchemeMap_id {V : Type u_1} [AddCommGroup V] [Module ℝ V] {N : Type u} [AddCommGroup N] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) : affineToricSchemeMap hi hi (AddMonoidHom.id N) LinearMap.id ⋯ ⋯ = CategoryTheory.CategoryStruct.id (affineToricScheme hi σ)

The identity map of a lattice cone induces the identity of its affine toric scheme.

@[simp]

theorem TauCeti.Toric.affineToricSchemeMap_comp {V : Type u_1} {V' : Type u_2} {V'' : Type u_3} [AddCommGroup V] [AddCommGroup V'] [AddCommGroup V''] [Module ℝ V] [Module ℝ V'] [Module ℝ V''] {σ : PointedCone ℝ V} {τ : PointedCone ℝ V'} {υ : PointedCone ℝ V''} {N N' N'' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] {i : N →+ V} {i' : N' →+ V'} {i'' : N'' →+ V''} (hi : IsIntegralLattice i) (hi' : IsIntegralLattice i') (hi'' : IsIntegralLattice i'') (f : N →+ N') (f' : N' →+ N'') (g : V →ₗ[ℝ] V') (g' : V' →ₗ[ℝ] V'') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hf'g' : ∀ (n : N'), g' (i' n) = i'' (f' n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) (hτυ : Set.MapsTo ⇑g' ↑τ ↑υ) : CategoryTheory.CategoryStruct.comp (affineToricSchemeMap hi hi' f g hfg hστ) (affineToricSchemeMap hi' hi'' f' g' hf'g' hτυ) = affineToricSchemeMap hi hi'' (f'.comp f) (g' ∘ₗ g) ⋯ ⋯

Applying Spec restores covariance: the morphism of a composite cone map is the composite of the corresponding affine toric morphisms.

theorem TauCeti.Toric.affineToricSchemeMap_comp_specMap_algebraMap {V : Type u_1} {V' : Type u_2} [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {σ : PointedCone ℝ V} {τ : PointedCone ℝ V'} {N N' : Type} [AddCommGroup N] [AddCommGroup N'] {i : N →+ V} {i' : N' →+ V'} (hi : IsIntegralLattice i) (hi' : IsIntegralLattice i') (f : N →+ N') (g : V →ₗ[ℝ] V') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) : CategoryTheory.CategoryStruct.comp (affineToricSchemeMap hi hi' f g hfg hστ) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi' τ)))) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ)))

Affine toric morphisms are morphisms over Spec ℂ: they commute with the projections of their source and target to Spec ℂ.

theorem TauCeti.Toric.affineToricSchemeMap_comp_specMap_algebraMap_assoc {V : Type u_1} {V' : Type u_2} [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {σ : PointedCone ℝ V} {τ : PointedCone ℝ V'} {N N' : Type} [AddCommGroup N] [AddCommGroup N'] {i : N →+ V} {i' : N' →+ V'} (hi : IsIntegralLattice i) (hi' : IsIntegralLattice i') (f : N →+ N') (g : V →ₗ[ℝ] V') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧ℂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (affineToricSchemeMap hi hi' f g hfg hστ) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi' τ)))) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ)))) h

Affine toric morphisms are morphisms over Spec ℂ: they commute with the projections of their source and target to Spec ℂ.