Simplicial cones

A simplicial cone is a pointed convex cone that equals the conic hull of a finite linearly independent set of vectors. We do not require that the generators span the ambient module. However, when the cone is also generating, its generators linearly span the module.

Main definitions

• PointedCone.IsSimplicial: A pointed cone is simplicial if it equals the conic hull of a finite linearly independent set.

Results

• PointedCone.IsSimplicial.span: The conic hull of a linearly independent finite set is simplicial.

References

• Aubrun et al. Entangleability of cones

def PointedCone.IsSimplicial {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid M] [Module R M] (C : PointedCone R M) : Prop

A pointed cone is simplicial if it equals the conic hull of a finite set that is linearly independent over R.

Equations

• C.IsSimplicial = ∃ (s : Set M), s.Finite ∧ LinearIndepOn R id s ∧ PointedCone.hull R s = C

theorem PointedCone.IsSimplicial.hull {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid M] [Module R M] {s : Set M} (hs : s.Finite) (hli : LinearIndepOn R id s) : (hull R s).IsSimplicial

The conic hull of a finite linearly independent set is simplicial.