Salient finitely generated cones are generated by their extremal rays

In a salient pointed cone generated by a set s, a generator that is not in the cone generated by the remaining generators spans a face of the cone. Choosing a generating set of least cardinality, every generator is of this kind. Hence a salient finitely generated pointed cone over an ordered division ring is the cone hull of finitely many nonzero vectors, each spanning a face. These faces are the one-dimensional faces, the extremal rays, of the cone; this is the conic analogue of the fact that a polytope is the convex hull of its vertices.

Salience cannot be dropped: a line through the origin is a finitely generated pointed cone whose only face is the line itself, so no nonzero vector spans a face of it.

Main declarations

• PointedCone.hull_singleton_isFaceOf_of_notMem_hull: in a salient cone generated by s, a generator outside the cone generated by the other generators spans a face.
• PointedCone.FG.exists_finset_hull_eq_isFaceOf: a salient finitely generated pointed cone is the cone hull of a finite set of nonzero vectors, each of which spans a face of the cone.

References

• W. Fulton, Introduction to Toric Varieties, §1.2, property (8) of cones.
• D. Cox, J. Little and H. Schenck, Toric Varieties, Lemma 1.2.15.

theorem PointedCone.hull_singleton_isFaceOf_of_notMem_hull {R : Type u_1} {M : Type u_2} [DivisionRing R] [LinearOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C : PointedCone R M} (hC : (↑C).Salient) {s : Set M} (hs : hull R s = C) {v : M} (hv : v ∈ s) (hvs : v ∉ hull R (s \ {v})) : (R ∙₊ v).IsFaceOf C

In a salient pointed cone generated by a set s, a generator v that does not lie in the cone generated by the other generators spans a face of the cone.

theorem PointedCone.FG.exists_finset_hull_eq_isFaceOf {R : Type u_1} {M : Type u_2} [DivisionRing R] [LinearOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C : PointedCone R M} (hfg : Submodule.FG C) (hC : (↑C).Salient) : ∃ (s : Finset M), hull R ↑s = C ∧ ∀ v ∈ s, v ≠ 0 ∧ (R ∙₊ v).IsFaceOf C

A salient finitely generated pointed cone over an ordered division ring is the cone hull of a finite set of nonzero vectors, each of which spans a face of the cone. Any generating set of least cardinality has this property.