Simplicial cones #
A simplicial cone is a pointed convex cone that equals the conic span 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 span of a finite linearly independent set.
Results #
PointedCone.IsSimplicial.span: The conic span of a linearly independent finite set is simplicial.
References #
- [Aubrun et al. Entangleability of cones][aubrunEntangleabilityCones2021]
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)
:
A pointed cone is simplicial if it equals the conic span of a finite set that is linearly
independent over R.
Equations
Instances For
theorem
PointedCone.IsSimplicial.span
{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)
:
(span R s).IsSimplicial
The conic span of a finite linearly independent set is simplicial.