OAI/GroupTheory/PolycyclicRecognition/Algebra/PolyhedralSymmetries.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite linear symmetry group of a spanning polytope

The support body in the height argument is a convex hull of finitely many covectors. Preserving that body permutes its extreme points. We prove that these form a finite spanning set, so the symmetry family is finite.

  1. theorem OAI.PolycyclicRecognition.finite_polytope_symmetries line 22

    Source documentation

    A finite spanning polytope has finitely many linear symmetries. Its given generators need not themselves be vertices.

    theorem finite_polytope_symmetries (s : Finset W)
    (hspan : Submodule.span ℝ (s : Set W) = ⊤) :
    Set.Finite {A : W ≃L[ℝ] W | A '' convexHull ℝ (s : Set W) = convexHull ℝ (s : Set W)} := by
…