Fix positive_eq_hull_preimage_singleton and move homogenize_top

Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/LinearMap.lean

@@ -43,6 +43,13 @@ lemma le_nonneg_add {C : PointedCone R M} {f g : M →ₗ[R] R}
     (hCf : C ≤ f.nonneg) (hCg : C ≤ g.nonneg) : C ≤ (f + g).nonneg :=
   fun _ hx => add_nonneg (hCf hx) (hCg hx)
 
+/-- The cone hull of a subset of a nonnegative level set of `f` is contained in the nonnegative
+cone of `f`. See `hull_le_positive_of_subset_preimage_singleton` for the strict version. -/
+lemma hull_le_nonneg_of_subset_preimage_singleton {f : M →ₗ[R] R} {s : Set M} {c : R}
+    (hc : 0 ≤ c) (hs : s ⊆ f ⁻¹' {c}) :
+    PointedCone.hull R s ≤ f.nonneg :=
+  Submodule.span_le.mpr fun x hx => mem_nonneg.mpr <| (hs hx : f x = c) ▸ hc
+
 end Semiring
 
 section IsStrictOrderedRing
@@ -102,18 +109,41 @@ lemma positive_inf_ker {f : M →ₗ[R] R} : f.positive ⊓ f.ker = ⊥ := by
 
 @[simp] lemma positive_zero : positive (0 : M →ₗ[R] R) = ⊥ := by ext x; simp
 
-lemma positive_eq_hull_preimage_singleton (f : M →ₗ[R] R) (c : R) (hc : c ≠ 0) :
-    f.positive = PointedCone.hull R (f ⁻¹' {c}) := by
-  sorry
-
+/-- The cone hull of a subset of a positive level set of `f` is contained in the positive cone
+of `f`. The assumption `0 < c` cannot be weakened to `c ≠ 0`: for `c < 0` the hull lies in the
+nonpositive cone of `f`. See `hull_le_nonneg_of_subset_preimage_singleton` for the version with
+`0 ≤ c` and `positive_eq_hull_preimage_singleton` for an equality version over linearly ordered
+fields. -/
 lemma hull_le_positive_of_subset_preimage_singleton {f : M →ₗ[R] R} {s : Set M} {c : R}
-    (hc : c ≠ 0) (hs : s ⊆ f ⁻¹' {c}) :
-    PointedCone.hull R s ≤ f.positive := by
-  rw [positive_eq_hull_preimage_singleton f c hc]
-  exact Submodule.span_mono hs
+    (hc : 0 < c) (hs : s ⊆ f ⁻¹' {c}) :
+    PointedCone.hull R s ≤ f.positive :=
+  Submodule.span_le.mpr fun x hx => mem_positive.mpr fun _ => (hs hx : f x = c) ▸ hc
 
 end IsStrictOrderedRing
 
+section Field
+
+variable {R : Type*} [Field R] [LinearOrder R] [IsOrderedRing R]
+variable {M : Type*} [AddCommGroup M] [Module R M]
+
+/-- Over a linearly ordered field, the positive cone of a linear form `f` is the cone hull of
+any of its positive level sets. This can fail in the absence of scalar inverses: over `ℕ` with
+`f = id` and `c = 2` the cone hull of the level set is `2 • ℕ`, while the positive cone is all
+of `ℕ`. -/
+lemma positive_eq_hull_preimage_singleton (f : M →ₗ[R] R) {c : R} (hc : 0 < c) :
+    f.positive = PointedCone.hull R (f ⁻¹' {c}) := by
+  refine le_antisymm (fun x hx => ?_) (hull_le_positive_of_subset_preimage_singleton hc subset_rfl)
+  by_cases hx0 : x = 0
+  · simp [hx0]
+  have hfx : 0 < f x := hx hx0
+  have hy : (c / f x) • x ∈ f ⁻¹' {c} := by
+    simp [div_mul_cancel₀ c hfx.ne']
+  have hmem := (PointedCone.hull R (f ⁻¹' {c})).smul_mem
+    (div_nonneg hfx.le hc.le) (Submodule.subset_span hy)
+  rwa [smul_smul, div_mul_div_comm, mul_comm c (f x), div_self (by positivity), one_smul] at hmem
+
+end Field
+
 section Ring
 
 variable {R M : Type*} [Ring R] [LinearOrder R] [IsOrderedRing R] [AddCommGroup M]

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

@@ -49,16 +49,15 @@ def homogenizeOrderHom : ConvexSet R A →o PointedCone R W where
 lemma homogenize_bot : homogenize W (⊥ : ConvexSet R A) = ⊥ := by
   simp [homogenize, Bot.bot]
 
-lemma homogenize_top : homogenize W (⊤ : ConvexSet R A) = hom.weight.positive := by
-  rw [homogenize, LinearMap.positive_eq_hull_preimage_singleton hom.weight 1 one_ne_zero,
-    ← hom.ofPoint_range_eq_preimage_weight_one]
-  congr
-  ext x
-  simp
+/- NOTE: `homogenize_top`, stating `homogenize W (⊤ : ConvexSet R A) = hom.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) :
     homogenize W K ≤ hom.weight.positive := by
-  exact LinearMap.hull_le_positive_of_subset_preimage_singleton one_ne_zero fun _ ↦ by
+  exact LinearMap.hull_le_positive_of_subset_preimage_singleton one_pos fun _ ↦ by
     rintro ⟨x, -, rfl⟩
     simp [hom.weight_one]
 
@@ -154,6 +153,14 @@ variable [IsModuleConvexSpace R W]
 
 variable [hom : Affine.IsHomogenization R A W]
 
+omit [IsModuleConvexSpace R W] in
+/-- The homogenization of the full affine space is the positive cone of the weight functional. -/
+lemma homogenize_top : homogenize W (⊤ : ConvexSet R A) = hom.weight.positive := by
+  rw [homogenize, LinearMap.positive_eq_hull_preimage_singleton hom.weight one_pos,
+    ← hom.ofPoint_range_eq_preimage_weight_one]
+  congr! with x
+  simp
+
 lemma smul_pos_of_mem_homogenize {P : ConvexSet R A} {x} (h : x ∈ homogenize W P) (hx : x ≠ 0) :
     x ∈ Set.Ioi (0 : R) • hom.ofPoint '' (P : Set A) :=
   (mem_hull_iff_mem_pos_smul_of_convex_nonzero