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..034887e4 --- /dev/null +++ b/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 diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean index 92281818..36817285 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean +++ b/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 diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean index 8f58b4ff..af80c786 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean +++ b/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}