Face generation and finiteness of the face lattice

A face of a cone generated by a set is generated by the members of that set which it contains. Consequently, a finitely generated pointed cone has only finitely many faces: each face is determined by a subset of any fixed finite generating set.

Main declarations

• PointedCone.IsFaceOf.eq_hull_inter_of_eq_hull: a face of the hull of a set is the hull of the generators lying in that face.
• PointedCone.IsFaceOf.eq_bot_or_eq_of_hull_singleton: a face of a singly generated cone is either the zero cone or the whole cone.
• PointedCone.FG.finite_face: the face lattice of a finitely generated pointed cone is finite.

References

This is the elementary face description for polyhedral cones; see D. Cox, J. Little and H. Schenck, Toric Varieties, Proposition 1.2.2.

theorem PointedCone.IsFaceOf.eq_hull_inter_of_eq_hull {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F : PointedCone R M} {s : Set M} (hF : F.IsFaceOf C) (hC : C = hull R s) : F = hull R (s ∩ ↑F)

A face of a cone generated by a set is generated by precisely the members of the generating set which lie in the face.

theorem PointedCone.IsFaceOf.eq_bot_or_eq_of_hull_singleton {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {F : PointedCone R M} (v : M) (hF : F.IsFaceOf (R ∙₊ v)) : F = ⊥ ∨ F = R ∙₊ v

A face of a cone generated by one vector is either the zero cone or the whole cone.

theorem PointedCone.FG.finite_face {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C : PointedCone R M} (hC : Submodule.FG C) : Finite C.Face

The face lattice of a finitely generated pointed cone is finite.