 Face of an additive monoid

A face $F$ of an additive monoid $S$ is a submonoid such that $a+b\in F$ implies $a,b\in F$. If $S=C\cap M$ for a rational polyhedral cone, its faces are precisely $S\cap \nu$ for faces $\nu$ of $C$. Finite generation and clearing rational denominators identify these monoid faces with the exposed faces of the cone.

// Target: geometry-and-topology.bigb