Face localizations of affine toric schemes

A character m in the dual semigroup of a cone σ is nonnegative on σ, so it cuts out the face σ ⊓ ker m of σ (PointedCone.isFaceOf_inf_ker). The inclusion of that face into σ induces the restriction map from the coordinate ring of σ to the coordinate ring of the face. When σ is finitely generated, this map is the localization away from the monomial of m: the dual semigroup of the face is obtained from that of σ by adjoining -m (TauCeti.Toric.dualSemigroup_inf_ker_eq_sup). On spectra, the affine toric scheme of the face is therefore the basic open subscheme of the affine toric scheme of σ where the monomial of m does not vanish, and the induced morphism is an open immersion.

Every face of a lattice-rational cone is cut out by such a character (TauCeti.Toric.IsLatticeRational.exists_mem_dualSemigroup_inf_ker_eq). Thus every face inclusion of a lattice-rational cone induces a localization at a single monomial and an open immersion of affine toric schemes.

These open immersions are the maps along which the affine toric schemes of a fan are glued. The canonical face maps introduced here satisfy identity and composition laws, so successive face restrictions give the same morphism as the composite face inclusion. This is the functoriality needed for the overlap and cocycle maps in fan gluing.

Main declarations

• TauCeti.Toric.isLocalization_away_affineCoordinateRingMap_inf_ker: the coordinate ring of the face σ ⊓ ker m is the localization of the coordinate ring of σ away from the monomial of m.
• TauCeti.Toric.isOpenImmersion_affineToricSchemeMap_inf_ker: the affine toric scheme of the face is an open subscheme of the affine toric scheme of σ.
• TauCeti.Toric.faceAffineCoordinateRingMap and TauCeti.Toric.faceAffineToricSchemeMap: the canonical restriction map and affine-scheme morphism attached to a face inclusion, with identity and composition laws; and TauCeti.Toric.faceAffineToricSchemeMap_eq_affineToricSchemeMap: the affine-scheme characterization of the canonical face morphism.
• TauCeti.Toric.IsLatticeRational.exists_isLocalization_away_faceAffineCoordinateRingMap and TauCeti.Toric.IsLatticeRational.isOpenImmersion_faceAffineToricSchemeMap: for a face τ of a lattice-rational cone σ, the coordinate ring of τ is the localization of that of σ away from a single monomial, and the affine toric scheme of τ is an open subscheme of that of σ.
• TauCeti.Toric.range_faceAffineToricSchemeMap and TauCeti.Toric.IsLatticeRational.range_faceAffineToricSchemeMap_inf: the image of the affine toric scheme of a face is a basic open set; for faces of a lattice-rational cone the image of their intersection is the intersection of their images.
• TauCeti.Toric.preimage_range_faceAffineToricSchemeMap_inf_ker: the inverse image, under the affine toric morphism of a cone map, of the open subscheme of the face cut out by a character is the open subscheme of the face cut out by the pulled-back character.
• TauCeti.Toric.Fan.affineToricChart, TauCeti.Toric.Fan.affineToricOverlap, TauCeti.Toric.Fan.affineToricOverlapLeft and TauCeti.Toric.Fan.affineToricOverlapRight: the affine toric charts of a fan and the two maps from their pairwise overlap; these maps are open immersions for every fan.

References

• W. Fulton, Introduction to Toric Varieties, §1.3.
• D. Cox, J. Little and H. Schenck, Toric Varieties, §1.3.

Canonical maps attached to face inclusions

noncomputable def TauCeti.Toric.faceAffineCoordinateRingMap {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hτσ : τ.IsFaceOf σ) : affineCoordinateRing hi σ →ₐ[ℂ] affineCoordinateRing hi τ

A face inclusion τ ≼ σ induces the restriction map from the coordinate ring of σ to the coordinate ring of τ.

@[simp]

theorem TauCeti.Toric.faceAffineCoordinateRingMap_single {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hτσ : τ.IsFaceOf σ) (m : ↥(dualSemigroup hi σ)) (z : ℂ) : (faceAffineCoordinateRingMap hi hτσ) (MonoidAlgebra.single (Multiplicative.ofAdd m) z) = MonoidAlgebra.single (Multiplicative.ofAdd ⟨↑m, ⋯⟩) z

Restriction along a face inclusion sends a monomial to the same integral character, regarded as an element of the larger dual semigroup of the face.

@[simp]

theorem TauCeti.Toric.faceAffineCoordinateRingMap_id {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) : faceAffineCoordinateRingMap hi ⋯ = AlgHom.id ℂ (affineCoordinateRing hi σ)

Restriction to a cone viewed as its own face is the identity map of its coordinate ring.

@[simp]

theorem TauCeti.Toric.faceAffineCoordinateRingMap_comp {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ υ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hυτ : υ.IsFaceOf τ) (hτσ : τ.IsFaceOf σ) : (faceAffineCoordinateRingMap hi hυτ).comp (faceAffineCoordinateRingMap hi hτσ) = faceAffineCoordinateRingMap hi ⋯

Restriction through two successive face inclusions is restriction along their composite.

noncomputable def TauCeti.Toric.faceAffineToricSchemeMap {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hτσ : τ.IsFaceOf σ) : affineToricScheme hi τ ⟶ affineToricScheme hi σ

The canonical morphism from the affine toric scheme of a face to that of its ambient cone.

theorem TauCeti.Toric.faceAffineToricSchemeMap_def {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hτσ : τ.IsFaceOf σ) : faceAffineToricSchemeMap hi hτσ = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (faceAffineCoordinateRingMap hi hτσ).toRingHom)

The morphism attached to a face inclusion is the spectrum of its coordinate-ring restriction.

theorem TauCeti.Toric.faceAffineToricSchemeMap_eq_affineToricSchemeMap {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hτσ : τ.IsFaceOf σ) : faceAffineToricSchemeMap hi hτσ = affineToricSchemeMap hi hi (AddMonoidHom.id N) LinearMap.id ⋯ ⋯

The canonical face morphism is the affine toric scheme map induced by the identity on the lattice and real vector space.

@[simp]

theorem TauCeti.Toric.faceAffineToricSchemeMap_id {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) : faceAffineToricSchemeMap hi ⋯ = CategoryTheory.CategoryStruct.id (affineToricScheme hi σ)

The morphism of a cone viewed as its own face is the identity morphism.

@[simp]

theorem TauCeti.Toric.faceAffineToricSchemeMap_comp {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ υ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hυτ : υ.IsFaceOf τ) (hτσ : τ.IsFaceOf σ) : CategoryTheory.CategoryStruct.comp (faceAffineToricSchemeMap hi hυτ) (faceAffineToricSchemeMap hi hτσ) = faceAffineToricSchemeMap hi ⋯

The morphism of a composite face inclusion is the composite of the face morphisms.

Localizations and open immersions

theorem TauCeti.Toric.isLocalization_away_affineCoordinateRingMap_inf_ker {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : Submodule.FG σ) (m : ↥(dualSemigroup hi σ)) : IsLocalization.Away (MonoidAlgebra.single (Multiplicative.ofAdd m) 1) (affineCoordinateRing hi (σ ⊓ ↑(LinearMap.ker (hi.realCharacter ↑m))))

For a character m in the dual semigroup of a finitely generated cone σ, the restriction map from the coordinate ring of σ to that of the face σ ⊓ ker m is the localization away from the monomial of m.

theorem TauCeti.Toric.isOpenImmersion_affineToricSchemeMap_inf_ker {V : Type u_2} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {N : Type u} [AddCommGroup N] {i : N →+ V} (hi : IsIntegralLattice i) (hσ : Submodule.FG σ) (m : ↥(dualSemigroup hi σ)) : AlgebraicGeometry.IsOpenImmersion (affineToricSchemeMap hi hi (AddMonoidHom.id N) LinearMap.id ⋯ ⋯)

For a character m in the dual semigroup of a finitely generated cone σ, the morphism from the affine toric scheme of the face σ ⊓ ker m to that of σ is an open immersion.

theorem TauCeti.Toric.range_faceAffineToricSchemeMap {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : Submodule.FG σ) (m : ↥(dualSemigroup hi σ)) : Set.range ⇑(faceAffineToricSchemeMap hi ⋯) = ↑(PrimeSpectrum.basicOpen (MonoidAlgebra.single (Multiplicative.ofAdd m) 1))

For a character m in the dual semigroup of a finitely generated cone σ, the image of the affine toric scheme of the face σ ⊓ ker m in that of σ is the basic open set where the monomial of m does not vanish.

theorem TauCeti.Toric.preimage_range_faceAffineToricSchemeMap_inf_ker {V : Type u_2} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {N N' : Type u} {V' : Type u_3} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {ρ : PointedCone ℝ 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 ↑σ ↑ρ) (hσ : Submodule.FG σ) (hρ : Submodule.FG ρ) (m : ↥(dualSemigroup hi' ρ)) : ⇑(affineToricSchemeMap hi hi' f g hfg hσρ) ⁻¹' Set.range ⇑(faceAffineToricSchemeMap hi' ⋯) = Set.range ⇑(faceAffineToricSchemeMap hi ⋯)

Let a compatible map of lattices carry a finitely generated cone σ into a finitely generated cone ρ, and let m be a character in the dual semigroup of ρ. The inverse image of the open subscheme of the face ρ ⊓ ker m is the open subscheme of the face of σ cut out by the pullback of m.

theorem TauCeti.Toric.IsLatticeRational.exists_isLocalization_away_faceAffineCoordinateRingMap {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsLatticeRational i σ) (hτ : τ.IsFaceOf σ) : ∃ (m : ↥(dualSemigroup hi σ)), IsLocalization.Away (MonoidAlgebra.single (Multiplicative.ofAdd m) 1) (affineCoordinateRing hi τ)

For a face τ of a lattice-rational cone σ, the restriction map from the coordinate ring of σ to that of τ is the localization away from the monomial of a character in the dual semigroup of σ.

theorem TauCeti.Toric.IsLatticeRational.isOpenImmersion_faceAffineToricSchemeMap {V : Type u_2} [AddCommGroup V] [Module ℝ V] {σ τ : PointedCone ℝ V} {N : Type u} [AddCommGroup N] {i : N →+ V} (hi : IsIntegralLattice i) (hσ : IsLatticeRational i σ) (hτ : τ.IsFaceOf σ) : AlgebraicGeometry.IsOpenImmersion (faceAffineToricSchemeMap hi hτ)

For a face τ of a lattice-rational cone σ, the morphism from the affine toric scheme of τ to that of σ is an open immersion.

theorem TauCeti.Toric.IsLatticeRational.range_faceAffineToricSchemeMap_inf {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsLatticeRational i σ) {υ : PointedCone ℝ V} (hτ : τ.IsFaceOf σ) (hυ : υ.IsFaceOf σ) : Set.range ⇑(faceAffineToricSchemeMap hi ⋯) = Set.range ⇑(faceAffineToricSchemeMap hi hτ) ∩ Set.range ⇑(faceAffineToricSchemeMap hi hυ)

For two faces τ and υ of a lattice-rational cone σ, the image of the affine toric scheme of τ ⊓ υ in that of σ is the intersection of the images of the affine toric schemes of τ and of υ.

Pairwise overlaps in a fan

@[reducible, inline]

noncomputable abbrev TauCeti.Toric.Fan.affineToricChart {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) : AlgebraicGeometry.Scheme

The affine toric chart indexed by a cone of a fan.

@[reducible, inline]

noncomputable abbrev TauCeti.Toric.Fan.affineToricOverlap {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ τ : ↑Φ.cones) : AlgebraicGeometry.Scheme

The affine toric scheme of the intersection of two cones is their pairwise overlap chart.

noncomputable def TauCeti.Toric.Fan.affineToricOverlapLeft {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ τ : ↑Φ.cones) : Φ.affineToricOverlap σ τ ⟶ Φ.affineToricChart σ

The canonical map from a pairwise overlap into its left affine chart.

noncomputable def TauCeti.Toric.Fan.affineToricOverlapRight {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ τ : ↑Φ.cones) : Φ.affineToricOverlap σ τ ⟶ Φ.affineToricChart τ

The canonical map from a pairwise overlap into its right affine chart.

@[simp]

theorem TauCeti.Toric.Fan.affineToricOverlapLeft_def {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ τ : ↑Φ.cones) : Φ.affineToricOverlapLeft σ τ = faceAffineToricSchemeMap ⋯ ⋯

The left overlap leg is the face map of the inclusion σ ⊓ τ ≼ σ.

@[simp]

theorem TauCeti.Toric.Fan.affineToricOverlapRight_def {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ τ : ↑Φ.cones) : Φ.affineToricOverlapRight σ τ = faceAffineToricSchemeMap ⋯ ⋯

The right overlap leg is the face map of the inclusion σ ⊓ τ ≼ τ.

theorem TauCeti.Toric.Fan.isOpenImmersion_affineToricOverlapLeft {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ τ : ↑Φ.cones) : AlgebraicGeometry.IsOpenImmersion (Φ.affineToricOverlapLeft σ τ)

The map from a pairwise overlap into its left affine chart is an open immersion.

theorem TauCeti.Toric.Fan.isOpenImmersion_affineToricOverlapRight {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ τ : ↑Φ.cones) : AlgebraicGeometry.IsOpenImmersion (Φ.affineToricOverlapRight σ τ)

The map from a pairwise overlap into its right affine chart is an open immersion.