From 15ba9522f7c1583e294ab56b19df300b5ade03a2 Mon Sep 17 00:00:00 2001
From: ovi <ovi@posteo.de>
Date: Tue, 23 Jun 2026 12:17:49 +0200
Subject: [PATCH 1/4] proving a convex set is a polytope iff the hom cone is
 FG. solves issue #62

---
 .../ConvexSpace/Polytope/Homogenization.lean  | 30 ++++++-
 .../ConvexSpace/Set/Homogenization.lean       | 86 +++++++++++++++++++
 2 files changed, 112 insertions(+), 4 deletions(-)

diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean
index 92281818..586a9358 100644
--- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean
+++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean
@@ -3,6 +3,7 @@ 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
+import Mathlib.Data.Finset.SDiff
 
 /-! This file proves results about polytopes, FG cones and homogenization. -/
 
@@ -36,8 +37,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
+    apply mem_convexHull_preimage_of_apply_mem_hull 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
+    rw [← C.isConvexSet.convexHull_eq_self]
+    intro x hx
+    simp only [Set.mem_preimage, SetLike.mem_coe] at hx
+    have := Submodule.mem_span_of_mem (R := {c : R // 0 ≤ c}) hx
+    simp_rw [hg] at this
+    have := mem_convexHull_preimage_of_apply_mem_hull (Set.image_subset_range _ _) this
+    simpa [Set.preimage_image_eq _ hom.ofPoint_injective]
 
 end Ring
 
@@ -49,9 +69,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
diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean
index 8f58b4ff..ba8f8b41 100644
--- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean
+++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean
@@ -22,6 +22,57 @@ variable [hom : Affine.IsHomogenization R A W]
 
 attribute [local instance] AddTorsor.toConvexSpace
 
+section Module
+
+variable [IsModuleConvexSpace R W]
+
+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))
+
+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
+
+theorem mem_convexHull_preimage_of_apply_mem_hull {x s} (hs : s ⊆ Set.range hom.ofPoint)
+    (h : hom.ofPoint x ∈ hull R s) : x ∈ Convexity.convexHull R (hom.ofPoint ⁻¹' s) := by
+  rw [← preimage_hull_eq_convexHull_preimage hs]
+  simpa [Set.image_preimage_eq_of_subset hs]
+
+end Module
+
 variable (W) in
 /-- The homogenization cone of a convex set in an affine space. -/
 def homogenize (P : ConvexSet R A) : PointedCone R W := hull R (hom.ofPoint '' P)
@@ -62,6 +113,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 +171,9 @@ lemma ofPoint_dehomogenize_eq_inter_ofPoint (C : PointedCone R W) :
     use y
     simpa
 
+
+end Module
+
 end Ring
 
 section Field
@@ -131,6 +211,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}

From 880b6fae5992bd3aab3092434c53b82e310f454c Mon Sep 17 00:00:00 2001
From: ovi <ovi@posteo.de>
Date: Tue, 23 Jun 2026 12:48:50 +0200
Subject: [PATCH 2/4] cleanup

---
 Polyhedral.lean                               |  9 ++-
 .../Convex/ConvexSpace/Homogenization.lean    | 79 +++++++++++++++++++
 .../ConvexSpace/Polytope/Homogenization.lean  |  7 +-
 .../ConvexSpace/Set/Homogenization.lean       | 51 ------------
 4 files changed, 86 insertions(+), 60 deletions(-)
 create mode 100644 Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean

diff --git a/Polyhedral.lean b/Polyhedral.lean
index 119b25bc..318af51d 100644
--- a/Polyhedral.lean
+++ b/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
diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean
new file mode 100644
index 00000000..2a4f96a1
--- /dev/null
+++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean
@@ -0,0 +1,79 @@
+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
+
+open Convexity
+
+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
+
+theorem mem_convexHull_preimage_of_apply_mem_hull {x s} (hs : s ⊆ Set.range hom.ofPoint)
+    (h : hom.ofPoint x ∈ hull R s) : x ∈ Convexity.convexHull R (hom.ofPoint ⁻¹' s) := by
+  rw [← preimage_hull_eq_convexHull_preimage hs]
+  simpa [Set.image_preimage_eq_of_subset hs]
+
+end Module
+
+end Ring
+
+end Convexity
diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean
index 586a9358..255380e4 100644
--- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean
+++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean
@@ -1,9 +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
-import Mathlib.Data.Finset.SDiff
 
 /-! This file proves results about polytopes, FG cones and homogenization. -/
 
@@ -21,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
diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean
index ba8f8b41..1a1235b6 100644
--- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean
+++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean
@@ -22,57 +22,6 @@ variable [hom : Affine.IsHomogenization R A W]
 
 attribute [local instance] AddTorsor.toConvexSpace
 
-section Module
-
-variable [IsModuleConvexSpace R W]
-
-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))
-
-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
-
-theorem mem_convexHull_preimage_of_apply_mem_hull {x s} (hs : s ⊆ Set.range hom.ofPoint)
-    (h : hom.ofPoint x ∈ hull R s) : x ∈ Convexity.convexHull R (hom.ofPoint ⁻¹' s) := by
-  rw [← preimage_hull_eq_convexHull_preimage hs]
-  simpa [Set.image_preimage_eq_of_subset hs]
-
-end Module
-
 variable (W) in
 /-- The homogenization cone of a convex set in an affine space. -/
 def homogenize (P : ConvexSet R A) : PointedCone R W := hull R (hom.ofPoint '' P)

From ae16b16a58f7af03b70c1515843468b0875fd117 Mon Sep 17 00:00:00 2001
From: ovi <ovi@posteo.de>
Date: Tue, 23 Jun 2026 14:49:27 +0200
Subject: [PATCH 3/4] cleanup, solving issue #54

---
 .../Geometry/Convex/ConvexSpace/Homogenization.lean  |  7 -------
 .../Convex/ConvexSpace/Polytope/Homogenization.lean  | 12 ++++++------
 .../Convex/ConvexSpace/Set/Homogenization.lean       |  5 +++++
 3 files changed, 11 insertions(+), 13 deletions(-)

diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean
index 2a4f96a1..e79de305 100644
--- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean
+++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean
@@ -8,8 +8,6 @@ namespace Convexity
 
 section Ring
 
-open Convexity
-
 variable {R : Type*} [Ring R] [PartialOrder R] [IsStrictOrderedRing R]
 variable {V : Type*} [AddCommGroup V] [Module R V]
 variable {A : Type*} [AddTorsor V A]
@@ -67,11 +65,6 @@ theorem preimage_hull_eq_convexHull_preimage {s : Set W} (hs : s ⊆ Set.range h
     rw [hom.ofPoint.isAffineMap.image_convexHull, Set.image_preimage_eq_iff.mpr hs]
     exact (hull R s).isConvexSet.convexHull_subset_iff.mpr subset_hull
 
-theorem mem_convexHull_preimage_of_apply_mem_hull {x s} (hs : s ⊆ Set.range hom.ofPoint)
-    (h : hom.ofPoint x ∈ hull R s) : x ∈ Convexity.convexHull R (hom.ofPoint ⁻¹' s) := by
-  rw [← preimage_hull_eq_convexHull_preimage hs]
-  simpa [Set.image_preimage_eq_of_subset hs]
-
 end Module
 
 end Ring
diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean
index 255380e4..36817285 100644
--- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean
+++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean
@@ -44,17 +44,17 @@ theorem IsPolytope.iff_homogenize_FG {C : ConvexSet R A} :
   simp only [Finset.coe_preimage]
   apply le_antisymm
   · intro x hx
-    apply mem_convexHull_preimage_of_apply_mem_hull hs
+    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
-    rw [← C.isConvexSet.convexHull_eq_self]
     intro x hx
     simp only [Set.mem_preimage, SetLike.mem_coe] at hx
-    have := Submodule.mem_span_of_mem (R := {c : R // 0 ≤ c}) hx
-    simp_rw [hg] at this
-    have := mem_convexHull_preimage_of_apply_mem_hull (Set.image_subset_range _ _) this
-    simpa [Set.preimage_image_eq _ hom.ofPoint_injective]
+    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
 
diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean
index 1a1235b6..af80c786 100644
--- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean
+++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean
@@ -120,6 +120,11 @@ 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
 

From 2aec8e5f9679d0eb83522b3e2a8f28fec8177a74 Mon Sep 17 00:00:00 2001
From: ovi <ovi@posteo.de>
Date: Tue, 23 Jun 2026 14:56:10 +0200
Subject: [PATCH 4/4] adding reverse

---
 .../Geometry/Convex/ConvexSpace/Homogenization.lean       | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean
index e79de305..034887e4 100644
--- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean
+++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean
@@ -65,6 +65,14 @@ theorem preimage_hull_eq_convexHull_preimage {s : Set W} (hs : s ⊆ Set.range h
     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