The goal of this project is to build a flexible, general and useful implementation of polyhedral geometry/combinatorics in Lean, for mathlib, on which more advanced theory can be built. This repository serves as a testing ground for features from which we subsequently build PRs for mathlib.
The main discussion happens on Zulip, in particular, in the thread "Polyhedra in mathlib".
Currently the project implements:
- duals of finitely generated cones (H-cones)
- duality theory for
FGpointed cones, in particular, a version of the Minkowski-Weyl theorem that also works in 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
- the lineality space of a cone
- faces and exposed faces of cones
- the face lattice of a cone
- Krein-Milman theorem for FG cones
- a proof that face lattices of finitely generated cones are graded
- convex sets, polytopes and polyhedra in
ConvexSpace - faces of convex sets
- affine homogenization
- tools for translating between cones in modules and convex sets in affine spaces
A detailed overview of the most relevant open and merged PRs is given in the Zulip thread "PRs for polyhedral geometry and combinatorics".