prove that a convex set is a polytope iff homogenization cone is FG

Polyhedral.lean

@@ -1,6 +1,5 @@
 import Polyhedral.Mathlib.Algebra.Group.Pointwise.SetLike.Basic
 import Polyhedral.Mathlib.Algebra.Group.Pointwise.SetLike.Scalar
-import Polyhedral.Mathlib.Algebra.Module.Submodule.SubMulActionWithZero
 import Polyhedral.Mathlib.Algebra.Module.Submodule.Basic
 import Polyhedral.Mathlib.Algebra.Module.Submodule.Dual
 import Polyhedral.Mathlib.Algebra.Module.Submodule.DualClosed
@@ -9,14 +8,12 @@ import Polyhedral.Mathlib.Algebra.Module.Submodule.FG
 import Polyhedral.Mathlib.Algebra.Module.Submodule.Hyperplane
 import Polyhedral.Mathlib.Algebra.Module.Submodule.Quotient
 import Polyhedral.Mathlib.Algebra.Module.Submodule.Restrict
+import Polyhedral.Mathlib.Algebra.Module.Submodule.SubMulActionWithZero
 import Polyhedral.Mathlib.Algebra.Order.Nonneg.Basic
 import Polyhedral.Mathlib.Algebra.Order.Nonneg.DivisionRing
 import Polyhedral.Mathlib.Algebra.Order.Nonneg.Ring
 import Polyhedral.Mathlib.Data.Set.Lattice.Image
 import Polyhedral.Mathlib.Data.SetLike.IsConcrete
-import Polyhedral.Mathlib.GroupTheory.GroupAction.SubMulActionWithZero
-import Polyhedral.Mathlib.GroupTheory.GroupAction.SubMulActionWithZero.Closure
-import Polyhedral.Mathlib.GroupTheory.GroupAction.SubMulActionWithZero.Nonneg
 import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Basic
 import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Convexity
 import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Dual
@@ -40,6 +37,7 @@ import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Ray
 import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Relint
 import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.SubMulActionWithZero
 import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
+import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Homogenization
 import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Module
 import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Basic
 import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Face
@@ -53,6 +51,9 @@ import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Homogenization
 import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Hull
 import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Lattice
 import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Pointwise
+import Polyhedral.Mathlib.GroupTheory.GroupAction.SubMulActionWithZero
+import Polyhedral.Mathlib.GroupTheory.GroupAction.SubMulActionWithZero.Closure
+import Polyhedral.Mathlib.GroupTheory.GroupAction.SubMulActionWithZero.Nonneg
 import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineMap
 import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Defs
 import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.Basic

Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean

@@ -0,0 +1,80 @@
+import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Convexity
+import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
+import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.Basic
+
+open Convexity Pointwise Set PointedCone Submodule
+
+namespace Convexity
+
+section Ring
+
+variable {R : Type*} [Ring R] [PartialOrder R] [IsStrictOrderedRing R]
+variable {V : Type*} [AddCommGroup V] [Module R V]
+variable {A : Type*} [AddTorsor V A]
+variable {W : Type*} [AddCommGroup W] [Module R W]
+variable [hom : Affine.IsHomogenization R A W]
+
+attribute [local instance] AddTorsor.toConvexSpace
+
+section Module
+
+variable [IsModuleConvexSpace R W]
+
+/-- If the homogenization of a point lies in the conic hull of a subset `s` of the homogenization
+plane, the point can be written as a convex combination of points in the preimage of `s` under the
+homogenization embedding. -/
+theorem exists_sConvexComb_preimage_of_mem_hull {x} {s : Set W} (hs : s ⊆ Set.range hom.ofPoint)
+    (hx : hom.ofPoint x ∈ hull R s) : ∃ c' : StdSimplex R A,
+      sConvexComb c' = x ∧ (c'.weights.support : Set A) ⊆ (hom.ofPoint ⁻¹' s) := by
+  obtain ⟨c, ha, hb, hc⟩ := mem_hull_set.mp hx
+  -- use the same weights, just un-embed the domain
+  use StdSimplex.mk (c.comapDomain hom.ofPoint hom.ofPoint_injective.injOn) ?_ ?_
+  constructor
+  · -- the convex combo yields x
+    apply hom.ofPoint_injective
+    rw [hom.ofPoint.isAffineMap.map_sConvexComb, sConvexComb_eq_sum,
+      StdSimplex.weights_map, ← hc, Finsupp.mapDomain_comapDomain _ hom.ofPoint_injective]
+    exact ha.trans hs
+  · -- the weights are a subset of the preimage of s
+    simpa using (Set.preimage_mono ha)
+  · -- they're always nonneg
+    intro y
+    simpa using hb (hom.ofPoint y)
+  · -- its actually a convex combo, i.e. weights sum to 1
+    have hsum : c.sum (fun a b => b * hom.weight a) = c.sum (fun a b => b) := by
+        refine Finsupp.sum_congr (fun a h => ?_)
+        obtain ⟨_, _, rfl⟩ := (ha.trans hs) h
+        simp [hom.weight_one]
+    -- apply weights map to both sides
+    have := congrArg hom.weight hc
+    simp only [map_finsuppSum, map_smul, smul_eq_mul, hsum, hom.weight_one] at this
+    rw [← this]
+    simp only [Finsupp.sum, Finsupp.comapDomain_support, Finsupp.comapDomain_apply]
+    rw [Finset.sum_preimage hom.ofPoint _ (hom.ofPoint_injective.injOn)]
+    exact fun _ hx hnx ↦ Finsupp.notMem_support_iff.mp fun _ ↦ hnx (hs (ha hx))
+
+/-- The preimage of the conic hull of a set in the homogenization plane is the convex hull of the
+preimage of the set. -/
+theorem preimage_hull_eq_convexHull_preimage {s : Set W} (hs : s ⊆ Set.range hom.ofPoint) :
+    hom.ofPoint ⁻¹' hull R s = Convexity.convexHull R (hom.ofPoint ⁻¹' s) := by
+  refine subset_antisymm ?_ ?_
+  · intro x hx
+    obtain ⟨c', rfl, hs⟩ := exists_sConvexComb_preimage_of_mem_hull hs hx
+    exact IsConvexSet.convexHull.sConvexComb_mem (le_trans hs subset_convexHull_self)
+  · apply Set.image_subset_iff.mp
+    rw [hom.ofPoint.isAffineMap.image_convexHull, Set.image_preimage_eq_iff.mpr hs]
+    exact (hull R s).isConvexSet.convexHull_subset_iff.mpr subset_hull
+
+/-- The homogenization embedding of the convex hull of a set is contained in the hull of the
+embedding of the set. -/
+theorem preimage_hull_eq_convexHull_preimagke {s : Set A} :
+    hom.ofPoint '' Convexity.convexHull R s ⊆ hull R (hom.ofPoint '' s) := by
+  apply Set.image_subset_iff.mp
+  rw [hom.ofPoint.isAffineMap.image_convexHull]
+  simpa using (hull R _).isConvexSet.convexHull_subset_iff.mpr subset_hull
+
+end Module
+
+end Ring
+
+end Convexity

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

@@ -1,8 +1,6 @@
-import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Finite.Face.Grade
+import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Homogenization
 import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Basic
 import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Homogenization
-import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Face.Basic
-import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Module
 
 /-! This file proves results about polytopes, FG cones and homogenization. -/
 
@@ -20,7 +18,7 @@ variable [AddCommGroup W] [Module R W] [IsModuleConvexSpace R W] [hom : IsHomoge
 
 open PointedCone
 
-/-- The Homogenization cone of a polytope is finitely generated. -/
+/-- The homogenization cone of a polytope is finitely generated. -/
 theorem IsPolytope.of_homogenize_FG {C : ConvexSet R A} (hCfg : IsPolytope R (C : Set A)) :
     (homogenize W C).FG := by
   obtain ⟨t, ht⟩ := hCfg
@@ -36,8 +34,27 @@ theorem IsPolytope.of_homogenize_FG {C : ConvexSet R A} (hCfg : IsPolytope R (C
 /-- A convex set is a polytope iff its homogenization cone is finitely generated. -/
 theorem IsPolytope.iff_homogenize_FG {C : ConvexSet R A} :
     IsPolytope R (C : Set A) ↔ (homogenize W C).FG := by
-  refine ⟨fun P ↦ IsPolytope.of_homogenize_FG P, ?_⟩
-  sorry -- issue #62
+  refine ⟨fun P ↦ IsPolytope.of_homogenize_FG P, fun hfg ↦ ?_⟩
+  -- get cone generators that lie in the embedding of A
+  obtain ⟨g, hg, hs⟩ := homogenize_FG_ofPoint_range hfg
+  classical
+  -- un-embed them
+  use g.preimage hom.ofPoint hom.ofPoint_injective.injOn
+  -- show they generate C
+  simp only [Finset.coe_preimage]
+  apply le_antisymm
+  · intro x hx
+    rw [← preimage_hull_eq_convexHull_preimage hs]
+    simp only [hg, homogenize]
+    exact Submodule.mem_span_of_mem <| Set.mem_image_of_mem hom.ofPoint hx
+  · apply C.isConvexSet.convexHull_subset_iff.mpr
+    intro x hx
+    simp only [Set.mem_preimage, SetLike.mem_coe] at hx
+    have := Set.mem_preimage.mpr <| Submodule.mem_span_of_mem (R := {c : R // 0 ≤ c}) hx
+    simp_rw [hg, homogenize] at this
+    rw [preimage_hull_eq_convexHull_preimage (Set.image_subset_range hom.ofPoint C)] at this
+    rw [← C.isConvexSet.convexHull_eq_self]
+    simpa [← C.isConvexSet.convexHull_eq_self, Set.preimage_image_eq _ hom.ofPoint_injective]
 
 end Ring
 
@@ -49,9 +66,11 @@ attribute [local instance] AddTorsor.toConvexSpace
 variable [AddCommGroup W] [Module R W] [IsModuleConvexSpace R W] [hom : IsHomogenization R A W]
 
 open Pointwise Submodule in
-/-- Dehomogenizing a finitely generated salient cone yields a polytope. -/
+/-- Dehomogenizing a finitely generated positive cone yields a polytope. -/
 theorem FG.dehomogenize_isPolytope {C : PointedCone R W} (h : C.FG)
     (hc : ∀ c ∈ C, c ≠ 0 → 0 < hom.weight c) :
-    IsPolytope R (dehomogenize A C : Set A) := by sorry -- issue #60
+    IsPolytope R (dehomogenize A C : Set A) := by
+  apply (IsPolytope.iff_homogenize_FG (hom := hom)).mpr
+  simpa [homogenize_dehomogenize_of_le_positive hc]
 
 end Field

Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean

@@ -62,6 +62,32 @@ lemma weight_nonneg_of_mem_homogenize {x : W} {P : ConvexSet R A} (h : x ∈ hom
 lemma homogenize_salient {K : ConvexSet R A} : PointedCone.Salient (homogenize W K) :=
   Salient.of_le_salient hom.weight.positive_salient (homogenize_le_weight_positive K)
 
+theorem homogenize_FG_ofPoint_range {C : ConvexSet R A} (h : (homogenize W C).FG) :
+    ∃ g : Finset W, PointedCone.hull R g = homogenize W C ∧
+      (g : Set W) ⊆ Set.range hom.ofPoint := by
+  obtain ⟨g, hg⟩ := h
+  -- express each generator as a positive combo of stuff in the embedding of C
+  have gsum {x} (hx : x ∈ g) := mem_hull_set.mp (hg ▸ (Submodule.mem_span_of_mem hx))
+  classical
+  -- collect all said stuff and use as the new generators
+  let g' := g.attach.biUnion (fun x => (Classical.choose (gsum x.2)).support)
+  use g'
+
+  have g'sub : (g' : Set W) ⊆ hom.ofPoint '' C := by
+    simpa [g'] using fun _ b ↦ (Classical.choose_spec (gsum b)).1
+
+  have gsubhull : (g : Set W) ⊆ hull R (g' : Set W) := by
+    intro x hx
+    obtain ⟨_, hnn, hsum⟩ := Classical.choose_spec (gsum hx)
+    refine hsum ▸ mem_hull_set.mpr ⟨Classical.choose (gsum hx), ?_, hnn, rfl⟩
+    simpa using Finset.subset_biUnion_of_mem
+      (fun p ↦ (Classical.choose (gsum p.2)).support) (Finset.mem_attach g ⟨x, hx⟩)
+
+  refine ⟨le_antisymm (hull_mono g'sub) ?_, g'sub.trans (by simp)⟩
+  simpa [hg] using hull_mono (R := R) gsubhull
+
+section Module
+
 attribute [local instance] AddTorsor.toConvexSpace
 variable [IsModuleConvexSpace R W] -- WARNING: this is currently inferred! This is dangerous
 
@@ -94,6 +120,14 @@ lemma ofPoint_dehomogenize_eq_inter_ofPoint (C : PointedCone R W) :
     use y
     simpa
 
+/-- The preimage of the conic hull of a set in the homogenization plane is the convex hull of the
+preimage of the set. -/
+theorem hull_image_ofPoint_eq_homogenize_convexHull {s : Set A} :
+    hull R (hom.ofPoint '' s) = homogenize W ⟨Convexity.convexHull R s, .convexHull⟩ := by
+  simp [homogenize, hom.ofPoint.isAffineMap.image_convexHull]
+
+end Module
+
 end Ring
 
 section Field
@@ -131,6 +165,12 @@ lemma ofPoint_mem_homogenize_iff_mem (x : A) (P : ConvexSet R A) :
     dehomogenize A (homogenize W P) = P := by
   ext x; exact ofPoint_mem_homogenize_iff_mem _ _ _
 
+lemma homogenize_injective : Function.Injective (homogenize (hom := hom) W) := by
+  intro P Q h
+  have hh := congr_arg (ConvexSet.dehomogenize A) h
+  simp [dehomogenize_homogenize] at hh
+  assumption
+
 /-- If the entire cone save the origin are at positive weight, homogenizing the dehomogenization
 of the homogenize yields the cone again. -/
 theorem homogenize_dehomogenize_of_le_positive {C : PointedCone R W}