The goal of this project is to provide a flexible and useful implementation of polyhedral geometry/combinatorics in Lean, for mathlib, on which more advanced theory can be built. Currently we focus on polyhedral cones since convexity on affine spaces is not yet well developed in mathlib. There is a clear plan for how to move to polyhedra and polytopes eventually. To get to a point where we can implement and work with polyhedral cones comfortably, we also needed to implement duality theory, faces of cones and many more details.
See also the Zulip discussion on the topic.
Currently the project implements:
- co-finitely generated submodules (
CoFG) - duality for submodules w.r.t. a general bilinear pairing.
- dual closed subspaces (
DualClosed) which expresses that a subspace is its own double dual. FGDualsubmodules, which are the dual ofFG(finitely generated) submodules.- duality theory for
FGsubmodules - dual closed pointed cones
FGDualpointed cones- duality theory for
FGpointed cones, in particular, a version of the Minkowski-Weyl theorem that works to infinite dimensional modules. - polyhedral cones as cones that can be written as the sum of an
FGcone and a submodule. - duality theory of polyhedral cones
- faces and exposed faces of cones
- the face lattice of a cone
- Krein-Milman theorem for FG cones
- face theory of polyhedral cones (all faces are exposed, the face lattice is graded, etc.)
Below is a short list of the most important PRs from this project. A more detailled overview of all open and merged PRs is given on Zulip.