Toric cones in a real vector space with a lattice map

A toric cone is the combinatorial datum from which an affine toric variety is built. Following the convention that the ambient convex geometry stays on Mathlib's carriers, a toric cone here is a predicate on a Mathlib PointedCone ℝ V, taken relative to a lattice map i : N →+ V: the cone must be generated by the images of finitely many lattice vectors, and salient, that is, it must contain no line.

Salience is the condition that distinguishes the cones of affine toric varieties from arbitrary pointed cones: Mathlib's name PointedCone records only that 0 belongs to the cone, so a line is a pointed cone but is never a toric cone.

Main declarations

• TauCeti.Toric.IsLatticeRational: a pointed cone is generated by the images of finitely many lattice vectors.
• TauCeti.Toric.IsToricCone: lattice rationality and salience.
• TauCeti.Toric.IsToricCone.of_isFaceOf and TauCeti.Toric.IsToricCone.face: a face of a toric cone is a toric cone. Since the pairwise intersection of two cones of a fan is a face of each of them, this is also what makes those intersections toric.
• TauCeti.Toric.IsToricCone.map: an injective real-linear map compatible with a map of lattices carries toric cones to toric cones, and TauCeti.Toric.isToricCone_map_equiv_iff upgrades this to an equivalence along an isomorphism of lattices.
• TauCeti.Toric.IsToricCone.prod: a product of toric cones is a toric cone for the product lattice map.

Implementation notes

Finite generation is not recorded as a field of IsToricCone: IsLatticeRational.fg already derives it from lattice rationality, and IsToricCone.fg exposes it.

IsLatticeRational is an ordinary (unexposed) definition, so its body is not visible to downstream modules; isLatticeRational_iff is the public introduction and elimination interface that replaces the unavailable anonymous constructor there.

The lattice map i : N →+ V asks nothing of N beyond AddZeroClass, and lattice rationality needs only an additive commutative monoid V; salience, and hence IsToricCone, needs V to be an additive group. Freeness and finiteness of N, and finite dimensionality of V, play no role in the definitions or preservation results here.

References

The mathematics is Chapter 1 of D. Cox, J. Little and H. Schenck, Toric Varieties, and §1.2 of W. Fulton, Introduction to Toric Varieties.

Lattice rationality

def TauCeti.Toric.IsLatticeRational {N : Type u_1} {V : Type u_3} [AddZeroClass N] [AddCommMonoid V] [Module ℝ V] (i : N →+ V) (σ : PointedCone ℝ V) : Prop

A pointed cone σ in V is lattice rational for the lattice map i : N →+ V when it is the cone hull of the images of finitely many lattice vectors.

theorem TauCeti.Toric.isLatticeRational_iff {N : Type u_1} {V : Type u_3} [AddZeroClass N] [AddCommMonoid V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} : IsLatticeRational i σ ↔ ∃ (s : Finset N), σ = PointedCone.hull ℝ (⇑i '' ↑s)

The characteristic property of IsLatticeRational: a cone is lattice rational exactly when it is the cone hull of the images of some finite set of lattice vectors.

@[simp]

theorem TauCeti.Toric.isLatticeRational_hull_image {N : Type u_1} {V : Type u_3} [AddZeroClass N] [AddCommMonoid V] [Module ℝ V] (i : N →+ V) (s : Finset N) : IsLatticeRational i (PointedCone.hull ℝ (⇑i '' ↑s))

The cone hull of the images of a finite set of lattice vectors is lattice rational.

@[simp]

theorem TauCeti.Toric.isLatticeRational_bot {N : Type u_1} {V : Type u_3} [AddZeroClass N] [AddCommMonoid V] [Module ℝ V] (i : N →+ V) : IsLatticeRational i ⊥

The zero cone is lattice rational.

theorem TauCeti.Toric.IsLatticeRational.fg {N : Type u_1} {V : Type u_3} [AddZeroClass N] [AddCommMonoid V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (h : IsLatticeRational i σ) : Submodule.FG σ

A lattice-rational cone is finitely generated.

theorem TauCeti.Toric.IsLatticeRational.exists_mem_ne_zero {N : Type u_1} {V : Type u_3} [AddZeroClass N] [AddCommMonoid V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (h : IsLatticeRational i σ) (hσ : σ ≠ ⊥) : ∃ (v : N), i v ∈ σ ∧ i v ≠ 0

A lattice-rational cone other than the zero cone contains a nonzero image i v of a lattice vector v.

theorem TauCeti.Toric.IsLatticeRational.sup {N : Type u_1} {V : Type u_3} [AddZeroClass N] [AddCommMonoid V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hσ : IsLatticeRational i σ) (hτ : IsLatticeRational i τ) : IsLatticeRational i (σ ⊔ τ)

The join of two lattice-rational cones is lattice rational. Salience is not preserved, so this is not a statement about toric cones.

theorem TauCeti.Toric.IsLatticeRational.map {N : Type u_1} {N' : Type u_2} {V : Type u_3} {V' : Type u_4} [AddZeroClass N] [AddZeroClass N'] [AddCommMonoid V] [AddCommMonoid V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {σ : PointedCone ℝ V} {f : N →+ N'} {g : V →ₗ[ℝ] V'} (hfg : ∀ (n : N), g (i n) = i' (f n)) (hσ : IsLatticeRational i σ) : IsLatticeRational i' (PointedCone.map g σ)

The image of a lattice-rational cone under a real-linear map compatible with a map of lattices is lattice rational.

theorem TauCeti.Toric.IsLatticeRational.prod {N : Type u_1} {N' : Type u_2} {V : Type u_3} {V' : Type u_4} [AddZeroClass N] [AddZeroClass N'] [AddCommMonoid V] [AddCommMonoid V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {σ : PointedCone ℝ V} {τ' : PointedCone ℝ V'} (hσ : IsLatticeRational i σ) (hτ' : IsLatticeRational i' τ') : IsLatticeRational (i.prodMap i') (Submodule.prod σ τ')

A product of lattice-rational cones is lattice rational for the product lattice map.

Toric cones

structure TauCeti.Toric.IsToricCone {N : Type u_1} {V : Type u_3} [AddZeroClass N] [AddCommGroup V] [Module ℝ V] (i : N →+ V) (σ : PointedCone ℝ V) : Prop

A toric cone for the lattice map i : N →+ V is a lattice-rational and salient Mathlib pointed cone. Salience says that σ ∩ (-σ) = {0}; it is not implied by the name PointedCone, which records only that the cone contains 0.

• rational : IsLatticeRational i σ

  A toric cone is generated by the images of finitely many lattice vectors.

• salient : (↑σ).Salient

  A toric cone contains no line.

theorem TauCeti.Toric.IsToricCone.fg {N : Type u_1} {V : Type u_3} [AddZeroClass N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (h : IsToricCone i σ) : Submodule.FG σ

A toric cone is finitely generated over the nonnegative reals.

@[simp]

theorem TauCeti.Toric.isToricCone_bot {N : Type u_1} {V : Type u_3} [AddZeroClass N] [AddCommGroup V] [Module ℝ V] (i : N →+ V) : IsToricCone i ⊥

The zero cone is a toric cone; it is the cone whose affine chart is the dense torus.

@[simp]

theorem TauCeti.Toric.isToricCone_hull_singleton {N : Type u_1} {V : Type u_3} [AddZeroClass N] [AddCommGroup V] [Module ℝ V] (i : N →+ V) (v : N) : IsToricCone i (ℝ ∙₊ i v)

The cone generated by a single lattice vector is a toric cone.

Faces

theorem TauCeti.Toric.IsLatticeRational.of_isFaceOf {N : Type u_1} {V : Type u_3} [AddZeroClass N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hσ : IsLatticeRational i σ) (hτ : τ.IsFaceOf σ) : IsLatticeRational i τ

A face of a lattice-rational cone is lattice rational: it is generated by exactly those lattice generators of the ambient cone that lie on the face.

theorem TauCeti.Toric.IsToricCone.of_isFaceOf {N : Type u_1} {V : Type u_3} [AddZeroClass N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hσ : IsToricCone i σ) (hτ : τ.IsFaceOf σ) : IsToricCone i τ

A face of a toric cone is a toric cone. Since the pairwise intersection of two cones of a fan is a face of each of them, this also supplies the toricity of those intersections.

theorem TauCeti.Toric.IsToricCone.face {N : Type u_1} {V : Type u_3} [AddZeroClass N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hσ : IsToricCone i σ) (F : σ.Face) : IsToricCone i ↑F

Every element of Mathlib's face lattice of a toric cone is a toric cone.

Maps of lattices

theorem TauCeti.Toric.IsToricCone.map {N : Type u_1} {N' : Type u_2} {V : Type u_3} {V' : Type u_4} [AddZeroClass N] [AddZeroClass N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {σ : PointedCone ℝ V} {f : N →+ N'} {g : V →ₗ[ℝ] V'} (hfg : ∀ (n : N), g (i n) = i' (f n)) (hg : Function.Injective ⇑g) (hσ : IsToricCone i σ) : IsToricCone i' (PointedCone.map g σ)

An injective real-linear map compatible with a map of lattices carries toric cones to toric cones. Injectivity is what preserves salience.

theorem TauCeti.Toric.isToricCone_map_equiv_iff {N : Type u_1} {N' : Type u_2} {V : Type u_3} {V' : Type u_4} [AddZeroClass N] [AddZeroClass N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {σ : PointedCone ℝ V} {f : N ≃+ N'} {e : V ≃ₗ[ℝ] V'} (hfe : ∀ (n : N), e (i n) = i' (f n)) : IsToricCone i' (PointedCone.map (↑e) σ) ↔ IsToricCone i σ

Toricity is invariant along an isomorphism of lattices: transporting a cone by a linear equivalence compatible with an isomorphism of the lattices neither creates nor destroys toric cones.

Products

theorem TauCeti.Toric.IsToricCone.prod {N : Type u_1} {N' : Type u_2} {V : Type u_3} {V' : Type u_4} [AddZeroClass N] [AddZeroClass N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {σ : PointedCone ℝ V} {τ' : PointedCone ℝ V'} (hσ : IsToricCone i σ) (hτ' : IsToricCone i' τ') : IsToricCone (i.prodMap i') (Submodule.prod σ τ')

A product of toric cones is a toric cone for the product lattice map.