diff --git a/Polyhedral.lean b/Polyhedral.lean index 242f3273..27628350 100644 --- a/Polyhedral.lean +++ b/Polyhedral.lean @@ -53,6 +53,7 @@ public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polyhedron.Lattice public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Basic public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Face public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Homogenization +public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.KreinMilman public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Lattice public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Pointwise public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Face.Basic @@ -64,11 +65,11 @@ public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Lattice public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.WithTop public import Polyhedral.Mathlib.Geometry.Convex.Fun.Defs public import Polyhedral.Mathlib.Geometry.Convex.Fun.Dual +public import Polyhedral.Mathlib.Geometry.Convex.Segment public import Polyhedral.Mathlib.GroupTheory.GroupAction.SubMulActionWithZero public import Polyhedral.Mathlib.GroupTheory.GroupAction.SubMulActionWithZero.Closure public import Polyhedral.Mathlib.GroupTheory.GroupAction.SubMulActionWithZero.Nonneg public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic -public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Range public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Defs public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.IsHomogenization public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.Set diff --git a/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Finite/Face/KreinMilman.lean b/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Finite/Face/KreinMilman.lean index 5ba34f43..df2834aa 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Finite/Face/KreinMilman.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Finite/Face/KreinMilman.lean @@ -1,19 +1,21 @@ /- -Copyright (c) 2025 Olivia Röhrig, Martin Winter. All rights reserved. +Copyright (c) 2026 Moritz Firsching. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Olivia Röhrig, Martin Winter +Authors: Moritz Firsching -/ module -public import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Finite.Face.Basic +public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Homogenization +public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.KreinMilman /-! In this file we prove the Krein-Milman theorem for FG cones: every finitely generated cone is spanned by its rays, that is, by the finite set of its 1-dimensional faces. -TODO: aspects of the proof are rather cumbersome since the atoms of the face lattice are rays -rather than points. We therefore intend to perform the proof on the polytope side and -transfer it here using homogenization. --/ +The theorem is derived from the Krein-Milman theorem for polytopes +(`IsPolytope.krein_milman`): a salient FG cone admits a linear functional that is positive on +all of its nonzero elements, the slice of the cone at weight one is a polytope, and the cone +is the homogenization of that slice, so its rays are the homogenizations of the vertices of +the slice. -/ @[expose] public section @@ -23,159 +25,21 @@ variable {R M : Type*} section Field -variable [Field R] [LinearOrder R] [IsOrderedRing R] +variable [Field R] [LinearOrder R] [IsStrictOrderedRing R] variable [AddCommGroup M] [Module R M] -variable {C F F₁ F₂ : PointedCone R M} - -section opt - -/- The minimum of `f/g` on a cone. -/ -def opt (C : PointedCone R M) (f g : M →ₗ[R] R) : PointedCone R M where - carrier := {x ∈ C | ∀ y ∈ C, f x * g y ≤ f y * g x} - add_mem' := by - intro a b ha hb - simp only [Set.mem_ofPred_eq, map_add] at * - refine ⟨C.add_mem ha.1 hb.1, ?_⟩ - intro y hy - rw [add_mul, mul_add] - exact add_le_add (ha.2 y hy) (hb.2 y hy) - zero_mem' := by simp only [Set.mem_ofPred_eq, zero_mem, map_zero, zero_mul, mul_zero, le_refl, - implies_true, and_self] - smul_mem' := by - intro a x hx - refine ⟨C.smul_mem a.2 hx.1, ?_⟩ - intro y hy - by_cases! h : a ≤ 0 - · simp [nonpos_iff_eq_zero.mp h] - simp only [LinearMap.map_smul_of_tower, Algebra.smul_mul_assoc, Algebra.mul_smul_comm] - exact (smul_le_smul_iff_of_pos_left h).mpr <| hx.2 y hy - --- TODO: the proof was modified after features changed and needs golfing: --- * `Salient.of_le_positive` was hacked in. --- * `mem_positive'` was hacked in to recover the previous form of `hg`. -lemma IsFaceOf.of_opt (C : PointedCone R M) (f g : M →ₗ[R] R) (hCg : C ≤ g.positive) : - (C.opt f g).IsFaceOf C := by - have hg : ∀ x ∈ C, 0 ≤ g x ∧ (g x = 0 → x = 0) := -- hacked in to recover `hg` - fun _ hx => g.mem_positive'.mp (hCg hx) - refine ⟨fun _ hx ↦ hx.1, ?_⟩ - intro x y a hx hy ha ⟨h2, h⟩ - by_cases! x_ne_0 : x = 0 - · rw [x_ne_0]; exact zero_mem (C.opt f g) - by_cases! t_ne_0 : a • x + y = 0 - · exfalso - have hC' := Salient.of_le_positive hCg - exact (smul_ne_zero (ne_of_gt ha) x_ne_0) <| - hC' (a • x) (C.smul_mem (le_of_lt ha) hx) y hy t_ne_0 - refine ⟨hx, fun z hz ↦ ?_⟩ - have : g x > 0 := lt_of_le_of_ne (hg _ hx).1 (fun h ↦ x_ne_0 <| (hg _ hx).2 (Eq.symm h)) - have t1 := h x hx - have t2 := h y hy - have t4 := (mul_le_mul_iff_of_pos_left this).mpr <| (h z hz) - simp only [map_add, map_smul, smul_eq_mul] at t1 t2 t4 - have local_lemma : ∀ {a b c d e : R}, e > 0 → a ≤ b → c ≤ d → e * a + c = e * b + d → a = b := - fun _ _ _ _ ↦ by nlinarith - have t3 : (a * f x + f y) * g x = f x * (a * g x + g y) := local_lemma ha t1 t2 (by ring) - have : a * g x + g y > 0 := by - simpa only [gt_iff_lt, map_add, map_smul, smul_eq_mul] using - lt_of_le_of_ne (hg _ h2).1 (fun h ↦ t_ne_0 <| (hg _ h2).2 (Eq.symm h)) - apply (mul_le_mul_iff_of_pos_left this).mp - nth_rw 3 [mul_comm] at t3 - rw [← mul_assoc, ← t3] - linarith - -lemma FG.exists_ne_zero_mem_opt (C : PointedCone R M) (hC : C.FG) (hC0 : C ≠ ⊥) (f g : M →ₗ[R] R) - (hCg : C ≤ g.positive) : ∃ x, x ≠ 0 ∧ x ∈ C.opt f g := by classical - have hg : ∀ x ∈ C, 0 ≤ g x ∧ (g x = 0 → x = 0) := -- hacked in to recover `hg` - fun _ hx => g.mem_positive'.mp (hCg hx) - obtain ⟨s, hs⟩ := hC - have hs0 : ∃ z ∈ s, z ≠ 0 := by - by_contra hs0 - push Not at hs0 - exact hC0 <| by rw [← hs]; exact Submodule.span_eq_bot.mpr hs0 - have hg_pos : ∀ {z : M}, z ∈ C → z ≠ 0 → 0 < g z := by - intro z hz hz0 - exact lt_of_le_of_ne (hg _ hz).1 (fun h ↦ hz0 <| (hg _ hz).2 (Eq.symm h)) - let s0 : Finset M := s.filter fun z => z ≠ 0 - have hs0_ne : s0.Nonempty := by - rcases hs0 with ⟨z, hzs, hz0⟩ - exact ⟨z, by simp [s0, hzs, hz0]⟩ - obtain ⟨x, hx0, hxmin⟩ := Finset.exists_min_image s0 (fun z => f z / g z) hs0_ne - have hxs : x ∈ s := (Finset.mem_filter.mp hx0).1 - have hx_ne_0 : x ≠ 0 := (Finset.mem_filter.mp hx0).2 - have hxC : x ∈ C := by rw [← hs]; exact subset_hull hxs - have hgx : 0 < g x := hg_pos hxC hx_ne_0 - have hgen : ∀ z ∈ s, f x * g z ≤ f z * g x := by - intro z hzs - by_cases hz0 : z = 0 - · simp [hz0] - have hzC : z ∈ C := by rw [← hs]; exact subset_hull hzs - have hgz : 0 < g z := hg_pos hzC hz0 - have hz0' : z ∈ s0 := by simp [s0, hzs, hz0] - exact (div_le_div_iff₀ hgx hgz).1 (hxmin _ hz0') - refine ⟨x, hx_ne_0, ?_⟩ - refine ⟨hxC, ?_⟩ - intro y hy - rw [← hs] at hy - induction hy using Submodule.span_induction with - | mem z hz => exact hgen z hz - | zero => - simp - | add y z _ _ hy hz => - simpa [map_add, add_mul, mul_add] using add_le_add hy hz - | smul a y _ hy => - have hy' := mul_le_mul_of_nonneg_left hy a.2 - simp only [LinearMap.map_smul_of_tower, Algebra.mul_smul_comm, Algebra.smul_mul_assoc, - ge_iff_le] - exact hy' - -lemma FG.opt_neq_bot (C : PointedCone R M) (hC : C.FG) (hC0 : C ≠ ⊥) (f g : M →ₗ[R] R) - (hCg : C ≤ g.positive) : C.opt f g ≠ ⊥ := by - rcases FG.exists_ne_zero_mem_opt C hC hC0 f g hCg with ⟨x, hx0, hxopt⟩ - exact fun hbot => hx0 <| by simpa [hbot] using hxopt - -end opt +variable {C : PointedCone R M} -/- For every ray `x` of the span of a set `s`, there is a member of `s` that also spans the ray. -/ -lemma IsFaceOf.hull_ray {s : Set M} {x : M} (hx : x ≠ 0) - (hspan : (R ∙₊ x).IsFaceOf (hull R s)) : ∃ y ∈ s, ∃ c : R, 0 < c ∧ y = c • x := by - have h := hspan.hull_inter_face_hull_inf_face - have ⟨y, hy, hy0⟩ : ∃ w ∈ s ∩ (R ∙₊ x), w ≠ 0 := by - by_contra H - absurd hx - push Not at H - simp only [← Set.mem_singleton_iff] at H - simpa [h] using Submodule.span_mono (R := {c : R // 0 ≤ c}) H - simp only [Set.mem_inter_iff, SetLike.mem_coe, Submodule.mem_span_singleton, - Subtype.exists] at hy - obtain ⟨hys, a, ha, rfl⟩ := hy - exact ⟨_, hys, a, lt_of_le_of_ne ha (fun h => hy0 (by simp [← h])), rfl⟩ +open Convexity Affine Affine.IsHomogenization -open Module in /-- Krein-Milman theorem: every finitely generated cone is spanned by its rays, that is, by the finite set of its 1-dimensional faces. -/ lemma FG.krein_milman (hfg : C.FG) (hsal : C.Salient) : ∃ s : Finset M, hull R s = C ∧ ∀ x ∈ s, (R ∙₊ x).IsFaceOf C := by classical - let ⟨s, hs⟩ := hfg - by_cases hs' : s = ∅ - · exact ⟨∅, by simp [← hs, hs']⟩ - by_contra! h - let t := s.filter fun x => (R ∙₊ x).IsFaceOf C - specialize h t - have hts : t ⊆ s := by simp [t] - have hst : ¬(s : Set M) ⊆ hull R (t : Set M) := by - by_contra h' - have h' := Submodule.span_mono (R := {c : R // 0 ≤ c}) h' - have h'' := Submodule.span_mono (R := {c : R // 0 ≤ c}) hts - simp only [Submodule.span_coe_eq_restrictScalars, Submodule.restrictScalars_self] at h' - rw [← le_antisymm h' h'', hs] at h - simp [t, and_assoc] at h - obtain ⟨x, hxs, hxt⟩ := Set.not_subset.mp hst - have hx : x ∈ C := by - rw [← hs] - exact subset_hull hxs - obtain ⟨f, hf, hf'⟩ := FG.farkas (Dual.eval R M) hxt + by_cases hbot : C = ⊥ + · exact ⟨∅, by simp [hbot]⟩ + -- a linear functional that is positive on all nonzero elements of `C` obtain ⟨g, hg, hgker⟩ := IsExposedFaceOf.lineal hfg have hker : C ⊓ g.ker = ⊥ := by rw [← hgker] @@ -188,50 +52,31 @@ lemma FG.krein_milman (hfg : C.FG) (hsal : C.Salient) : have : y ∈ C ⊓ g.ker := ⟨hy, hgy⟩ rw [hker] at this simpa using this - simp only [Dual.eval_apply] at hf hf' - let F := C.opt f g - have hF : F.IsFaceOf C := IsFaceOf.of_opt C f g hgC - have hC0 : C ≠ ⊥ := by - intro hC0 - have : x = 0 := by simpa [hC0] using hx - exact hxt (by simp [this]) - have hF' := opt_neq_bot C hfg hC0 f g hgC - have hFsal := Salient.of_le_salient hsal hF.le - obtain ⟨r, hr0, hrF⟩ := exists_ray (hF.fg hfg) hF' hFsal - have hr := IsFaceOf.trans hrF hF - rw [← hs] at hr - obtain ⟨w, hws, c, hc', h⟩ := hr.hull_ray hr0 - simp only [SetLike.mem_coe] at hws - have hc0 := (ne_of_lt hc').symm - have hrw : r = c⁻¹ • w := by - subst h hs - simp [smul_smul, hc0] - rw [hrw] at hr - rw [hull_singleton_smul_eq (inv_pos.mpr hc')] at hr - have hwt : w ∈ t := by - simpa [Finset.mem_filter, t] using ⟨hws, hs ▸ hr⟩ - have hwF : r ∈ F := by - have : r ∈ hull R {r} := by simp - exact hrF.le this - have hwF : w ∈ F := by - rw [h] - exact F.smul_mem (le_of_lt hc') hwF - simp only [opt, Submodule.mem_mk, AddSubmonoid.mem_mk, AddSubsemigroup.mem_mk, Set.mem_ofPred_eq, - F] at hwF - have hgw : 0 < g w := by - have hw0 : w ≠ 0 := by - rw [h] - exact smul_ne_zero hc0 hr0 - by_contra! h - have hgw := g.mem_positive'.mp (hgC hwF.1) - have hgw' := le_antisymm hgw.1 h - have := hgw.2 hgw'.symm - absurd hxt - contradiction - have hwF := hwF.2 x hx - have : 0 ≤ f w * g x := mul_nonneg (hf' w hwt) (g.mem_positive'.mp (hgC hx)).1 - have : f x * g w < 0 := mul_neg_of_neg_of_pos hf hgw - linarith + -- the weight-one slice of `C` is nonempty + obtain ⟨y, hyC, hy0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hbot + have hg : g ≠ 0 := fun h ↦ hy0 <| by simpa [h] using (LinearMap.mem_positive'.mp (hgC hyC)).2 + -- choose the homogenization whose affine space is the weight-one plane + let ℋ := IsHomogenization.ofWeightNeZero hg + -- view `C` as the homogenization of its weight-one slice + let weightOnePlane := AffineSubspace.comap (g.toAffineMap) {1} + have : Nonempty weightOnePlane := + Function.Surjective.nonempty (Set.restrictPreimage_surjective {1} (g.surjective_of_ne_zero hg)) + let : ConvexSpace R weightOnePlane := .ofAddTorsor + let : ConvexSpace R M := .ofModule + have hCP : homogenize ℋ (dehomogenize ℋ C) = C := + homogenize_dehomogenize_of_le_positive ((weight_ofWeightNeZero hg).symm ▸ hgC) + -- the slice is a polytope; apply the Krein-Milman theorem for polytopes + have hP : IsPolytope R (dehomogenize ℋ C : Set weightOnePlane) := by + rw [IsPolytope.iff_homogenize_fg (W := M), hCP] + · exact hfg + · exact dehomogenize_isConvexSet ℋ C + obtain ⟨s, hs, hface⟩ := IsPolytope.krein_milman hP + refine ⟨s.image ℋ.ofPoint, ?_, ?_⟩ + · rw [Finset.coe_image, hull_image_ofPoint_eq_homogenize_convexHull, hs, hCP] + · intro x hx + obtain ⟨q, hq, rfl⟩ := Finset.mem_image.mp hx + have h := homogenize_isFaceOf ℋ (dehomogenize_isConvexSet ℋ C) (hface q hq) + rwa [homogenize_singleton, hCP] at h end Field diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Order.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Order.lean index a92cc733..e68bc405 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Order.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Order.lean @@ -115,7 +115,7 @@ lemma upperMass_eq_one_iff : w.upperMass x = 1 ↔ ∀ y, w.weights y ≠ 0 → refine ⟨fun h1 y hy ↦ ?_, fun hall ↦ ?_⟩ · rw [h1] at h have hz := add_left_cancel (h.trans (add_zero 1).symm) - by_contra! hxy + by_contra hxy exact hy <| (Finset.sum_eq_zero_iff_of_nonneg fun _ _ ↦ w.weights_nonneg _).1 hz y <| by simp [hy, hxy] · rwa [Finset.sum_eq_zero fun y ↦ by simp +contextual [hall], add_zero] at h diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polyhedron/Lattice.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polyhedron/Lattice.lean index 7ac33064..9f9e4cc5 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polyhedron/Lattice.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polyhedron/Lattice.lean @@ -17,7 +17,7 @@ namespace Convexity open Convexity variable {R : Type*} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] -variable {V : Type*} [AddCommGroup V] [Module R V] -- [ConvexSpace R V] [IsModuleConvexSpace R V] +variable {V : Type*} [AddCommGroup V] [Module R V] variable {A : Type*} [AddTorsor V A] [ConvexSpace R A] variable (R A) in @@ -50,11 +50,6 @@ section IsModuleConvexSpace variable [ConvexSpace R V] [IsModuleConvexSpace R V] [IsAffineConvexSpace R V A] -@[coe] def toConvexSet (P : Polyhedron R A) : ConvexSet R A := - ⟨P, P.isPolyhedron.isConvexSet⟩ - -instance : Coe (Polyhedron R A) (ConvexSet R A) := ⟨toConvexSet⟩ - end IsModuleConvexSpace /- # LE -/ diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Face.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Face.lean index 3ad5e25f..cc5dcc02 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Face.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Face.lean @@ -7,6 +7,7 @@ module public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Lattice public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Face.Homogenization +public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Face.Lattice import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Finite.Face.Grade import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Homogenization @@ -18,7 +19,9 @@ public section variable {R V A : Type*} -open Convexity ConvexSet Affine +open Convexity IsConvexSet Affine + +namespace Convexity section Field @@ -26,20 +29,20 @@ variable [Field R] [LinearOrder R] [IsStrictOrderedRing R] variable [AddCommGroup V] [Module R V] variable [AddTorsor V A] [ConvexSpace R A] [IsAffineConvexSpace R V A] -variable {C F : ConvexSet R A} +variable {C F : Set A} include V in /-- Faces of polytopes are polytopes. -/ -theorem IsPolytope.face_isPolytope (hC : IsPolytope R (C : Set A)) (hF : IsFaceOf F C) : +theorem IsPolytope.face_isPolytope (hC : IsPolytope R C) (hF : IsFaceOf R F C) : IsPolytope R (F : Set A) := by let : ConvexSpace R (Homogenization R A) := ConvexSpace.ofModule - have homF := (IsHomogenization.canonical R A).homogenize_isFaceOf hF + have homF := (IsHomogenization.canonical R A).homogenize_isFaceOf hC.isConvexSet hF have := PointedCone.IsFaceOf.fg (IsPolytope.homogenize_fg _ hC) homF convert FG.dehomogenize_isPolytope this (fun _ a b ↦ weight_pos_of_mem_homogenize a b) - simp [dehomogenize_homogenize] + rw [dehomogenize_homogenize _ hF.isConvexSet] include V in -instance {P : Polytope R A} : CoeOut (Face (P : ConvexSet R A)) (Polytope R A) where +instance {P : Polytope R A} : CoeOut (Face P.isPolytope.isConvexSet) (Polytope R A) where coe F := ⟨_, IsPolytope.face_isPolytope P.isPolytope F.isFaceOf⟩ include V in @@ -49,12 +52,14 @@ homogenization cones. 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 + GradeOrder ℕ (Face P.isPolytope.isConvexSet) := by let : ConvexSpace R (Homogenization R A) := ConvexSpace.ofModule let ℋ := IsHomogenization.canonical R A - have : (homogenize _ (P : ConvexSet R A)).FG := IsPolytope.homogenize_fg ℋ P.isPolytope + have : (homogenize _ P).FG := IsPolytope.homogenize_fg ℋ P.isPolytope let := PointedCone.FG.gradeOrder_finrank this - refine GradeOrder.liftRight _ (face_homogenizeIso ℋ P).strictMono ?_ + refine GradeOrder.liftRight _ (face_homogenizeIso ℋ P.isPolytope.isConvexSet).strictMono ?_ exact fun x y ↦ (apply_covBy_apply_iff _).mpr end Field + +end Convexity diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean index af88ac64..2f5d3287 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean @@ -17,7 +17,7 @@ public section variable {R V W A : Type*} -open Convexity ConvexSet Affine IsHomogenization +open Convexity Affine IsHomogenization section Ring @@ -33,21 +33,20 @@ variable (ℋ : IsHomogenization R A W) open PointedCone /-- The homogenization of a polytope is a finitely generated cone. -/ -theorem IsPolytope.homogenize_fg {C : ConvexSet R A} (hCfg : IsPolytope R (C : Set A)) : +theorem IsPolytope.homogenize_fg {C : Set A} (hCfg : IsPolytope R C) : (homogenize ℋ C).FG := by obtain ⟨t, ht⟩ := hCfg - have : C = ⟨convexHull R t, IsConvexSet.convexHull⟩ := SetLike.ext' ht - have := congrArg (ConvexSet.homogenize ℋ) this + have := congrArg (homogenize ℋ) ht rw [this] use t.map ⟨_, ℋ.ofPoint_injective⟩ simp only [Finset.coe_map, Function.Embedding.coeFn_mk, homogenize, - PointedCone.hull, ConvexSet.mk_eq] + PointedCone.hull] rw [ℋ.ofPoint.isAffineMap.image_convexHull t] exact (PointedCone.hull_convexHull (ℋ.ofPoint '' t)).symm /-- A convex set is a polytope iff its homogenization is a finitely generated cone. -/ -theorem IsPolytope.iff_homogenize_fg {C : ConvexSet R A} : - IsPolytope R (C : Set A) ↔ (homogenize ℋ C).FG := by classical +theorem IsPolytope.iff_homogenize_fg {C : Set A} (hC : IsConvexSet R C) : + IsPolytope R C ↔ (homogenize ℋ C).FG := by classical refine ⟨homogenize_fg _, fun hfg ↦ ?_⟩ -- get cone generators that lie in the embedding of A obtain ⟨g, hg, hs⟩ := homogenize_fg_ofPoint_range hfg @@ -60,14 +59,14 @@ theorem IsPolytope.iff_homogenize_fg {C : ConvexSet R A} : rw [← preimage_hull_eq_convexHull_preimage hs] simp only [hg, homogenize] exact Submodule.mem_span_of_mem <| Set.mem_image_of_mem ℋ.ofPoint hx - · apply C.isConvexSet.convexHull_subset_iff.mpr + · apply hC.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 ℋ.ofPoint C)] at this - rw [← C.isConvexSet.convexHull_eq_self] - simpa [← C.isConvexSet.convexHull_eq_self, Set.preimage_image_eq _ ℋ.ofPoint_injective] + rw [← hC.convexHull_eq_self] + simpa [hC.convexHull_eq_self, Set.preimage_image_eq _ ℋ.ofPoint_injective] end Ring @@ -86,7 +85,7 @@ open Pointwise Submodule in /-- Dehomogenizing a finitely generated positive cone yields a polytope. -/ theorem FG.dehomogenize_isPolytope {C : PointedCone R W} (h : C.FG) (hc : C ≤ ℋ.weight.positive) : IsPolytope R (dehomogenize ℋ C : Set A) := by - rw [IsPolytope.iff_homogenize_fg ℋ] + rw [IsPolytope.iff_homogenize_fg ℋ (dehomogenize_isConvexSet ℋ C)] simpa [homogenize_dehomogenize_of_le_positive hc] end Field diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/KreinMilman.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/KreinMilman.lean new file mode 100644 index 00000000..7679fc16 --- /dev/null +++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/KreinMilman.lean @@ -0,0 +1,96 @@ +/- +Copyright (c) 2026 Mortiz Firschinggit , Martin Winter. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mortiz Firsching +-/ +module + +public import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Finite.Face.Basic +public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Module +public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Basic +public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Face.Homogenization + +/-! In this file we prove the Krein-Milman theorem for polytopes: every polytope is the convex +hull of its vertices, that is, of the finite set of points whose singletons are faces. + +The proof is independent of the Krein-Milman theorem for FG cones +(`PointedCone.FG.krein_milman`); the cone version is instead derived from the present theorem +by slicing a salient cone at weight one. The key step here shows that a generator outside the +convex hull of the remaining generators spans a singleton face; this is obtained from the +cone-side lemma `PointedCone.span_singleton_isFaceOf_sup_singleton_of_not_mem` via +homogenization. -/ + +@[expose] public section + +variable {R V A : Type*} + +open Convexity Affine Affine.IsHomogenization PointedCone + +namespace Convexity + +section Field + +variable [Field R] [LinearOrder R] [IsStrictOrderedRing R] +variable [AddCommGroup V] [Module R V] +variable [AddTorsor V A] + +variable {P : Set A} + +variable [ConvexSpace R A] [IsAffineConvexSpace R V A] + +include V in +/-- If a point `x` does not lie in the convex hull of a set `s`, then the singleton of `x` is +a face of the convex hull of `insert x s`. -/ +lemma IsFaceOf.singleton_convexHull_insert {s : Set A} {x : A} (hx : x ∉ convexHull R s) : + IsFaceOf R ({x} : Set A) (convexHull R (insert x s)) := by + let : ConvexSpace R (Homogenization R A) := .ofModule + let ℋ := IsHomogenization.canonical R A + have hhom : homogenize (IsHomogenization.canonical R A) (convexHull R (insert x s)) = + PointedCone.hull R (ℋ.ofPoint '' s) ⊔ (R ∙₊ ℋ.ofPoint x) := by + rw [← hull_image_ofPoint_eq_homogenize_convexHull, Set.image_insert_eq, hull_insert, sup_comm] + have hnot : ℋ.ofPoint x ∉ PointedCone.hull R (ℋ.ofPoint '' s) := by + rw [hull_image_ofPoint_eq_homogenize_convexHull] + exact fun h => hx ((ofPoint_mem_homogenize_iff_mem _ x IsConvexSet.convexHull).mp h) + have hsal : (PointedCone.hull R (ℋ.ofPoint '' s) ⊔ (R ∙₊ ℋ.ofPoint x)).Salient := + hhom ▸ homogenize_salient _ _ + have hface := span_singleton_isFaceOf_sup_singleton_of_not_mem hnot hsal + rw [← hhom] at hface + have h := dehomogenize_isFaceOf ℋ hface + rwa [dehomogenize_homogenize, dehomogenize_hull_singleton_ofPoint ℋ x] at h + exact IsConvexSet.convexHull + +include V in +/-- Krein-Milman theorem for polytopes: every polytope is the convex hull of its vertices, +that is, of the finite set of points whose singletons are faces. -/ +theorem IsPolytope.krein_milman (hP : IsPolytope R P) : + ∃ s : Finset A, Convexity.convexHull R (s : Set A) = P ∧ ∀ x ∈ s, IsFaceOf R {x} P := by + classical + suffices h : ∀ t : Finset A, ∀ P : Set A, Convexity.convexHull R (t : Set A) = P → + ∃ s : Finset A, Convexity.convexHull R (s : Set A) = P ∧ ∀ x ∈ s, IsFaceOf R {x} P by + obtain ⟨t, ht⟩ := hP + exact h t P ht.symm + intro t + induction t using Finset.strongInduction with + | _ t ih => + intro P hP + by_cases hex : ∃ x ∈ t, x ∈ Convexity.convexHull R ((t.erase x : Finset A) : Set A) + · -- a redundant generator can be dropped and the induction hypothesis applies + obtain ⟨x, hxt, hx⟩ := hex + refine ih (t.erase x) (Finset.erase_ssubset hxt) P ?_ + rw [← hP] + refine subset_antisymm + (convexHull_mono (Finset.coe_subset.mpr (Finset.erase_subset x t))) ?_ + refine (IsConvexSet.convexHull_subset_iff IsConvexSet.convexHull).mpr ?_ + intro y hy + rcases eq_or_ne y x with rfl | hne + · exact hx + · exact subset_convexHull_self (Finset.mem_coe.mpr (Finset.mem_erase.mpr ⟨hne, hy⟩)) + · -- otherwise every generator is a vertex + push Not at hex + refine ⟨t, hP, fun x hxt => ?_⟩ + have h := IsFaceOf.singleton_convexHull_insert (R := R) (hex x hxt) + rwa [← Finset.coe_insert, Finset.insert_erase hxt, hP] at h + +end Field + +end Convexity diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Lattice.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Lattice.lean index c49cc73c..e1c12558 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Lattice.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Lattice.lean @@ -5,8 +5,10 @@ Authors: Martin Winter, Olivia Röhrig -/ module -public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Lattice public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Pointwise +public import Polyhedral.Mathlib.Data.SetLike.IsConcrete +public import Polyhedral.Mathlib.Algebra.Group.Pointwise.SetLike.Basic +public import Polyhedral.Mathlib.Algebra.Group.Pointwise.SetLike.Scalar /-! This file defines polytopes as bundles objects. -/ @@ -52,9 +54,6 @@ variable (P) in @[simp] theorem mk_eq {s h} : (⟨s, h⟩ : Polytope R X) = s := by ext; simp -instance : Coe (Polytope R X) (ConvexSet R X) where - coe P := ⟨P, P.isPolytope.isConvexSet⟩ - /- # LE -/ instance : PartialOrder (Polytope R X) := .ofSetLike .. @@ -162,8 +161,6 @@ instance : Neg (Polytope R X) where instance : IsConcreteNeg (Polytope R X) X := ⟨fun _ => rfl⟩ -instance : InvolutiveNeg (ConvexSet R X) := .ofSetLike .. - /-! ### Minkowski addition -/ instance : Add (Polytope R X) where diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Basic.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Basic.lean index 9ba2a405..85d1a258 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Basic.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Basic.lean @@ -1,184 +1,219 @@ /- -Copyright (c) 2026 Olivia Röhrig, Martin Winter. All rights reserved. +Copyright (c) 2025 Olivia Röhrig. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Olivia Röhrig, Mara Gruß, Valentina Taylor Cerra, Martin Winter +Authors: Olivia Röhrig -/ module -public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Lattice +public import Mathlib.Analysis.Convex.Extreme +public import Polyhedral.Mathlib.Geometry.Convex.Segment +public import Mathlib.Geometry.Convex.Set -/-! This file defines faces of convex sets. +/-! +# Faces of sets + +This file defines what it means for a set in a convex space to be a face of another set and +establishes basic properties of this relation. + +## Main declarations + +* `IsFaceOf F C`: States that the set `F` is a face of the set `C`. -TODO: align this API with `IsFaceOf` for cones. -/ +open Function Convexity + @[expose] public section namespace Convexity -open Function - -variable {R M M₁ M₂ : Type*} +variable {R M N : Type*} section Semiring -variable [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] -variable [ConvexSpace R M] +variable [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R M] [ConvexSpace R N] -/- NOTE: this is a copy of mathlib convexity API adapted to `ConvexSpace`. -/ variable (R) in -/-- Open segment in a convex space. Note that `openSegment 𝕜 x x = {x}` instead of being `∅` when -the base semiring has some element between `0` and `1`. -/ -def openSegment (x y : M) : Set M := - { z : M | ∃ (a b : R) (a0 : 0 < a) (b0 : 0 < b) (ab : a + b = 1), - convexCombPair a b a0.le b0.le ab x y = z } - -/- (x,y) = (y,x) -/ -theorem openSegment_symm (x y : M) : openSegment R x y = openSegment R y x := by - ext z - constructor - all_goals (intro h; rcases h with ⟨m, n, hm , hn , hmn , hz⟩; use n, m, hn, hm) - all_goals (rw [convexCombPair_symm] at hz; rw [add_comm] at hmn; use hmn) - -namespace ConvexSet - -/- NOTE: maybe this should be defined on `Set` instead of `ConvexSet`. -/ -/-- A subset `F` of a convex set `C` is a face of `C` iff it is an extreme subset. -/ -structure IsFaceOf (F C : ConvexSet R M) where - le : F ≤ C - left_mem_of_mem_openSegment : ∀ ⦃x⦄, x ∈ C → ∀ ⦃y⦄, y ∈ C → - ∀ ⦃z⦄, z ∈ F → z ∈ openSegment R x y → x ∈ F +/-- A subset `F` of a set `F` is a face of `C` iff it is an extreme convex subset. -/ +@[mk_iff] +structure IsFaceOf (F C : Set M) : Prop where + isConvexSet : IsConvexSet R F + le : F ⊆ C + left_mem_of_mem_Ioo {x y z : M} : x ∈ C → y ∈ C → + z ∈ F → z ∈ Ioo R x y → x ∈ F + +variable {C C₁ C₂ F F₁ F₂ : Set M} namespace IsFaceOf -theorem empty {C : ConvexSet R M} : IsFaceOf ∅ C where - le := SetLike.empty_le _ - left_mem_of_mem_openSegment := by simp - -/- A convex set is a face of itself. -/ -theorem refl (C : ConvexSet R M) : C.IsFaceOf C := - ⟨by simp , by intro x hx y hy z hz h; apply hx⟩ - -/- The face relation is transitive. -/ -theorem trans {C F₁ F₂ : ConvexSet R M} (h₁ : F₂.IsFaceOf F₁) (h₂ : F₁.IsFaceOf C) : - F₂.IsFaceOf C := by - constructor - · apply Set.Subset.trans h₁.1 h₂.1 - · intro x hx y hy z hz hhz - have hz' : z ∈ F₁.carrier := Set.mem_of_mem_of_subset hz h₁.1 - exact @h₁.2 x (@h₂.2 x hx y hy z hz' hhz) y (@h₂.2 y hy x hx z hz' (by simpa [openSegment_symm] - using hhz)) z hz hhz - -/- For two faces `F₁, F₂` of `C`, `F₁` is a face of `F₂` iff it is a subset of `F₂`. -/ -theorem iff_le_of_isFaceOf {C F₁ F₂ : ConvexSet R M} (h₁ : F₁.IsFaceOf C) (h₂ : F₂.IsFaceOf C) : - F₁.IsFaceOf F₂ ↔ F₁.carrier ⊆ F₂.carrier := by - constructor - · exact fun h => h.1 - · intro hh - constructor - · exact hh - · intro x hx y hy z hz hhz - exact h₁.2 (Set.mem_of_mem_of_subset hx h₂.1) (Set.mem_of_mem_of_subset hy h₂.1) hz hhz - -/- A convex set is a face of a face iff it is contained in the face and it is a face -of the ambient set. -/ -lemma isFaceOf_iff {F C : ConvexSet R M} (F₁ : ConvexSet R M) (H : F.IsFaceOf C) : - F₁.IsFaceOf F ↔ F₁.carrier ⊆ F.carrier ∧ F₁.IsFaceOf C:= by - apply Iff.intro - · exact fun h => ⟨h.1, trans h H⟩ - · intro h - constructor - · apply h.1 - · intro x hx y hy z hz hhz - exact @h.2.2 x (Set.mem_of_mem_of_subset hx H.1) y (Set.mem_of_mem_of_subset hy H.1) z hz hhz - -/- The intersection of two faces of two convex sets is a face of the intersection of the convex -sets. -/ -theorem inf {S₁ S₂ F₁ F₂ : ConvexSet R M} (h₁ : F₁.IsFaceOf S₁) (h₂ : F₂.IsFaceOf S₂) : - (F₁ ⊓ F₂).IsFaceOf (S₁ ⊓ S₂) := by - constructor - · intro x hx - exact ⟨Set.mem_of_mem_of_subset hx.1 h₁.1, Set.mem_of_mem_of_subset hx.2 h₂.1⟩ - · intro a ha b hb z hz hhz - exact ⟨@h₁.2 a ha.1 b hb.1 z hz.1 hhz, @h₂.2 a ha.2 b hb.2 z hz.2 hhz⟩ - -/- The intersection of two faces is a face. -/ -theorem inf_left {C F₁ F₂ : ConvexSet R M} (h₁ : F₁.IsFaceOf C) (h₂ : F₂.IsFaceOf C) : - (F₁ ⊓ F₂).IsFaceOf C := by - constructor - · exact le_trans inf_le_left h₁.le - · intro x hx y hy z hz hhz - exact ⟨@h₁.2 x hx y hy z hz.1 hhz, @h₂.2 x hx y hy z hz.2 hhz⟩ - -/- The face of two convex sets is a face of the intersection. -/ -theorem inf_right {S₁ S₂ F : ConvexSet R M} (h₁ : F.IsFaceOf S₁) (h₂ : F.IsFaceOf S₂) : - F.IsFaceOf (S₁ ⊓ S₂) := - ⟨Set.subset_inter h₁.1 h₂.1, by intro x hx y hy z hz hhz; exact @h₁.2 x hx.1 y hy.1 z hz hhz⟩ - -variable [ConvexSpace R M₁] -variable [ConvexSpace R M₂] +/-- A convex set `C` is a face of itself. -/ +@[refl, simp] +protected theorem refl {C : Set M} (h : IsConvexSet R C) : IsFaceOf R C C := + ⟨h, fun _ a ↦ a, fun hx _ _ _ ↦ hx⟩ + +protected theorem rfl {C : Set M} {h : IsConvexSet R C} : IsFaceOf R C C := .refl h + +/-- A face of a set is a face of another if and only if they are contained in each other. -/ +theorem isFaceOf_iff_le (h₁ : IsFaceOf R F₁ C) (h₂ : IsFaceOf R F₂ C) : + IsFaceOf R F₁ F₂ ↔ F₁ ⊆ F₂ := + ⟨IsFaceOf.le, fun h ↦ ⟨h₁.isConvexSet, h, fun hx hy hz hs↦ h₁.3 (h₂.le hx) (h₂.le hy) hz hs⟩⟩ + +/-- The empty set is a face of every set. -/ +protected theorem empty {C : Set M} : IsFaceOf R ∅ C := + ⟨IsConvexSet.empty, Set.empty_subset C, fun _ _ h _ ↦ h⟩ + +/-- The intersection of two faces of two sets is a face of the intersection of the sets. -/ +protected theorem inf (h₁ : IsFaceOf R F₁ C₁) (h₂ : IsFaceOf R F₂ C₂) : + IsFaceOf R (F₁ ∩ F₂) (C₁ ∩ C₂) where + isConvexSet := IsConvexSet.inter h₁.isConvexSet h₂.isConvexSet + le := le_inf_iff.mpr ⟨Set.inter_subset_left.trans h₁.le, Set.inter_subset_right.trans h₂.le⟩ + left_mem_of_mem_Ioo := by + simp only [Set.mem_inter_iff, and_imp] + refine fun xC₁ xC₂ yC₁ yC₂ zF₁ zF₂ hz ↦ ⟨?_, ?_⟩ + · exact h₁.left_mem_of_mem_Ioo xC₁ yC₁ zF₁ hz + · exact h₂.left_mem_of_mem_Ioo xC₂ yC₂ zF₂ hz + +/-- The intersection of two faces of a set is a face of the set. -/ +theorem inf_left (h₁ : IsFaceOf R F₁ C) (h₂ : IsFaceOf R F₂ C) : IsFaceOf R (F₁ ∩ F₂) C := + inf_idem C ▸ IsFaceOf.inf h₁ h₂ + +/-- If a set is a face of two sets simultaneously, then it's also a face of their intersection. -/ +theorem inf_right (h₁ : IsFaceOf R F C₁) (h₂ : IsFaceOf R F C₂) : IsFaceOf R F (C₁ ∩ C₂) := + inf_idem F ▸ IsFaceOf.inf h₁ h₂ + +protected theorem sInf (hc : IsConvexSet R C) {F : Set (Set M)} (h : ∀ f ∈ F, IsFaceOf R f C) : + IsFaceOf R (C ∩ sInf F) C where + isConvexSet := IsConvexSet.inter hc <| IsConvexSet.sInter (fun f hf ↦ (h f hf).isConvexSet) + le _ sm := sm.1 + left_mem_of_mem_Ioo := by + simp only [Set.sInf_eq_sInter, Set.mem_inter_iff, Set.mem_sInter, and_imp] + intro _ _ _ xc yc zc zf zs + simpa [xc] using fun f hf ↦ (h f hf).left_mem_of_mem_Ioo xc yc (zf f hf) zs + +protected theorem sInf' {F : Set (Set M)} (hne : F.Nonempty) (h : ∀ f ∈ F, IsFaceOf R f C) : + IsFaceOf R (sInf F) C where + isConvexSet := IsConvexSet.sInter (fun f hf ↦ (h f hf).isConvexSet) + le := by + obtain ⟨f, hf⟩ := hne + exact fun z hz ↦ (h f hf).le (Set.mem_sInter.mp hz f hf) + left_mem_of_mem_Ioo := by + intro x y z hx hy hz hseg + rw [Set.sInf_eq_sInter, Set.mem_sInter] at hz ⊢ + exact fun f hf ↦ (h f hf).left_mem_of_mem_Ioo hx hy (hz f hf) hseg + +/-- The face of a face of a set is also a face of the set. -/ +@[trans] +protected theorem trans (h₁ : IsFaceOf R F₂ F₁) (h₂ : IsFaceOf R F₁ C) : IsFaceOf R F₂ C := by + refine ⟨h₁.isConvexSet, h₁.le.trans h₂.le, ?_⟩ + intro x y z hx hy hz hhz + have hz' : z ∈ F₁ := h₁.le hz + exact h₁.3 (h₂.3 hx hy hz' hhz) + (h₂.3 hy hx hz' (by simpa [Ioo_symm, Ioo_symm] using hhz)) hz hhz + +section Map + +variable {C₁ F₁ : Set M} {C₂ F₂ : Set N} /- The image of a face under an injective affine map is a face of the image. -/ -theorem map {f : M₁ → M₂} {F C : ConvexSet R M₁} (hhf : IsAffineMap R f) (hf : Injective f) - (hF : F.IsFaceOf C) : (F.map hhf).IsFaceOf (C.map hhf) := by - constructor - · intro x hx - rcases hx with ⟨y , hy, rfl⟩ - exact Set.mem_image_of_mem _ (Set.mem_of_mem_of_subset hy hF.1) - · intro x hx y hy z hz hhz - rcases hx with ⟨m , hmC, rfl⟩ - rcases hy with ⟨n , hnC, rfl⟩ - rcases hz with ⟨l , hlF, rfl⟩ - have hl : l ∈ Convexity.openSegment R m n := by - rcases hhz with ⟨ a, b, ha, hb, hab, hcomb⟩ - have h : f (convexCombPair a b ha.le hb.le hab m n) = - convexCombPair a b ha.le hb.le hab (f m) (f n) := hhf.map_convexCombPair ha.le hb.le hab m n - have hh : f (convexCombPair a b ha.le hb.le hab m n) = f l := by - simpa [h] using hcomb - exact ⟨ a, b, ha, hb, hab, hf hh⟩ - exact Set.mem_image_of_mem _ (@hF.2 m hmC n hnC l hlF hl) +theorem map {φ : M → N} (hφ : IsAffineMap R φ) (hinj : Injective φ) + (hF : IsFaceOf R F₁ C₁) : IsFaceOf R (φ '' F₁) (φ '' C₁) where + isConvexSet := IsConvexSet.image hφ hF.isConvexSet + le := Set.image_mono hF.le + left_mem_of_mem_Ioo := by + rintro _ _ a ⟨x, hmC, rfl⟩ ⟨y, hnC, rfl⟩ ⟨z, hlF, rfl⟩ ⟨_, _, ha, hb, hab, hcomb⟩ + refine Set.mem_image_of_mem _ (hF.3 hmC hnC hlF ⟨_, _, ha, hb, hab, hinj ?_⟩) + simpa [hφ.map_convexCombPair] using hcomb /- The preimage of a face is a face of the preimage. -/ -theorem comap_face {f : M₁ → M₂} {F C : ConvexSet R M₂} (hf : IsAffineMap R f) (hF : F.IsFaceOf C) : - (F.comap hf).IsFaceOf (C.comap hf) := by - constructor - · apply Set.preimage_mono hF.1 - · have hF1 := hF.2 - intro x hx y hy z hz hhz - have hhz' : f z ∈ Convexity.openSegment R (f x) (f y) := by - rcases hhz with ⟨ a, b, ha, hb, hab, hcomb⟩ - have hff : f (convexCombPair a b ha.le hb.le hab x y) = - convexCombPair a b ha.le hb.le hab (f x) (f y) := hf.map_convexCombPair ha.le hb.le hab x y - rw [hcomb] at hff - use a, b, ha, hb, hab, hff.symm - specialize @hF1 (f x) (Set.mem_preimage.mp hx ) (f y) (Set.mem_preimage.mp hy) (f z) ( - Set.mem_preimage.mp hz) hhz' - apply Set.mem_preimage.mp hF1 +theorem preimage {φ : M → N} (hφ : IsAffineMap R φ) (hF : IsFaceOf R F₂ C₂) : + IsFaceOf R (φ ⁻¹' F₂) (φ ⁻¹' C₂) where + isConvexSet := IsConvexSet.preimage hφ hF.isConvexSet + le := Set.preimage_mono hF.le + left_mem_of_mem_Ioo := by + rintro x y z hx hy hz ⟨a, b, ha, hb, hab, hcomb⟩ + refine hF.3 hx hy hz ⟨a, b, ha, hb, hab, ?_⟩ + exact hcomb ▸ (hφ.map_convexCombPair ha.le hb.le hab x y).symm + +theorem of_map_injective {φ : M → N} (hφ : IsAffineMap R φ) (hinj : Injective φ) + (hF : IsFaceOf R (φ '' F₁) (φ '' C₁)) : IsFaceOf R F₁ C₁ := by + have h' := IsFaceOf.preimage hφ hF + rwa [Set.preimage_image_eq _ hinj, Set.preimage_image_eq _ hinj] at h' + +theorem of_preimage_surjective {φ : M → N} (hφ : IsAffineMap R φ) (hsurj : Function.Surjective φ) + (hc : IsFaceOf R (φ ⁻¹' F₂) (φ ⁻¹' C₂)) : IsFaceOf R F₂ C₂ := by + have hcv := IsConvexSet.image hφ hc.isConvexSet + rw [Set.image_preimage_eq _ hsurj] at hcv + refine ⟨hcv, fun x xF ↦ ?_, fun {x y z} xC yC zF h ↦ ?_⟩ + · rw [← (hsurj x).choose_spec] at xF ⊢ + exact Set.mem_preimage.mp (hc.le xF) + · rw [← (hsurj x).choose_spec] at h ⊢ xC + rw [← (hsurj y).choose_spec] at h yC + rw [← hφ.image_Ioo] at h + obtain ⟨a, b, rfl⟩ := h + exact hc.left_mem_of_mem_Ioo xC yC zF b + +end Map + +end IsFaceOf /- `F` is a face of `C` iff the image of `F` is a face of the image of `C` under an injective affine map -/ -theorem isFaceOf_map_iff {f : M₁ → M₂} {F C : ConvexSet R M₁} (hhf : IsAffineMap R f) - (hf : Injective f) : (F.map hhf).IsFaceOf (C.map hhf) ↔ F.IsFaceOf C := by - constructor - · intro h - have hh := comap_face hhf h - have h (A : ConvexSet R M₁) : (A.map hhf).comap hhf = A := by - ext z - constructor - · intro hz - rcases hz with ⟨y, hy, hzy⟩ - rw [hf hzy] at hy - use hy - · intro hz - exact ⟨z, hz, rfl⟩ - rw [h F, h C] at hh - exact hh - · intro h - apply map hhf hf h +theorem isFaceOf_map_iff {φ : M → N} (hφ : IsAffineMap R φ) (hinj : Injective φ) : + IsFaceOf R (φ '' F₁) (φ '' C₁) ↔ IsFaceOf R F₁ C₁ := + ⟨IsFaceOf.of_map_injective hφ hinj, IsFaceOf.map hφ hinj⟩ -end IsFaceOf +variable {C₂ F₂ : Set N} in +/-- The preimage of a set `F` under a surjective affine map is a face of the +preimage of another set `F` if and only if `F` is a face of `C`. -/ +theorem isFaceOf_preimage_iff {φ : M → N} (hφ : IsAffineMap R φ) (hsurj : Function.Surjective φ) : + IsFaceOf R (φ ⁻¹' F₂) (φ ⁻¹' C₂) ↔ IsFaceOf R F₂ C₂ := + ⟨IsFaceOf.of_preimage_surjective hφ hsurj, IsFaceOf.preimage hφ⟩ + +namespace IsFaceOf + +section Prod + +/-- The product of two faces of two sets is a face of the product of the sets. -/ +protected theorem prod {C₁ F₁ : Set M} {C₂ F₂ : Set N} + (hF₁ : IsFaceOf R F₁ C₁) (hF₂ : IsFaceOf R F₂ C₂) : IsFaceOf R (F₁ ×ˢ F₂) (C₁ ×ˢ C₂) where + isConvexSet := IsConvexSet.prod hF₁.isConvexSet hF₂.isConvexSet + le := fun x hx ↦ by simpa [Set.mem_prod] using ⟨hF₁.le hx.1, hF₂.le hx.2⟩ + left_mem_of_mem_Ioo := by + simp only [Set.mem_prod, and_imp, Prod.forall] + intro _ _ _ _ _ _ xC₁ xC₂ yC₁ yC₂ ha hb hs + have := Prod.Ioo_subset R _ _ hs + exact ⟨hF₁.3 xC₁ yC₁ ha this.1, hF₂.3 xC₂ yC₂ hb this.2⟩ + +/-- The projection of a face of a product set onto the first component is a face of the +projection of the product set onto the first component. -/ +protected theorem fst {C₁ : Set M} {C₂ : Set N} {F : Set (M × N)} + (hF : IsFaceOf R F (C₁ ×ˢ C₂)) : IsFaceOf R (Prod.fst '' F) C₁ where + isConvexSet := IsConvexSet.image Prod.isAffineMap_fst hF.isConvexSet + le := by + intro x hx + simp only [Set.mem_image, Prod.exists, exists_and_right, exists_eq_right] at hx + exact (Set.mem_prod.mp <| hF.le hx.choose_spec).1 + left_mem_of_mem_Ioo := by + simp only [Set.mem_image, Prod.exists, exists_and_right, exists_eq_right, forall_exists_index] + intro x y a hx hy ha z h + refine ⟨ha, hF.left_mem_of_mem_Ioo (x := (x, ha)) (y := (y, ha)) (z := (a, ha)) ?_ ?_ z ?_⟩ + · exact Set.mem_prod.mp ⟨hx, (hF.le z).2⟩ + · exact Set.mem_prod.mp ⟨hy, (hF.le z).2⟩ + · rw [← Prod.image_mk_Ioo_left R x y ha] + simpa + +/-- The projection of a face of a product set onto the second component is a face of the +projection of the product set onto the second component. -/ +protected theorem snd {C₁ : Set M} {C₂ : Set N} {F : Set (M × N)} + (hF : IsFaceOf R F (C₁ ×ˢ C₂)) : IsFaceOf R (Prod.snd '' F) C₂ := by + have := hF.map (φ := Prod.swap) ((Prod.isAffineMap_snd).prodMk (Prod.isAffineMap_fst)) + Prod.swap_injective + convert IsFaceOf.fst (by simpa) + simp [Set.image_image] + +end Prod -end ConvexSet +end IsFaceOf end Semiring diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Homogenization.lean index a128565b..c657f9c2 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Homogenization.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Homogenization.lean @@ -15,7 +15,7 @@ public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Homogenization namespace Affine.IsHomogenization -open Set Convexity ConvexSet Submodule +open Set Convexity IsConvexSet Submodule variable {R V A W : Type*} @@ -33,10 +33,10 @@ variable (ℋ : Affine.IsHomogenization R A W) variable {ℋ} in /-- If the homogenization of a point `q` is a positive combination of the homogenization of two other points, then `q` lies in the open segment between them. -/ -theorem pos_combo_openSegment {r₁ r₂ t : R} {p₁ p₂ q : A} +theorem pos_combo_Ioo {r₁ r₂ t : R} {p₁ p₂ q : A} (h₁ : 0 < r₁) (h₂ : 0 < r₂) (hₜ : 0 < t) (h : r₁ • ℋ.ofPoint p₁ + r₂ • ℋ.ofPoint p₂ = t • ℋ.ofPoint q) : - q ∈ Convexity.openSegment R p₁ p₂ := by + q ∈ Convexity.Ioo R p₁ p₂ := by have : r₁ + r₂ = t := by simpa [ℋ.weight_ofPoint, map_add, map_smul] using congr_arg ℋ.weight h have : t⁻¹ • r₁ + t⁻¹ • r₂ = 1 := by simp_rw [← smul_add, smul_eq_mul, this, mul_comm, Field.mul_inv_cancel _ hₜ.ne.symm] @@ -48,40 +48,41 @@ theorem pos_combo_openSegment {r₁ r₂ t : R} {p₁ p₂ q : A} /-- If `F` is a face of `P`, then the homogenization of `F` is a face of the homogenization of `P`. -/ -theorem homogenize_isFaceOf {F P : ConvexSet R A} (he : F.IsFaceOf P) : - (F.homogenize ℋ).IsFaceOf (P.homogenize ℋ) where - le := (homogenizeOrderHom ℋ).monotone' he.le +theorem homogenize_isFaceOf {F P : Set A} (hP : IsConvexSet R P) + (hF : IsFaceOf R F P) : (homogenize ℋ F).IsFaceOf (homogenize ℋ P) where + le := (homogenizeOrderHom ℋ).monotone' hF.le mem_of_smul_add_mem := by intro v w a hv hw ha hvw have hhom := homogenize_salient ℋ P by_cases hnf : (F : Set A).Nonempty - · have cF := F.isConvexSet.image ℋ.ofPoint.isAffineMap + · have cF := hF.isConvexSet.image ℋ.ofPoint.isAffineMap apply (Set.ext_iff.mp (PointedCone.hull_eq_smul (hnf.image _) cF) _).mpr by_cases hv0 : v = 0 · exact ⟨0, le_rfl, mem_smul_set.mpr (by simpa [hv0] using nonempty_def.mp hnf)⟩ · by_cases hw0 : w = 0 · subst hw0 - obtain ⟨r, hr, r', ⟨w, hw, _⟩, hra⟩ := - smul_pos_of_mem_homogenize hvw (by simpa using smul_ne_zero ha.ne.symm hv0) + obtain ⟨r, hr, r', ⟨w, hw, _⟩, hra⟩ := smul_pos_of_mem_homogenize hF.isConvexSet hvw + (by simpa using smul_ne_zero ha.ne.symm hv0) simp only [add_zero] at ⊢ hra use a⁻¹ • r, (smul_pos (inv_pos.mpr ha) hr).le, r' constructor · use w, hw simp only rw [smul_assoc, hra, ← smul_assoc, smul_eq_mul, inv_mul_cancel₀ ha.ne.symm, one_smul] - · obtain ⟨rw, rw0, q, ⟨q', qq, rfl⟩, _, _⟩ := smul_pos_of_mem_homogenize hw hw0 - obtain ⟨rv, rv0, _, ⟨p', pp, rfl⟩, _, _⟩ := smul_pos_of_mem_homogenize hv hv0 + · obtain ⟨rw, rw0, q, ⟨q', qq, rfl⟩, _, _⟩ := smul_pos_of_mem_homogenize hP hw hw0 + obtain ⟨rv, rv0, _, ⟨p', pp, rfl⟩, _, _⟩ := smul_pos_of_mem_homogenize hP hv hv0 have : a • (rv • ℋ.ofPoint p') + (rw • ℋ.ofPoint q') ≠ 0 := by intro hc exact (smul_ne_zero rw0.ne.symm (ℋ.ofPoint_ne_zero q')) <| hhom _ hw _ (PointedCone.smul_mem _ ha.le hv) (by simpa [add_comm] using hc) - obtain ⟨_, rvw0, _, ⟨_, qqp, rfl⟩, pdp⟩ := smul_pos_of_mem_homogenize hvw this - have := he.left_mem_of_mem_openSegment pp qq qqp ?_ + obtain ⟨_, rvw0, _, ⟨_, qqp, rfl⟩, pdp⟩ := + smul_pos_of_mem_homogenize hF.isConvexSet hvw this + have := hF.left_mem_of_mem_Ioo pp qq qqp ?_ · refine ⟨rv, rv0.le, smul_mem_smul_set <| mem_image_of_mem ℋ.ofPoint this⟩ rw [← smul_assoc _ rv] at pdp - exact pos_combo_openSegment (smul_pos ha rv0) rw0 rvw0 pdp.symm + exact pos_combo_Ioo (smul_pos ha rv0) rw0 rvw0 pdp.symm · have := not_nonempty_iff_eq_empty.mp hnf - simp_all only [homogenize, SetLike.coe, image_empty, span_empty, mem_bot] + simp_all only [homogenize, image_empty, span_empty, mem_bot] by_contra hxx have : -v = a⁻¹ • w := by simp [← neg_eq_of_add_eq_zero_right hvw, smul_neg, smul_smul, inv_mul_cancel₀ (ne_of_gt ha)] @@ -93,10 +94,11 @@ theorem homogenize_isFaceOf {F P : ConvexSet R A} (he : F.IsFaceOf P) : /-- If `F` is a face of `C`, then the dehomogenization of `F` is a face of the dehomogenization of `C`. -/ theorem dehomogenize_isFaceOf {F C : PointedCone R W} (hf : F.IsFaceOf C) : - (ConvexSet.dehomogenize ℋ F).IsFaceOf (ConvexSet.dehomogenize ℋ C) where + IsFaceOf R (dehomogenize ℋ F) (dehomogenize ℋ C) where + isConvexSet := dehomogenize_isConvexSet ℋ F le := preimage_mono (fun _ x ↦ hf.le x) - left_mem_of_mem_openSegment := by - rintro x hx y hy z hz ⟨a, b, ha, hb, hab, hzo⟩ + left_mem_of_mem_Ioo := by + rintro x y z hx hy hz ⟨a, b, ha, hb, hab, hzo⟩ refine hf.mem_of_smul_add_mem hx (C.smul_mem hb.le hy) ha ?_ rwa [← convexCombPair_eq_sum _ _ ha.le hb.le hab, ← ℋ.ofPoint.isAffineMap.map_convexCombPair, hzo] @@ -107,17 +109,19 @@ its homogenization cone. This isomorphism is used to translate results between face lattices of cones and face lattices of convex sets. -/ -def _root_.ConvexSet.face_homogenizeIso (P : ConvexSet R A) : - Face P ≃o PointedCone.Face (P.homogenize ℋ) where - toFun F := ⟨_, ℋ.homogenize_isFaceOf F.isFaceOf⟩ +def _root_.Convexity.face_homogenizeIso {P : Set A} (hP : IsConvexSet R P) : + Face hP ≃o PointedCone.Face (homogenize ℋ P) where + toFun F := ⟨_, ℋ.homogenize_isFaceOf hP F.isFaceOf⟩ invFun F := ⟨dehomogenize ℋ F.toSubmodule, - by simpa [dehomogenize_homogenize ℋ] using dehomogenize_isFaceOf ℋ F.isFaceOf⟩ + by simpa [dehomogenize_homogenize ℋ hP] using dehomogenize_isFaceOf ℋ F.isFaceOf⟩ map_rel_iff' := by intro a b refine ⟨fun h x xm ↦ ?_, fun h _ xm ↦ span_mono (image_mono h) xm⟩ - refine (ofPoint_mem_homogenize_iff_mem _ x b.toConvexSet).mp (h ?_) - exact (ofPoint_mem_homogenize_iff_mem _ x a.toConvexSet).mpr xm - left_inv _ := by simp [dehomogenize_homogenize] + refine (ofPoint_mem_homogenize_iff_mem _ x b.isFaceOf.isConvexSet).mp (h ?_) + exact (ofPoint_mem_homogenize_iff_mem _ x a.isFaceOf.isConvexSet).mpr xm + left_inv F := by + simp only [Face.carrier_eq_coe, Face.ext_iff] + exact dehomogenize_homogenize ℋ F.isFaceOf.isConvexSet right_inv F := by have := homogenize_dehomogenize_of_le_positive (fun _ h n ↦ weight_pos_of_mem_homogenize (F.isFaceOf.le h) n) diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Lattice.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Lattice.lean index 5b3d6acc..a08a5f34 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Lattice.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Lattice.lean @@ -6,8 +6,10 @@ Authors: Olivia Röhrig, Mara Gruß, Valentina Taylor Cerra, Martin Winter module public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Face.Basic +public import Polyhedral.Mathlib.Geometry.Convex.Set +import Polyhedral.Mathlib.Data.SetLike.IsConcrete -import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Lattice +-- import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Lattice /-! This file defines faces of convex sets. @@ -25,35 +27,31 @@ section Semiring variable [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] variable [ConvexSpace R M] -namespace ConvexSet +namespace IsConvexSet -/- NOTE: maybe this should be defined on `Set` instead of `ConvexSet`. -/ /-- A face of a convex set `P`. Represents the face lattice of `P`. -/ -structure Face (P : ConvexSet R M) extends toConvexSet : ConvexSet R M where - isFaceOf : IsFaceOf toConvexSet P +@[ext] +structure Face {p : Set M} (P : IsConvexSet R p) where + carrier : Set M + isFaceOf : IsFaceOf R carrier p -attribute [coe] Face.toConvexSet +attribute [coe] Face.carrier namespace Face -variable {P : ConvexSet R M} +variable {p : Set M} {P : IsConvexSet R p} instance : SetLike (Face P) M where - coe F := F.toConvexSet.carrier + coe F := F.carrier coe_injective a b h := by - cases a; cases b; congr; exact SetLike.coe_injective h + cases a; cases b; congr -instance : CoeOut (Face P) (ConvexSet R M) := ⟨toConvexSet⟩ +instance : CoeOut (Face P) (Set M) := ⟨carrier⟩ @[simp] theorem carrier_eq_coe {F : Face P} : F.carrier = F := by rfl @[simp] theorem mem_coe {F : Face P} (x : M) : x ∈ F.carrier ↔ x ∈ F := .rfl -@[ext] theorem ext {F₁ F₂ : Face P} (h : ∀ x, x ∈ F₁ ↔ x ∈ F₂) : F₁ = F₂ := SetLike.ext h - -@[simp] theorem coe_eq_toConvexSet_coe {F : Face P} : (F : Set M) = F.toConvexSet := - SetLike.ext'_iff.mp rfl - @[simp] theorem mem_mk {s h x} : x ∈ (⟨s, h⟩ : Face P) ↔ x ∈ s := .rfl @[simp] theorem mk_eq {s h} : (⟨s, h⟩ : Face P) = s := by ext; simp @@ -69,49 +67,24 @@ lemma nonempty_of_ne_bot {F : Face P} (h : F ≠ ⊥) : (F : Set M).Nonempty := intro heq apply h ext - simp [← SetLike.mem_coe, heq, Bot.bot] + simp [heq, Bot.bot] instance : OrderTop (Face P) where - top := ⟨P, IsFaceOf.refl P⟩ + top := ⟨_, IsFaceOf.refl P⟩ le_top F := F.isFaceOf.le instance : Inhabited (Face P) := ⟨⊤⟩ -theorem toConvexSet_le {F : Face P} : F ≤ P := F.isFaceOf.le - -@[simp] -theorem toConvexSet_le_toConvexSet {F₁ F₂ : Face P} : - F₁.toConvexSet ≤ F₂.toConvexSet ↔ F₁ ≤ F₂ := .rfl - -@[simp] -theorem toConvexSet_lt_toConvexSet {F₁ F₂ : Face P} : - F₁.toConvexSet < F₂.toConvexSet ↔ F₁ < F₂ := .rfl - -@[simp] -theorem mem_toConvexSet {F : Face P} (x : M) : x ∈ F.toConvexSet ↔ x ∈ F := .rfl - -@[simp] theorem toConvexSet_bot : ((⊥ : Face P) : ConvexSet R M) = ∅ := rfl - -@[simp] theorem toConvexSet_top : ((⊤ : Face P) : ConvexSet R M) = P := rfl - /-! ### Infimum, supremum and lattice -/ -/-- The infimum of two faces `F₁`, `F₂` of `C` is the intersection of the cones `F₁` and `F₂`. -/ +/-- The infimum of two faces `F₁`, `F₂` of `P` is the intersection of `F₁` and `F₂`. -/ instance : Min (Face P) where - min F₁ F₂ := ⟨F₁ ⊓ F₂, F₁.isFaceOf.inf_left F₂.isFaceOf⟩ - -protected theorem IsFaceOf.sInf (F : Set (ConvexSet R M)) (h : ∀ f ∈ F, f.IsFaceOf P) : - (P ⊓ sInf F).IsFaceOf P where - le _ sm := sm.1 - left_mem_of_mem_openSegment := by - simp only [SetLike.mem_min, SetLike.mem_sInf, and_imp] - intro x hx y hy z hz h₁ h₂ - simpa [hx] using fun F Fs ↦ (h F Fs).left_mem_of_mem_openSegment hx hy (by grind) h₂ + min F₁ F₂ := ⟨_, F₁.isFaceOf.inf_left F₂.isFaceOf⟩ instance : InfSet (Face P) where sInf S := - { toConvexSet := P ⊓ sInf {s.1 | s ∈ S} - isFaceOf := IsFaceOf.sInf _ (fun _ ⟨s, _, hs2⟩ ↦ hs2 ▸ s.isFaceOf) } + { carrier := p ∩ sInf {s.1 | s ∈ S} + isFaceOf := IsFaceOf.sInf P (fun _ hf ↦ hf.choose_spec.2 ▸ hf.choose.isFaceOf) } instance : SemilatticeInf (Face P) where inf := min @@ -123,19 +96,20 @@ instance : CompleteSemilatticeInf (Face P) where __ := instSemilatticeInf isGLB_sInf S := by constructor <;> intro f fS - · rw [← toConvexSet_le_toConvexSet] - refine inf_le_of_right_le ?_ - simpa [LE.le] using fun _ xs ↦ xs f fS - · simp only [sInf, Set.sInter_image, Set.mem_ofPred_eq, - Set.iInter_exists, Set.biInter_and', Set.iInter_iInter_eq_right] - simpa [LE.le] using fun x a ↦ ⟨f.2.1 a, fun i hi ↦ (mem_coe x).mp (fS hi a)⟩ + · rintro _ ⟨_, hz⟩ + simp only [carrier_eq_coe, Set.sInf_eq_sInter, Set.mem_sInter, Set.mem_ofPred_eq, + forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, SetLike.mem_coe] at hz + exact hz _ fS + · simp only [sInf, carrier_eq_coe, Set.mem_ofPred_eq, forall_exists_index, and_imp, + forall_apply_eq_imp_iff₂, SetLike.mem_coe] + simpa [LE.le] using fun x a ↦ ⟨f.isFaceOf.le a, fun i hi ↦ (mem_coe x).mp (fS hi a)⟩ instance : CompleteLattice (Face P) where - top := ⟨P, .refl _⟩ - le_top _ := toConvexSet_le + top := ⟨_, .refl P⟩ + le_top f := f.isFaceOf.le __ := completeLatticeOfCompleteSemilatticeInf _ -end ConvexSet.Face +end IsConvexSet.Face end Semiring diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean index 2504afbb..aa4bfb4d 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean @@ -15,7 +15,7 @@ public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.IsHomo open Convexity Pointwise Set PointedCone Submodule -namespace Convexity.ConvexSet +namespace Convexity variable {R V A W : Type*} @@ -26,66 +26,65 @@ open Convexity variable [Ring R] [PartialOrder R] [IsStrictOrderedRing R] variable [AddCommGroup V] [Module R V] variable [AddCommGroup W] [Module R W] -variable [AddTorsor V A] [ConvexSpace R A] +variable [AddTorsor V A] variable (ℋ : Affine.IsHomogenization R A W) /-- The homogenization cone of a convex set in an affine space. -/ -def homogenize (P : ConvexSet R A) : PointedCone R W := hull R (ℋ.ofPoint '' P) +def homogenize (P : Set A) : PointedCone R W := hull R (ℋ.ofPoint '' P) -lemma homogenize_mono {K₁ K₂ : ConvexSet R A} (h : K₁ ≤ K₂) : - K₁.homogenize ℋ ≤ K₂.homogenize ℋ := Submodule.span_mono <| Set.image_mono h +lemma homogenize_mono {K₁ K₂ : Set A} (h : K₁ ≤ K₂) : + homogenize ℋ K₁ ≤ homogenize ℋ K₂ := Submodule.span_mono <| Set.image_mono h -lemma homogenize_monotone : Monotone (homogenize ℋ : ConvexSet R A → PointedCone R W) := +lemma homogenize_monotone : Monotone (homogenize ℋ : Set A → PointedCone R W) := fun _ _ => homogenize_mono _ /-- Homogenization from convex set to convex cones as an order homomorphism. -/ -def homogenizeOrderHom : ConvexSet R A →o PointedCone R W where +def homogenizeOrderHom : Set A →o PointedCone R W where toFun := homogenize ℋ monotone' := homogenize_monotone _ -lemma homogenize_singleton (p : A) : homogenize ℋ ({p} : ConvexSet R A) = R ∙₊ ℋ.ofPoint p := by - have h : (({p} : ConvexSet R A) : Set A) = {p} := rfl - rw [homogenize, h, Set.image_singleton] +lemma homogenize_singleton (p : A) : homogenize ℋ {p} = R ∙₊ ℋ.ofPoint p := by + rw [homogenize, Set.image_singleton] @[simp] -lemma homogenize_bot : homogenize ℋ (⊥ : ConvexSet R A) = ⊥ := by - simp [homogenize, Bot.bot] +lemma homogenize_bot : homogenize ℋ ∅ = ⊥ := by + simp [homogenize] @[simp] -lemma homogenize_eq_bot_iff (P : ConvexSet R A) : homogenize ℋ P = ⊥ ↔ P = ⊥ := by - refine ⟨fun h ↦ ?_, by simp +contextual [-SetLike.bot_eq_empty]⟩ +lemma homogenize_eq_bot_iff (P : Set A) : homogenize ℋ P = ⊥ ↔ P = ∅ := by + refine ⟨fun h ↦ ?_, by simp +contextual [homogenize]⟩ ext x - simp only [homogenize, span_eq_bot, mem_image, SetLike.mem_coe, forall_exists_index, and_imp, + simp only [homogenize, span_eq_bot, mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at h simpa using fun hx ↦ ℋ.ofPoint_ne_zero _ (h x hx) -/- NOTE: `homogenize_top`, stating `homogenize ℋ (⊤ : ConvexSet R A) = ℋ.weight.positive`, +/- NOTE: `homogenize_top`, stating `homogenize ℋ (⊤ : Set A) = ℋ.weight.positive`, only holds over linearly ordered fields and is proven in the `Field` section below. Over a general ordered ring it fails: for `R = ℤ[ε]` with `ε` a positive infinitesimal, the point `(1, ε)` lies in `weight.positive` but not in the cone hull of the weight-one hyperplane, since all nonnegative coefficients bounded by `ε` lie in the ideal `(ε)`. -/ -lemma homogenize_le_weight_positive (K : ConvexSet R A) : +lemma homogenize_le_weight_positive (K : Set A) : homogenize ℋ K ≤ ℋ.weight.positive := by exact LinearMap.hull_le_positive_of_subset_preimage_singleton one_pos fun _ ↦ by rintro ⟨x, -, rfl⟩ simp [ℋ.weight_ofPoint] variable {ℋ} in -lemma weight_pos_of_mem_homogenize {x} {P : ConvexSet R A} (h : x ∈ homogenize ℋ P) (hx : x ≠ 0) : +lemma weight_pos_of_mem_homogenize {x} {P : Set A} (h : x ∈ homogenize ℋ P) (hx : x ≠ 0) : 0 < ℋ.weight x := homogenize_le_weight_positive _ P h hx variable {ℋ} in -lemma weight_nonneg_of_mem_homogenize {x : W} {P : ConvexSet R A} (h : x ∈ homogenize ℋ P) : +lemma weight_nonneg_of_mem_homogenize {x : W} {P : Set A} (h : x ∈ homogenize ℋ P) : 0 ≤ ℋ.weight x := (LinearMap.mem_positive'.mp (homogenize_le_weight_positive _ P h)).1 -lemma homogenize_salient (K : ConvexSet R A) : PointedCone.Salient (homogenize ℋ K) := +lemma homogenize_salient (K : Set A) : PointedCone.Salient (homogenize ℋ K) := Salient.of_le_salient ℋ.weight.positive_salient (homogenize_le_weight_positive _ K) variable {ℋ} in -theorem homogenize_fg_ofPoint_range {C : ConvexSet R A} (h : (homogenize ℋ C).FG) : +theorem homogenize_fg_ofPoint_range {C : Set A} (h : (homogenize ℋ C).FG) : ∃ g : Finset W, PointedCone.hull R g = homogenize ℋ C ∧ (g : Set W) ⊆ Set.range ℋ.ofPoint := by obtain ⟨g, hg⟩ := h @@ -108,32 +107,30 @@ theorem homogenize_fg_ofPoint_range {C : ConvexSet R A} (h : (homogenize ℋ C). section Module -variable [ConvexSpace R W] [IsModuleConvexSpace R W] [IsAffineConvexSpace R V A] -def dehomogenize (C : PointedCone R W) : ConvexSet R A := - ⟨_, C.isConvexSet.preimage ℋ.ofPoint.isAffineMap⟩ +def dehomogenize (C : PointedCone R W) : Set A := ℋ.ofPoint ⁻¹' C -alias _root_.PointedCone.dehomogenize := dehomogenize +-- alias _root_.PointedCone.dehomogenize := dehomogenize @[simp] -lemma dehomogenize_bot : dehomogenize ℋ (⊥ : PointedCone R W) = ⊥ := by +lemma dehomogenize_bot : dehomogenize ℋ (⊥ : PointedCone R W) = ∅ := by ext simp [dehomogenize, Affine.IsHomogenization.ofPoint_ne_zero] @[simp] -lemma dehomogenize_top : dehomogenize ℋ (⊤ : PointedCone R W) = ⊤ := by +lemma dehomogenize_top : dehomogenize ℋ (⊤ : PointedCone R W) = univ := by ext - simp [dehomogenize, SetLike.mem_coe.mp] + simp [dehomogenize] @[simp] -lemma dehomogenize_weight_positive : dehomogenize ℋ ℋ.weight.positive = ⊤ := - SetLike.eq_top_of_forall fun _ ↦ LinearMap.mem_positive'.mpr (by simp [ℋ.weight_ofPoint]) +lemma dehomogenize_weight_positive : dehomogenize ℋ ℋ.weight.positive = ⊤ := by + simp [dehomogenize, LinearMap.positive] lemma dehomogenize_mono {C₁ C₂ : PointedCone R W} (h : C₁ ≤ C₂) : dehomogenize ℋ C₁ ≤ dehomogenize ℋ C₂ := Set.preimage_mono <| Set.preimage_mono h -- Q: why Set.preimage_mono twice? -lemma dehomogenize_monotone : Monotone (dehomogenize ℋ : PointedCone R W → ConvexSet R A) := +lemma dehomogenize_monotone : Monotone (dehomogenize ℋ) := fun _ _ => dehomogenize_mono _ -- This lemma is just `Set.image_preimage_eq_inter_range` in disguise. It is likely not needed. @@ -148,11 +145,37 @@ lemma ofPoint_dehomogenize_eq_inter_ofPoint (C : PointedCone R W) : use y simpa +/-- The dehomogenization of the ray spanned by an embedded point is the singleton of that +point. -/ +@[simp] +lemma dehomogenize_hull_singleton_ofPoint (p : A) : dehomogenize ℋ (R ∙₊ ℋ.ofPoint p) = {p} := by + ext q + constructor + · intro hq + simp only [dehomogenize, mem_preimage, SetLike.mem_coe, mem_span_singleton, Subtype.exists, + Nonneg.mk_smul] at hq + obtain ⟨a, -, ha⟩ := hq + have hw := congrArg ℋ.weight ha + simp only [map_smul, ℋ.weight_ofPoint, smul_eq_mul, mul_one] at hw + rw [hw, one_smul] at ha + exact ℋ.ofPoint_injective ha ▸ rfl + · rintro rfl + simp [Convexity.dehomogenize] + +section + +variable [ConvexSpace R A] [ConvexSpace R W] [IsModuleConvexSpace R W] [IsAffineConvexSpace R V A] + +lemma dehomogenize_isConvexSet (C : PointedCone R W) : IsConvexSet R (dehomogenize ℋ C) := + C.isConvexSet.preimage ℋ.ofPoint.isAffineMap + /-- 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 (ℋ.ofPoint '' s) = homogenize ℋ (ConvexSet.convexHull R s) := by - simp [homogenize, ConvexSet.convexHull, ℋ.ofPoint.isAffineMap.image_convexHull] + hull R (ℋ.ofPoint '' s) = homogenize ℋ (convexHull R s) := by + simp [homogenize, ℋ.ofPoint.isAffineMap.image_convexHull] + +end end Module @@ -163,32 +186,35 @@ section Field variable [Field R] [LinearOrder R] [IsOrderedRing R] variable [AddCommGroup V] [Module R V] variable [AddCommGroup W] [Module R W] -variable [AddTorsor V A] [ConvexSpace R A] +variable [AddTorsor V A] variable (ℋ : Affine.IsHomogenization R A W) /-- The homogenization of the full affine space is the positive cone of the weight functional. -/ -lemma homogenize_top : homogenize ℋ (⊤ : ConvexSet R A) = ℋ.weight.positive := by +lemma homogenize_top : homogenize ℋ (univ : Set A) = ℋ.weight.positive := by have : ℋ.weight ⁻¹' {1} = AffineSubspace.comap ℋ.weight.toAffineMap {1} := rfl rw [homogenize, LinearMap.positive_eq_hull_preimage_singleton ℋ.weight one_pos, this, ← ℋ.ofPoint_range_eq_comap_weight_one] congr! with x simp -variable [ConvexSpace R W] [IsModuleConvexSpace R W] [IsAffineConvexSpace R V A] +section + +variable [ConvexSpace R A] [ConvexSpace R W] [IsModuleConvexSpace R W] [IsAffineConvexSpace R V A] variable {ℋ} in -lemma smul_pos_of_mem_homogenize {P : ConvexSet R A} {x} (h : x ∈ homogenize ℋ P) (hx : x ≠ 0) : +lemma smul_pos_of_mem_homogenize {P : Set A} (hP : IsConvexSet R P) {x} (h : x ∈ homogenize ℋ P) + (hx : x ≠ 0) : x ∈ Set.Ioi (0 : R) • ℋ.ofPoint '' (P : Set A) := (mem_hull_iff_mem_pos_smul_of_convex_nonzero - (P.isConvexSet.image ℋ.ofPoint.isAffineMap) hx).mp h + (hP.image ℋ.ofPoint.isAffineMap) hx).mp h -- TODO: This lemma should be proven for general sets (homogenizing to SubMulAction) and then -- applied here as a special case. -lemma ofPoint_mem_homogenize_iff_mem (x : A) (P : ConvexSet R A) : +lemma ofPoint_mem_homogenize_iff_mem (x : A) {P : Set A} (hP : IsConvexSet R P) : ℋ.ofPoint x ∈ homogenize ℋ P ↔ x ∈ P := by refine ⟨fun h ↦ ?_, fun h ↦ mem_span_of_mem (Set.mem_image_of_mem ℋ.ofPoint h)⟩ - obtain ⟨_, _, h'⟩ := smul_pos_of_mem_homogenize (Set.mem_preimage.mpr h) (ℋ.ofPoint_ne_zero x) + obtain ⟨_, _, h'⟩ := smul_pos_of_mem_homogenize hP (Set.mem_preimage.mpr h) (ℋ.ofPoint_ne_zero x) obtain ⟨_, ⟨_, _, hyy'⟩, hy'⟩ := Set.mem_smul_set.mp h' have := congrArg ℋ.weight hy' simp [← hyy', ℋ.weight_ofPoint] at this @@ -197,14 +223,14 @@ lemma ofPoint_mem_homogenize_iff_mem (x : A) (P : ConvexSet R A) : simpa [← ℋ.ofPoint_injective hxx'] /-- Dehomogenizing the homogenization of a convex set yields the same set again. -/ -@[simp] theorem dehomogenize_homogenize (P : ConvexSet R A) : +@[simp] theorem dehomogenize_homogenize {P : Set A} (hP : IsConvexSet R P) : dehomogenize ℋ (homogenize ℋ P) = P := by - ext x; exact ofPoint_mem_homogenize_iff_mem _ _ _ + ext x; exact ofPoint_mem_homogenize_iff_mem _ _ hP -lemma homogenize_injective : Function.Injective (homogenize ℋ) := by - intro P Q h - have hh := congr_arg (ConvexSet.dehomogenize ℋ) h - simp [dehomogenize_homogenize] at hh +lemma homogenize_injective_isConvexSet {P Q : Set A} (hP : IsConvexSet R P) (hQ : IsConvexSet R Q) + (h : homogenize ℋ P = homogenize ℋ Q) : P = Q := by + have hh := congr_arg (dehomogenize ℋ) h + simp [dehomogenize_homogenize _ hP, dehomogenize_homogenize _ hQ] at hh assumption variable {ℋ} in @@ -230,21 +256,27 @@ theorem homogenize_dehomogenize_of_le_positive {C : PointedCone R W} exact ⟨y', hy'C, hy'⟩ · exact C.isConvexSet.inter (.range ℋ.ofPoint.isAffineMap) -lemma homogenize_mono_iff {K₁ K₂ : ConvexSet R A} : - K₁.homogenize ℋ ≤ K₂.homogenize ℋ ↔ K₁ ≤ K₂ where - mp h := by simpa using dehomogenize_mono ℋ h +lemma homogenize_mono_iff {K₁ K₂ : Set A} (h₁ : IsConvexSet R K₁) (h₂ : IsConvexSet R K₂) : + homogenize ℋ K₁ ≤ homogenize ℋ K₂ ↔ K₁ ≤ K₂ where + mp h := by simpa [dehomogenize_homogenize _ h₁, dehomogenize_homogenize _ h₂] + using dehomogenize_mono ℋ h mpr := homogenize_mono _ -- Issue #66 /-- The lattice of convex sets is isomorphic to the lattice of convex sub-cones of the positive cone. -/ -def homogenizeOrderEquiv : ConvexSet R A ≃o Set.Iic ℋ.weight.positive where - toFun K := ⟨_, K.homogenize_le_weight_positive _⟩ - invFun C := dehomogenize ℋ C.1 - left_inv K := dehomogenize_homogenize _ K +def homogenizeOrderEquiv : {s : Set A // IsConvexSet R s} ≃o Set.Iic ℋ.weight.positive where + toFun K := ⟨_, homogenize_le_weight_positive _ K.val⟩ + invFun C := ⟨dehomogenize ℋ C.1, dehomogenize_isConvexSet _ _⟩ + left_inv K := by simp [dehomogenize_homogenize _ K.prop] right_inv C := by dsimp; congr; exact homogenize_dehomogenize_of_le_positive C.2 - map_rel_iff' := homogenize_mono_iff _ + map_rel_iff' := by + refine homogenize_mono_iff _ ?_ ?_ + · expose_names; exact a.prop + · expose_names; exact b.prop + +end end Field -end Convexity.ConvexSet +end Convexity diff --git a/Polyhedral/Mathlib/Geometry/Convex/Segment.lean b/Polyhedral/Mathlib/Geometry/Convex/Segment.lean new file mode 100644 index 00000000..bcfeeda9 --- /dev/null +++ b/Polyhedral/Mathlib/Geometry/Convex/Segment.lean @@ -0,0 +1,260 @@ +/- +Copyright (c) 2026 Olivia Röhrig. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Olivia Röhrig +-/ + +module + +public import Mathlib.Data.Set.Insert +public import Mathlib.Geometry.Convex.ConvexSpace.Prod + +/-! +# Segments in convex spaces + +In an R-convex space, we define the following objects: +* `Icc R x y`: Closed segment joining `x` and `y`. +* `Ioo R x y`: Open segment joining `x` and `y`. +* `Ico R x y`: Right-open segment joining `x` and `y`. +-/ + +-- this file is PR #44799 + +namespace Convexity + +open Convexity Function + +@[expose] public section Semiring + +variable (R) {X} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {s : Set X} + {x y z : X} + +/-- Segments in a convex space. Denoted as `Icc R x y` within the `Convex` namespace. -/ +def Icc (x y : X) : Set X := + { z : X | ∃ (a b : R) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), + convexCombPair a b ha hb hab x y = z } + +/-- Open segments in a convex space. Note that `Ioo R x x = {x}` instead of being `∅` when +the base semiring has some element between `0` and `1`. -/ +def Ioo (x y : X) : Set X := + { z : X | ∃ (a b : R) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1), + convexCombPair a b ha.le hb.le hab x y = z } + +/-- Left-open segments in a convex space. Denoted as `Ico R x y` within the `Convex` namespace. -/ +def Ico (x y : X) : Set X := + { z : X | ∃ (a b : R) (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1), + convexCombPair a b ha.le hb hab x y = z } + +/- [x,y] = [y,x] -/ +theorem Icc_symm (x y : X) : Icc R x y = Icc R y x := by + ext z + constructor + all_goals (intro h; rcases h with ⟨m, n, hm , hn , hmn , hz⟩; use n, m, hn, hm) + all_goals (rw [convexCombPair_symm] at hz; rw [add_comm] at hmn; use hmn) + +/- (x,y) = (y,x) -/ +theorem Ioo_symm (x y : X) : Ioo R x y = Ioo R y x := by + ext z + constructor + all_goals (intro h; rcases h with ⟨m, n, hm , hn , hmn , hz⟩; use n, m, hn, hm) + all_goals (rw [convexCombPair_symm] at hz; rw [add_comm] at hmn; use hmn) + +theorem Ioo_subset_Ico (x y : X) : Ioo R x y ⊆ Ico R x y := + fun _ ⟨a, b, ha, hb, hab, hz⟩ ↦ ⟨a, b, ha, hb.le, hab, hz⟩ + +theorem Ico_subset_Icc (x y : X) : Ico R x y ⊆ Icc R x y := + fun _ ⟨a, b, ha, hb, hab, hz⟩ ↦ ⟨a, b, ha.le, hb, hab, hz⟩ + +theorem Ioo_subset_Icc (x y : X) : Ioo R x y ⊆ Icc R x y := + le_trans (Ioo_subset_Ico R x y) (Ico_subset_Icc R x y) + +section + +variable {R} + +theorem convexCombPair_mem_Icc {a b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : + convexCombPair a b ha hb hab x y ∈ Icc R x y := by + use a, b, ha, hb, hab + +theorem convexCombPair_mem_Ioo {a b : R} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) : + convexCombPair a b ha.le hb.le hab x y ∈ Ioo R x y := by + use a, b, ha, hb, hab + +theorem convexCombPair_mem_Ico {a b : R} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) : + convexCombPair a b ha.le hb hab x y ∈ Ico R x y := by + use a, b, ha, hb, hab + +theorem forall_mem_Icc_iff (p : X → Prop) : (∀ z ∈ Icc R x y, p z) ↔ + ∀ {a b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), + p (convexCombPair a b ha hb hab x y) where + mp := fun h _ _ _ _ _ ↦ h _ <| convexCombPair_mem_Icc .. + mpr := fun h _ hz => by rcases hz with ⟨_, _, _, _, _, rfl⟩; apply h + +theorem forall_mem_Ioo_iff (p : X → Prop) : (∀ z ∈ Ioo R x y, p z) ↔ + ∀ {a b : R} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1), + p (convexCombPair a b ha.le hb.le hab x y) where + mp := fun h _ _ ha hb _ ↦ h _ <| convexCombPair_mem_Ioo ha hb .. + mpr := fun h _ hz => by rcases hz with ⟨_, _, ha, hb, _, rfl⟩; apply h ha hb + +theorem forall_mem_Ico_iff (p : X → Prop) : (∀ z ∈ Ico R x y, p z) ↔ + ∀ {a b : R} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1), + p (convexCombPair a b ha.le hb hab x y) where + mp := fun h _ _ ha hb _ ↦ h _ <| convexCombPair_mem_Ico ha .. + mpr := fun h _ hz => by rcases hz with ⟨_, _, ha, hb, _, rfl⟩; apply h ha hb + +theorem Icc_subset_iff : Icc R x y ⊆ s ↔ ∀ {a b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), + convexCombPair a b ha hb hab x y ∈ s := + forall_mem_Icc_iff .. + +theorem Ioo_subset_iff : + Ioo R x y ⊆ s ↔ ∀ {a b : R} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1), + convexCombPair a b ha.le hb.le hab x y ∈ s := + forall_mem_Ioo_iff .. + +theorem Ico_subset_iff : + Ico R x y ⊆ s ↔ ∀ {a b : R} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1), + convexCombPair a b ha.le hb hab x y ∈ s := + forall_mem_Ico_iff .. + +end + +theorem left_mem_Icc (x y : X) : x ∈ Icc R x y := + ⟨1, 0, zero_le_one, le_refl 0, add_zero 1, by rw [convexCombPair_one]⟩ + +theorem right_mem_Icc (x y : X) : y ∈ Icc R x y := + Icc_symm R y x ▸ left_mem_Icc R y x + +theorem left_mem_Ico (x y : X) : x ∈ Ico R x y := + ⟨1, 0, zero_lt_one, le_refl 0, add_zero 1, convexCombPair_one⟩ + +@[simp] +theorem Icc_same (x : X) : Icc R x x = {x} := + Set.ext fun z ↦ + ⟨fun ⟨a, b, _, _, hab, hz⟩ ↦ by + simpa [(add_smul ..).symm, Set.mem_singleton_iff, hab, one_smul, eq_comm] using hz, + fun h ↦ Set.mem_singleton_iff.1 h ▸ left_mem_Icc R z z⟩ + +@[simp] +theorem Ico_same (x : X) : Ico R x x = {x} := by + apply Set.Subset.antisymm + · rw [← Icc_same R x]; exact Ico_subset_Icc R x x + · simp [left_mem_Ico] + +theorem Ioo_insert_left (x y : X) : insert x (Ioo R x y) = Ico R x y := by + simp only [subset_antisymm_iff, Set.insert_subset_iff, left_mem_Ico, Ioo_subset_Ico, and_self, + true_and] + rintro z ⟨a, b, ha, hb', hab, rfl⟩ + by_cases hb : 0 < b + · exact Set.mem_insert_of_mem x (convexCombPair_mem_Ioo ha hb hab) + · rw [← eq_of_le_of_not_lt hb' hb] at hab + simp [← eq_of_le_of_not_lt hb' hb, add_zero a ▸ hab] + +theorem Ico_insert (x y : X) : insert y (Ico R x y) = Icc R x y := by + simp only [subset_antisymm_iff, Set.insert_subset_iff, right_mem_Icc, Ico_subset_Icc, true_and] + rintro z ⟨a, b, ha, hb, hab, rfl⟩ + refine ha.eq_or_lt.imp ?_ (fun hal ↦ convexCombPair_mem_Ico hal hb hab) + rintro rfl + simp [zero_add b ▸ hab] + +theorem Ioo_insert (x y : X) : insert x (insert y (Ioo R x y)) = Icc R x y := by + rw [Ioo_symm, Ioo_insert_left, Ico_insert, Icc_symm] + +namespace IsAffineMap + +variable {R} {Y} [ConvexSpace R Y] {f : X → Y} + +@[simp] +theorem image_Icc (hf : IsAffineMap R f) (a b : X) : + f '' Icc R a b = Icc R (f a) (f b) := + Set.ext fun _ ↦ by simp [Icc, IsAffineMap.map_convexCombPair hf] + +theorem mem_Icc_image (hf : IsAffineMap R f) {a b c : X} + (h : c ∈ Icc R a b) : f c ∈ Icc R (f a) (f b) := by + rw [← image_Icc hf, Set.mem_image] + exact ⟨c, ⟨h, rfl⟩⟩ + +@[simp] +theorem image_Ioo (hf : IsAffineMap R f) (a b : X) : + f '' Ioo R a b = Ioo R (f a) (f b) := + Set.ext fun _ ↦ by simp [Ioo, IsAffineMap.map_convexCombPair hf] + +theorem mem_Ioo_image (hf : IsAffineMap R f) {a b c : X} + (h : c ∈ Ioo R a b) : f c ∈ Ioo R (f a) (f b) := by + rw [← image_Ioo hf, Set.mem_image] + exact ⟨c, ⟨h, rfl⟩⟩ + +@[simp] +theorem image_Ico (hf : IsAffineMap R f) (a b : X) : f '' Ico R a b = Ico R (f a) (f b) := + Set.ext fun _ ↦ by simp [Ico, IsAffineMap.map_convexCombPair hf] + +theorem mem_Ico_image (hf : IsAffineMap R f) {a b c : X} (h : c ∈ Ico R a b) : + f c ∈ Ico R (f a) (f b) := by + rw [← image_Ico hf, Set.mem_image] + exact ⟨c, ⟨h, rfl⟩⟩ + +end IsAffineMap + +namespace Prod + +variable {Y} [ConvexSpace R Y] + +theorem Icc_subset (x y : X × Y) : Icc R x y ⊆ Icc R x.1 y.1 ×ˢ Icc R x.2 y.2 := by + rintro z ⟨a, b, ha, hb, hab, hz⟩ + exact ⟨⟨a, b, ha, hb, hab, by subst hz; simp⟩, a, b, ha, hb, hab, by subst hz; simp⟩ + +theorem Ioo_subset (x y : X × Y) : + Ioo R x y ⊆ Ioo R x.1 y.1 ×ˢ Ioo R x.2 y.2 := by + rintro z ⟨a, b, ha, hb, hab, hz⟩ + exact ⟨⟨a, b, ha, hb, hab, by subst hz; simp⟩, a, b, ha, hb, hab, by subst hz; simp⟩ + +theorem Ico_subset (x y : X × Y) : + Ico R x y ⊆ Ico R x.1 y.1 ×ˢ Ico R x.2 y.2 := by + rintro z ⟨a, b, ha, hb, hab, hz⟩ + exact ⟨⟨a, b, ha, hb, hab, by subst hz; simp⟩, a, b, ha, hb, hab, by subst hz; simp⟩ + +theorem image_mk_Icc_left (x₁ x₂ : X) (y : Y) : + (fun x ↦ (x, y)) '' Icc R x₁ x₂ = Icc R (x₁, y) (x₂, y) := + (IsAffineMap.prodMk IsAffineMap.id (IsAffineMap.const y)).image_Icc .. + +theorem image_mk_Icc_right (x : X) (y₁ y₂ : Y) : + (fun y ↦ (x, y)) '' Icc R y₁ y₂ = Icc R (x, y₁) (x, y₂) := + (IsAffineMap.prodMk (IsAffineMap.const x) IsAffineMap.id).image_Icc .. + +theorem image_mk_Ioo_left (x₁ x₂ : X) (y : Y) : + (fun x ↦ (x, y)) '' Ioo R x₁ x₂ = Ioo R (x₁, y) (x₂, y) := + (IsAffineMap.prodMk IsAffineMap.id (IsAffineMap.const y)).image_Ioo .. + +theorem image_mk_Ioo_right (x : X) (y₁ y₂ : Y) : + (fun y ↦ (x, y)) '' Ioo R y₁ y₂ = Ioo R (x, y₁) (x, y₂) := + (IsAffineMap.prodMk (IsAffineMap.const x) IsAffineMap.id).image_Ioo .. + +theorem image_mk_Ico_left (x₁ x₂ : X) (y : Y) : + (fun x ↦ (x, y)) '' Ico R x₁ x₂ = Ico R (x₁, y) (x₂, y) := + (IsAffineMap.prodMk IsAffineMap.id (IsAffineMap.const y)).image_Ico .. + +theorem image_mk_Ico_right (x : X) (y₁ y₂ : Y) : + (fun y ↦ (x, y)) '' Ico R y₁ y₂ = Ico R (x, y₁) (x, y₂) := + (IsAffineMap.prodMk (IsAffineMap.const x) IsAffineMap.id).image_Ico .. + +end Prod + +end Semiring + +section DenselyOrderedRing + +variable (R) {X} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] + [DenselyOrdered R] + +@[simp] +theorem Ioo_same (x : X) : Ioo R x x = {x} := + Set.ext fun z ↦ + ⟨fun ⟨a, b, _, _, hab, hz⟩ ↦ by + simpa only [convexCombPair_same, Set.mem_singleton_iff, eq_comm] using hz, + fun h : z = x ↦ by + obtain ⟨a, ha₀, ha₁⟩ := DenselyOrdered.dense (0 : R) 1 zero_lt_one + refine ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel .., ?_⟩ + rw [convexCombPair_same, h]⟩ + +end DenselyOrderedRing + +end Convexity diff --git a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Range.lean b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Range.lean deleted file mode 100644 index cd20e131..00000000 --- a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Range.lean +++ /dev/null @@ -1,94 +0,0 @@ -/- -Copyright (c) 2026 Olivia Röhrig. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Olivia Röhrig --/ -module - -public import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic - -/-! -# Range of affine maps - -The range of an affine map `f : P₁ →ᵃ[R] P₂` is an affine subspace of `P₂`. - -# Implementation note - -Follows `LinearMap.range`. - --/ - -@[expose] public section - -open Affine Module AffineMap AffineSubspace - -section - -variable {R V₁ V₂ P₁ P₂ : Type*} - -namespace AffineMap - -variable [Ring R] -variable [AddCommGroup V₁] [Module R V₁] -variable [AddCommGroup V₂] [Module R V₂] -variable [AffineSpace V₁ P₁] [AffineSpace V₂ P₂] - -variable (f : P₁ →ᵃ[R] P₂) - -/-- The range of an affine map is an affine subspace. -/ -def range : AffineSubspace R P₂ where - carrier := Set.range f - smul_vsub_vadd_mem' := by - simp only [Set.mem_range, forall_exists_index] - intro c _ _ _ x₁ h₁ x₂ h₂ x₃ h₃ - exact ⟨c • (x₁ -ᵥ x₂) +ᵥ x₃, by simp [map_vadd, ← h₁, ← h₂, ← h₃]⟩ - -/-- The range of an affine map is nonempty. -/ -instance instNonemptyRange : Nonempty (range f) := - Set.instNonemptyRange f - -@[simp, norm_cast] -theorem coe_range : f.range = Set.range f := rfl - -@[simp] -theorem mem_range (x : P₂) : x ∈ f.range ↔ ∃ (y : P₁), f y = x := - Iff.rfl - -theorem range_eq_map_top : f.range = .map f ⊤ := by ext; simp - -theorem mem_range_self (x : P₁) : f x ∈ f.range := by simp - -@[simp] -theorem range_id : (id R P₁).range = ⊤ := by ext; simp - -theorem range_direction_eq_linear_range : f.range.direction = f.linear.range := by - rw [range_eq_map_top, map_direction, direction_top, Submodule.map_top] - -variable {f} in -theorem range_subset_iff {s : AffineSubspace R P₂} : f.range ≤ s ↔ ∀ y, f y ∈ s := by - simp [AffineSubspace.le_def'] - -/-- Restrict the codomain of an affine map `f` to `f.range`. -/ -def rangeRestrict : P₁ →ᵃ[R] f.range where - toFun p := ⟨f p, p, rfl⟩ - linear := f.linear.codRestrict f.range.direction - (f.range_direction_eq_linear_range ▸ f.linear.mem_range_self) - map_vadd' _ _ := by ext; simp [map_vadd] - -theorem surjective_rangeRestrict : Function.Surjective ⇑f.rangeRestrict := - fun ⟨_, y, rfl⟩ => ⟨y, rfl⟩ - -@[simp] -theorem range_rangeRestrict : f.rangeRestrict.range = ⊤ := by - ext ⟨_, x, rfl⟩ - simpa [AffineSubspace.mem_top, iff_true] using ⟨x, rfl⟩ - -@[simp] -theorem injective_rangeRestrict_iff : - Function.Injective (rangeRestrict f) ↔ Function.Injective f := by - convert (Function.Injective.of_comp_iff Subtype.val_injective f.rangeRestrict).symm - ext; simp [rangeRestrict] - -end AffineMap - -end diff --git a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Homogenization/Basic.lean b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Homogenization/Basic.lean new file mode 100644 index 00000000..a9b6252a --- /dev/null +++ b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Homogenization/Basic.lean @@ -0,0 +1,259 @@ +/- +Copyright (c) 2026 Olivia Röhrig. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Olivia Röhrig +-/ +module + +public import Mathlib.LinearAlgebra.AffineSpace.Homogenization +public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineMap +public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.Canonical + +import Mathlib.Algebra.Module.Submodule.EqLocus + +/-! This file defines affine homogenization as any vector space linearly equivalent to +`Homogenization`, the canonical homogenization from Mathlib. It also proves every object +that satisfies the axiomatic description from [Gallier2011GeometricMethods] is a homogenization +in the linear equivalence sense (see `ofEmbed`). Use `IsHomogenization` for convenience if you want +to consider an embedding into a vector space that is not the canonical `Homogenization`. + +## Implementation notes +* We transport relevant theorems from `Homogenization`. +* The axiomatization in the literature is redundant. The universal property can be proven solely +from the remaning axioms, as is done in `lift`. +* We choose the definition via `LinearEquiv` instead of the axiomatization, since the latter only +classifies homogenizations over a ring. The one presented here can be adapted to semirings if affine +spaces over semirings become necessary. + +## References + +* [J. Gallier, *Geometric Methods and Applications for Computer Science and + Engineering*][Gallier2011GeometricMethods] + -/ + +public noncomputable section + +namespace Affine + +section Ring + +open Function Submodule + +variable {R : Type*} [Ring R] +variable {V : Type*} [AddCommGroup V] [Module R V] +variable {A : Type*} [AddTorsor V A] +variable {W : Type*} [AddCommGroup W] [Module R W] + +variable (R A W) in +/-- A triple of a ring `R`, `R`-affine space `A` and `R`-vector space `W` is a homogenization if +`W` is linearly equivalent to the canonical homogenization. -/ +structure IsHomogenization where ofRepr :: + repr : W ≃ₗ[R] Homogenization R A + +namespace IsHomogenization + +variable (ℋ : IsHomogenization R A W) + +/-- The embedding of the affine space into the homogenization. -/ +@[expose] +def ofPoint : A →ᵃ[R] W := ℋ.repr.symm.toAffineMap.comp Homogenization.ofPoint + +/-- The embedding of the vector space into the homogenization. -/ +@[expose] +def ofVector : V →ₗ[R] W := ℋ.repr.symm.toLinearMap ∘ₗ Homogenization.ofVector + +theorem ofPoint_injective : Injective ℋ.ofPoint := by + simpa [ofPoint] using Homogenization.ofPoint_injective + +theorem ofVector_injective : Injective ℋ.ofVector := by + simpa [ofVector] using Homogenization.ofVector_injective + +theorem span_range_ofPoint : span R (Set.range ℋ.ofPoint) = ⊤ := by + simpa [Set.range_comp, ofPoint] using Homogenization.span_range_ofPoint + +section + +variable {U : Type*} [AddCommGroup U] [Module R U] +variable {F : Type*} [FunLike F W U] [LinearMapClass F R _ _] + +-- we duplicate the proof because translating using the typeclass is a pain +theorem hom_ext {f g : F} (h : ∀ x, f (ℋ.ofPoint x) = g (ℋ.ofPoint x)) : f = g := by + apply LinearMap.ofClass_injective + rwa [← LinearMap.eqLocus_eq_top, eq_top_iff, ← ℋ.span_range_ofPoint, Submodule.span_le, + Set.range_subset_iff] + +theorem hom_ext_iff {f g : F} : f = g ↔ ∀ x, f (ℋ.ofPoint x) = g (ℋ.ofPoint x) := + ⟨by rintro rfl _; rfl, ℋ.hom_ext⟩ + +end + +section + +variable {U : Type*} [AddCommGroup U] [Module R U] + +/-- An affine map on `A` taking values in a vector space extends uniquely to a linear map on `W`. +-/ +def lift : (A →ᵃ[R] U) ≃+ (W →ₗ[R] U) := + Homogenization.lift.trans (ℋ.repr.arrowCongrAddEquiv (LinearEquiv.refl ..)).symm + +@[simp] +theorem lift_apply_ofPoint (f : A →ᵃ[R] U) (p : A) : ℋ.lift f (ℋ.ofPoint p) = f p := by + simp [lift, ofPoint] + +@[simp] +theorem lift_apply_ofVector (f : A →ᵃ[R] U) (v : V) : ℋ.lift f (ℋ.ofVector v) = f.linear v := by + simp [lift, ofVector] + +end + +/-- The linear map that is constantly `1` when restricted to `A`. -/ +def weight : W →ₗ[R] R := Homogenization.weight ∘ₗ ℋ.repr.toLinearMap + +/-- The homogenization of a point in `A` has weight 1. -/ +@[simp] +theorem weight_ofPoint (a₀ : A) : ℋ.weight (ℋ.ofPoint a₀) = 1 := by simp [weight, ofPoint] + +/-- The homogenization of a point in `V` has weight 0. -/ +@[simp] +theorem weight_ofVector (v : V) : ℋ.weight (ℋ.ofVector v) = 0 := by simp [weight, ofVector] + +theorem weight_eq_zero_iff {x : W} : ℋ.weight x = 0 ↔ ∃ v, x = ℋ.ofVector v := by + simpa [← LinearEquiv.symm_apply_eq, weight, ofVector] using Homogenization.weight_eq_zero_iff + +theorem weight_eq_one_iff {x : W} : ℋ.weight x = 1 ↔ ∃ p, x = ℋ.ofPoint p := by + simpa [← LinearEquiv.symm_apply_eq, weight, ofPoint] using Homogenization.weight_eq_one_iff + +-- the following two are in canonical hom in #43448 +theorem ofPoint_ne_ofVector [Nontrivial R] (x : A) (v : V) : ℋ.ofPoint x ≠ ℋ.ofVector v := + ne_of_apply_ne ℋ.weight <| by simp + +theorem ofPoint_ne_zero [Nontrivial R] (x : A) : ℋ.ofPoint x ≠ 0 := by + simpa using ℋ.ofPoint_ne_ofVector x 0 + +theorem ofPoint_range_eq_preimage_weight_one : Set.range ℋ.ofPoint = ℋ.weight ⁻¹' {1} := by + ext; simp [↓weight_eq_one_iff, eq_comm] + +theorem ofVector_range_eq_preimage_weight_zero : Set.range ℋ.ofVector = ℋ.weight ⁻¹' {0} := by + ext; simp [↓weight_eq_zero_iff, eq_comm] + +/-- Embedding the underlying vector space is exactly the weight-0 hyperplane. -/ +theorem ofVector_range_eq_weight_ker : ℋ.ofVector.range = ℋ.weight.ker := by + apply SetLike.ext' + rw [LinearMap.coe_range, ofVector_range_eq_preimage_weight_zero, LinearMap.ker] + ext x + simp + +theorem repr_comp_ofPoint : + ℋ.repr ∘ ℋ.ofPoint = Homogenization.ofPoint := by + ext a; simp [ofPoint] + +theorem weight_comp_repr : + ℋ.weight ∘ₗ ℋ.repr.symm = Homogenization.weight (P := A) := by + simp [weight, LinearMap.comp_assoc] + +open AffineMap LinearEquiv in +/-- The linear equivalence between the underlying vector space and its embedding. -/ +def ofVectorRangeEquiv : V ≃ₗ[R] ℋ.ofVector.range where + toFun v := ⟨ℋ.ofVector v, ℋ.ofVector.mem_range_self v⟩ + map_add' v w := by simp + map_smul' r v := by simp + invFun := (ofInjective ℋ.ofVector (linear_injective_iff _ |>.mpr ℋ.ofPoint_injective)).invFun + left_inv := LinearEquiv.left_inv _ + right_inv := LinearEquiv.right_inv _ + +/-- The affine equivalence between the affine space space and its embedding. -/ +public def ofPointRangeEquiv : A ≃ᵃ[R] ℋ.ofPoint.range := + .ofBijective + ⟨ℋ.ofPoint.rangeRestrict_injective_iff.mpr ℋ.ofPoint_injective, fun ⟨_, a, rfl⟩ => ⟨a, rfl⟩⟩ + +theorem apply_ofPointRangeEquiv_symm (x : ℋ.ofPoint.range) : + ℋ.ofPoint (ℋ.ofPointRangeEquiv.symm x) = x := by + rw [← ℋ.ofPointRangeEquiv.right_inv x] + congr; exact ℋ.ofPointRangeEquiv.symm_apply_apply _ + +section + +variable {U : Type*} [AddCommGroup U] [Module R U] {f : A →ᵃ[R] U} {g : U →ₗ[R] R} + +lemma comp_lift_eq_weight_of_range_preimage (f_range : Set.range f = g ⁻¹' {1}) : + g ∘ₗ (ℋ.lift f) = ℋ.weight := by + refine ℋ.hom_ext (fun p ↦ ?_) + have := f_range ▸ Set.mem_range_self p + simpa [LinearMap.comp_apply, ofPoint, weight, lift] using this + +lemma lift_bijective_of_injective_of_range_preimage (f_inj : Injective f) + (f_range : Set.range f = g ⁻¹' {1}) : Bijective (ℋ.lift f) := by + constructor + · rw [injective_iff_map_eq_zero] + intro a ha + have : ℋ.weight a = 0 := by simp [← ℋ.comp_lift_eq_weight_of_range_preimage f_range, ha] + obtain ⟨_, rfl⟩ := ℋ.weight_eq_zero_iff.mp this + rw [ℋ.lift_apply_ofVector] at ha + simp [(map_eq_zero_iff _ (f.linear_injective_iff.mpr f_inj)).mp ha] + · intro w + obtain p₀ := Classical.arbitrary A + obtain ⟨a, ha⟩ : w - g w • f p₀ + f p₀ ∈ Set.range f := by + rw [f_range] + have : g (w - g w • f p₀ + f p₀) = 1 := by + have : f p₀ ∈ g ⁻¹' {1} := f_range ▸ Set.mem_range_self p₀ + rw [map_add, map_sub, map_smul, this, smul_eq_mul, mul_one, sub_self, zero_add] + simpa using this + exact ⟨ℋ.ofVector (a -ᵥ p₀) + g w • ℋ.ofPoint p₀, by simp [ofPoint, ofVector, lift, ha]⟩ + +end + +section Constructions + +variable (R A) in +/-- The canonical homogenization is a homogenization. -/ +def canonical : IsHomogenization R A (Homogenization R A) := ofRepr <| LinearEquiv.refl .. + +/-- Construct a homogenization from an embedding of the affine space `A` into the vector +space `W` and a weight map that is the constant 1-map on the embedded `A`. This follows the +axiomatization in Definition 4.2 of [Gallier2011GeometricMethods] +https://www.cis.upenn.edu/~jean/gma-v2-root.pdf -/ +def ofEmbed {embed : A →ᵃ[R] W} (embed_inj : Injective embed) {weight : W →ₗ[R] R} + (embed_range : Set.range embed = weight ⁻¹' {1}) : + IsHomogenization R A W where + repr := by + apply (LinearEquiv.ofBijective (Homogenization.lift embed) ?_).symm + exact (lift_bijective_of_injective_of_range_preimage (canonical R A) embed_inj embed_range) + +/-- The embedding used in the construction becomes the embedding in the homogenization. -/ +theorem ofEmbed_ofPoint {embed : A →ᵃ[R] W} (embed_inj : Injective embed) + {weight : W →ₗ[R] R} (embed_range : Set.range embed = weight ⁻¹' {1}) : + (ofEmbed embed_inj embed_range).ofPoint = embed := by + ext p + exact Homogenization.lift_apply_ofPoint .. + +/-- The weight used in the construction becomes the weight in the homogenization. -/ +theorem ofEmbed_weight {embed : A →ᵃ[R] W} (embed_inj : Injective embed) + {weight : W →ₗ[R] R} (embed_range : Set.range embed = weight ⁻¹' {1}) : + (ofEmbed embed_inj embed_range).weight = weight := by + ext w + unfold IsHomogenization.weight + have : Homogenization.lift embed ((ofEmbed embed_inj embed_range).repr w) = w := by + rw [← LinearEquiv.ofBijective_apply] + exact LinearEquiv.apply_symm_apply _ w + rw [LinearMap.coe_comp, ← this, ← LinearMap.comp_apply] + congr + exact (comp_lift_eq_weight_of_range_preimage (canonical R A) embed_range).symm + +/-- A module is a homogenization of the weight-one hyperplane of any linear functional, +provided that hyperplane is nonempty. -/ +def ofWeightOne (g : W →ₗ[R] R) [Nonempty ((affineSpan R {1}).comap g.toAffineMap)] : + IsHomogenization R ((affineSpan R {1}).comap g.toAffineMap) W := + ofEmbed (weight := g) (AffineSubspace.subtype_injective _) (by simp; rfl) + +@[simp] +theorem ofWeightOne_weight (g : W →ₗ[R] R) [Nonempty ((affineSpan R {1}).comap g.toAffineMap)] : + (ofWeightOne g).weight = g := by + simp [ofWeightOne, ofEmbed_weight] + +end Constructions + +end IsHomogenization + +end Ring + +end Affine diff --git a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Homogenization/IsHomogenization.lean b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Homogenization/IsHomogenization.lean index 0269d8f3..b6530a8e 100644 --- a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Homogenization/IsHomogenization.lean +++ b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Homogenization/IsHomogenization.lean @@ -6,7 +6,7 @@ Authors: Olivia Röhrig, Martin Winter module public import Mathlib.LinearAlgebra.AffineSpace.AffineMap -public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Range +public import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Range public import Mathlib.LinearAlgebra.AffineSpace.Homogenization public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic @@ -174,7 +174,7 @@ lemma comp_lift_eq_weight (h : ∀ p, g (f p) = 1) : g ∘ₗ (ℋ.lift f) = ℋ lemma lift_bijective_injective_range_comap (hinj : Injective f) (hrange : f.range = comap g.toAffineMap {1}) : Bijective (ℋ.lift f) := by - have g_f : ∀ p, g (f p) = 1 := AffineMap.range_subset_iff.mp hrange.le + have g_f : ∀ p, g (f p) = 1 := Set.range_subset_iff.mp hrange.le constructor · rw [injective_iff_map_eq_zero] intro a ha diff --git a/lake-manifest.json b/lake-manifest.json index 4810c658..3e505232 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "cfc55fc58714a59dc06e6e79edc6d1d95140d3c2", + "rev": "eb6d361fd932140a10cc8d9f4be0db7f73b9bedf", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "dfa4f38190d07c37e315953e08b90fe2d95b3c24", + "rev": "c2d7840c65673533e15b499f25beecdc6227f7d8", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d6b4c7be5be75ec4917c873ac50c756dc1436372", + "rev": "9d39f9bb0c30aa2f6200808805ff16e6ce950890", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93", + "rev": "19a8e822bfeace1ae4e090045aad81e0c930e6cf", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "df72b022e558978a1c50264cfc4d7fec86fa8e04", + "rev": "ff78fbc75a9bffb4ef08f8c290e268d120cd27d7", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4a174c490d8707121c4a9290800489f105d85e07", + "rev": "29c64c56cc38211d39b306db2df11701e3d3de11", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "dce0ad79c486cb1fb504af04f953c3466b0c6db8", + "rev": "6d26f8bb4b2bb78f929ad160feac508866821316", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "66e469188fe07963e5cf666c7d4433f45b8131c5", + "rev": "8e746d768c73b716c7d4bc07bd8e73f2a75bdb60", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -115,10 +115,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "c24fe6078c630e89b489bffe59b3e20ac30d12c8", + "rev": "34d2efffcb6dc8d5f3537cf6a7f88bfaa999ec49", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.35.0", + "inputRev": "v4.36.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/fgdorais/lean4-unicode-basic", diff --git a/lean-toolchain b/lean-toolchain index a6aff065..d0cf8c52 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.35.0 +leanprover/lean4:v4.36.0-rc1 \ No newline at end of file