feat: face lattice of a polytope is graded by the dimension of the face

Polyhedral.lean

@@ -77,5 +77,6 @@ public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.Set
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Lattice
 public import Polyhedral.Mathlib.LinearAlgebra.BilinearMap
 public import Polyhedral.Mathlib.LinearAlgebra.Dual.Basis
+public import Polyhedral.Mathlib.Order.WithBot
 public import Polyhedral.Mathlib.RingTheory.Finiteness.Cofinite
 public import Polyhedral.Mathlib.RingTheory.Finiteness.Corank

Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Basic.lean

@@ -6,10 +6,12 @@ Authors: Martin Winter, Olivia Röhrig
 module
 
 public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Hull
+public import Mathlib.RingTheory.Finiteness.Basic
 
 import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
 import Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
 import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
+import Mathlib.Algebra.Group.Pointwise.Set.Finite
 
 /-! This file introduces `IsPolytope` and proves basic properties about convex polytopes. -/
 
@@ -97,6 +99,23 @@ protected lemma prod {P₂ : Set Y} (hP₁ : IsPolytope R P₁) (hP₂ : IsPolyt
 
 end Semiring
 
+section Ring
+
+variable [Ring R] [PartialOrder R] [IsStrictOrderedRing R]
+variable [ConvexSpace R X]
+variable [AddCommGroup V] [Module R V] [AddTorsor V X] [IsAffineConvexSpace R V X]
+
+variable {P : Set X}
+
+theorem finite_vectorSpan (hP : IsPolytope R P) : Module.Finite R (vectorSpan R P) := by
+  obtain ⟨t, rfl⟩ := hP
+  rw [vectorSpan_convexHull]
+  -- TODO: Can be `infer_instance` after https://github.com/leanprover-community/mathlib4/pull/43770
+  rw [vectorSpan_def]
+  exact Module.Finite.span_of_finite _ <| t.finite_toSet.vsub t.finite_toSet
+
+end Ring
+
 section Field
 
 variable [Field R] [PartialOrder R] [IsStrictOrderedRing R]

Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Face.lean

@@ -7,16 +7,18 @@ module
 
 public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Lattice
 public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Face.Homogenization
+public import Mathlib.Order.Grade
 
 import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Finite.Face.Grade
 import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Homogenization
+import Polyhedral.Mathlib.Order.WithBot
 
 /-! This file proves results about faces of polytopes by transporting results from FG
 cones along a homogenization. -/
 
 public section
 
-variable {R V A : Type*}
+variable {R V W A : Type*}
 
 open Convexity ConvexSet Affine
 
@@ -44,21 +46,50 @@ include V in
 instance {P : Polytope R A} : CoeOut (Face (P : ConvexSet R A)) (Polytope R A) where
   coe F := ⟨_, IsPolytope.face_isPolytope P.isPolytope F.isFaceOf⟩
 
-include V in
-/-- The face lattice of a polytope as a graded order with grading given by the dimensions of
-homogenization cones.
+instance {P : Polytope R A} (F : Face (P : ConvexSet R A)) :
+    Module.Finite R (vectorSpan R (F.toConvexSet : Set A)) :=
+  IsPolytope.finite_vectorSpan (IsPolytope.face_isPolytope P.isPolytope F.isFaceOf)
 
-This is private since it does not yet have the correct grading (off-by-one).
--/
-private noncomputable instance Polytope.faceHomogenizationGradeOrder (P : Polytope R A) :
-    GradeOrder ℕ (Face (P : ConvexSet R A)) := by
-  let W := Homogenization R A
-  letI : ConvexSpace R W := ConvexSpace.ofModule
-  have : PointedCone.FG (homogenize W (P : ConvexSet R A)) :=
-    IsPolytope.homogenize_fg (W := W) P.isPolytope
-  let := PointedCone.FG.gradeOrder_finrank this
-  refine GradeOrder.liftRight (β := (homogenize W (P : ConvexSet R A)).Face) _
-    IsHomogenization.Face.homogenizeIso.strictMono ?_
-  exact fun x y ↦ (apply_covBy_apply_iff _).mpr
+/-- The face lattice of a polytope is graded by the dimension of the affine span of each face,
+with the empty face receiving the grade `⊥`. -/
+noncomputable instance (P : Polytope R A) :
+    GradeMinOrder (WithBot ℕ) (Face (P : ConvexSet R A)) where
+  grade F := (affineSpan R F.carrier).finDim
+  grade_strictMono x y h := by
+    let : ConvexSpace R (Homogenization R A) := ConvexSpace.ofModule
+    simp only [Face.carrier_eq_coe, Face.coe_eq_toConvexSet_coe,
+      finDim_affineSpan_eq_pred_finrank_homogenize (Homogenization R A)]
+    refine Order.pred_lt_pred_of_not_isMin ?_ (by simp)
+    exact_mod_cast PointedCone.FG.finrank_strictMono (IsPolytope.homogenize_fg P.isPolytope)
+      (IsHomogenization.Face.homogenizeIso.strictMono h)
+  covBy_grade x y h := by
+    let : ConvexSpace R (Homogenization R A) := ConvexSpace.ofModule
+    have := PointedCone.FG.finrank_covBy (IsPolytope.homogenize_fg P.isPolytope)
+      ((apply_covBy_apply_iff
+        (IsHomogenization.Face.homogenizeIso (W := Homogenization R A))).mpr h)
+    have : (homogenize (Homogenization R A) x.toConvexSet).finrank + 1
+        = (homogenize (Homogenization R A) y.toConvexSet).finrank :=
+      Nat.covBy_iff_add_one_eq.mp this
+    simp only [Face.carrier_eq_coe, Face.coe_eq_toConvexSet_coe,
+      finDim_affineSpan_eq_pred_finrank_homogenize (Homogenization R A), ← this]
+    exact Order.succ_eq_iff_covBy.mp (by simp)
+  isMin_grade f h := by simp [isMin_iff_eq_bot.mp h]
+
+section Homogenization
+
+variable [AddCommGroup W] [Module R W] [hom : IsHomogenization R A W]
+
+variable (W) in
+theorem Polytope.grade_eq_pred_finrank_homogenize {P : Polytope R A}
+    (f : Face (P : ConvexSet R A)) :
+    GradeOrder.grade f = Order.pred ((homogenize W f.toConvexSet).finrank : WithBot ℕ) :=
+  finDim_affineSpan_eq_pred_finrank_homogenize ..
+
+theorem Polytope.succ_grade_eq_finrank_homogenize {P : Polytope R A}
+    (f : Face (P : ConvexSet R A)) :
+    Order.succ (GradeOrder.grade f : WithBot ℕ) = (homogenize W f.toConvexSet).finrank := by
+  rw [Polytope.grade_eq_pred_finrank_homogenize W, Order.succ_pred_of_not_isMin (by simp)]
+
+end Homogenization
 
 end Field

Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Lattice.lean

@@ -107,6 +107,17 @@ instance : SemilatticeSup (Polytope R X) where
 
 end Semiring
 
+section Ring
+
+variable [Ring R] [PartialOrder R] [IsStrictOrderedRing R]
+variable [ConvexSpace R X]
+variable [AddCommGroup V] [Module R V] [AddTorsor V X] [IsAffineConvexSpace R V X]
+
+instance finite_vectorSpan (P : Polytope R X) : Module.Finite R (vectorSpan R (P : Set X)) :=
+  IsPolytope.finite_vectorSpan P.isPolytope
+
+end Ring
+
 section Field
 
 variable [Field R] [PartialOrder R] [IsStrictOrderedRing R]

Polyhedral/Mathlib/Order/WithBot.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2026 Vlad Tsyrklevich. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Vlad Tsyrklevich
+-/
+
+module
+
+public import Mathlib.Algebra.Order.SuccPred.WithBot
+public import Mathlib.Data.Nat.SuccPred
+public import Mathlib.Order.SuccPred.WithBot
+public import Mathlib.Order.WithBot
+
+/-! WithBot lemmas -/
+
+public section
+
+namespace WithBot
+
+theorem natCast_orderSucc (a : ℕ) : Nat.cast (Order.succ a) = Order.succ (a : WithBot ℕ) :=
+  WithBot.orderSucc_coe _
+
+@[simp]
+theorem pred_natCast_add_one (a : ℕ) : Order.pred ((a : WithBot ℕ) + 1) = a := by
+  rw [← Nat.cast_succ, ← Nat.succ_eq_succ, natCast_orderSucc]
+  simp
+
+end WithBot