refactor: redefine ProperCone as an abbrev for ClosedSubmodule (#25204)

... and derive the `ProperCone` operations from `ClosedSubmodule` too. Also rename the scalar ring from `𝕜` to `R`.

From Toric

Author: YaelDillies

Mathlib/Analysis/Convex/Cone/Basic.lean

@@ -1,10 +1,12 @@
 /-
 Copyright (c) 2022 Apurva Nakade. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Apurva Nakade
+Authors: Apurva Nakade, Yaël Dillies
 -/
 import Mathlib.Analysis.Convex.Cone.Closure
-import Mathlib.Analysis.InnerProductSpace.Defs
+import Mathlib.Topology.Algebra.Module.ClosedSubmodule
+import Mathlib.Topology.Algebra.Order.Module
+import Mathlib.Topology.Order.OrderClosed
 
 /-!
 # Proper cones
@@ -30,156 +32,119 @@ The next steps are:
 
 -/
 
-open ContinuousLinearMap Filter Set
+open ContinuousLinearMap Filter Function Set
 
-/-- A proper cone is a pointed cone `K` that is closed. Proper cones have the nice property that
+variable {R E F G : Type*} [Semiring R] [PartialOrder R] [IsOrderedRing R]
+variable [AddCommMonoid E] [TopologicalSpace E] [Module R E]
+variable [AddCommMonoid F] [TopologicalSpace F] [Module R F]
+variable [AddCommMonoid G] [TopologicalSpace G] [Module R G]
+
+local notation "R≥0" => {r : R // 0 ≤ r}
+
+variable (R E) in
+/-- A proper cone is a pointed cone `C` that is closed. Proper cones have the nice property that
 they are equal to their double dual, see `ProperCone.dual_dual`.
 This makes them useful for defining cone programs and proving duality theorems. -/
-structure ProperCone (𝕜 : Type*) (E : Type*)
-    [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [AddCommMonoid E]
-    [TopologicalSpace E] [Module 𝕜 E] extends Submodule {c : 𝕜 // 0 ≤ c} E where
-  isClosed' : IsClosed (carrier : Set E)
+abbrev ProperCone := ClosedSubmodule R≥0 E
 
 namespace ProperCone
 section Module
+variable {C C₁ C₂ : ProperCone R E} {r : R} {x : E}
 
-variable {𝕜 : Type*} [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜]
-variable {E : Type*} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E]
-
-/-- A `PointedCone` is defined as an alias of submodule. We replicate the abbreviation here and
-define `toPointedCone` as an alias of `toSubmodule`. -/
-abbrev toPointedCone (C : ProperCone 𝕜 E) := C.toSubmodule
+/-- Any proper cone can be seen as a pointed cone.
 
-attribute [coe] toPointedCone
+This is an alias of `ClosedSubmodule.toSubmodule` for convenience and discoverability. -/
+@[coe] abbrev toPointedCone (C : ProperCone R E) : PointedCone R E := C.toSubmodule
 
-instance : Coe (ProperCone 𝕜 E) (PointedCone 𝕜 E) :=
-  ⟨toPointedCone⟩
+instance : Coe (ProperCone R E) (PointedCone R E) := ⟨toPointedCone⟩
 
-theorem toPointedCone_injective : Function.Injective ((↑) : ProperCone 𝕜 E → PointedCone 𝕜 E) :=
-  fun S T h => by cases S; cases T; congr
+lemma toPointedCone_injective : Injective ((↑) : ProperCone R E → PointedCone R E) :=
+  ClosedSubmodule.toSubmodule_injective
 
 -- TODO: add `ConvexConeClass` that extends `SetLike` and replace the below instance
-instance : SetLike (ProperCone 𝕜 E) E where
-  coe K := K.carrier
-  coe_injective' _ _ h := ProperCone.toPointedCone_injective (SetLike.coe_injective h)
+instance : SetLike (ProperCone R E) E where
+  coe C := C.carrier
+  coe_injective' _ _ h := ProperCone.toPointedCone_injective <| SetLike.coe_injective h
 
-@[ext]
-theorem ext {S T : ProperCone 𝕜 E} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T :=
-  SetLike.ext h
+@[ext] lemma ext (h : ∀ x, x ∈ C₁ ↔ x ∈ C₂) : C₁ = C₂ := SetLike.ext h
 
-@[simp]
-theorem mem_coe {x : E} {K : ProperCone 𝕜 E} : x ∈ (K : PointedCone 𝕜 E) ↔ x ∈ K :=
-  Iff.rfl
+@[simp] lemma mem_toPointedCone : x ∈ C.toPointedCone ↔ x ∈ C := .rfl
 
-instance instZero (K : ProperCone 𝕜 E) : Zero K := PointedCone.instZero (K.toSubmodule)
+@[deprecated (since := "2025-06-11")] alias mem_coe := mem_toPointedCone
 
-protected theorem nonempty (K : ProperCone 𝕜 E) : (K : Set E).Nonempty :=
-  ⟨0, by { simp_rw [SetLike.mem_coe, ← ProperCone.mem_coe, Submodule.zero_mem] }⟩
+lemma pointed_toConvexCone (C : ProperCone R E) : (C : ConvexCone R E).Pointed :=
+  C.toPointedCone.pointed_toConvexCone
 
-protected theorem isClosed (K : ProperCone 𝕜 E) : IsClosed (K : Set E) :=
-  K.isClosed'
+@[deprecated (since := "2025-06-11")] protected alias pointed := pointed_toConvexCone
 
-end Module
+protected lemma nonempty (C : ProperCone R E) : (C : Set E).Nonempty := C.toSubmodule.nonempty
+protected lemma isClosed (C : ProperCone R E) : IsClosed (C : Set E) := C.isClosed'
 
-section PositiveCone
+protected nonrec lemma smul_mem (C : ProperCone R E) (hx : x ∈ C) (hr : 0 ≤ r) : r • x ∈ C :=
+  C.smul_mem ⟨r, hr⟩ hx
 
-variable (𝕜 E)
-variable [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜]
-  [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E]
-  [TopologicalSpace E] [OrderClosedTopology E]
+section T1Space
+variable [T1Space E]
 
-/-- The positive cone is the proper cone formed by the set of nonnegative elements in an ordered
-module. -/
-def positive : ProperCone 𝕜 E where
-  toSubmodule := PointedCone.positive 𝕜 E
-  isClosed' := isClosed_Ici
+lemma mem_bot : x ∈ (⊥ : ProperCone R E) ↔ x = 0 := .rfl
 
-@[simp]
-theorem mem_positive {x : E} : x ∈ positive 𝕜 E ↔ 0 ≤ x :=
-  Iff.rfl
+@[simp, norm_cast] lemma coe_bot : (⊥ : ProperCone R E) = ({0} : Set E) := rfl
+@[simp, norm_cast] lemma toPointedCone_bot : (⊥ : ProperCone R E).toPointedCone = ⊥ := rfl
 
-@[simp]
-theorem coe_positive : ↑(positive 𝕜 E) = ConvexCone.positive 𝕜 E :=
-  rfl
+@[deprecated (since := "2025-06-11")] alias mem_zero := mem_bot
+@[deprecated (since := "2025-06-11")] alias coe_zero := coe_bot
+@[deprecated (since := "2025-06-11")] alias pointed_zero := pointed_toConvexCone
 
-end PositiveCone
+end T1Space
 
-section Module
+/-- The closure of image of a proper cone under a `R`-linear map is a proper cone. We
+use continuous maps here so that the comap of f is also a map between proper cones. -/
+abbrev comap (f : E →L[R] F) (C : ProperCone R F) : ProperCone R E :=
+  ClosedSubmodule.comap (f.restrictScalars R≥0) C
 
-variable {𝕜 : Type*} [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜]
-variable {E : Type*} [AddCommMonoid E] [TopologicalSpace E] [T1Space E] [Module 𝕜 E]
+@[simp] lemma comap_id (C : ProperCone R F) : C.comap (.id _ _) = C := rfl
 
-instance : Zero (ProperCone 𝕜 E) :=
-  ⟨{ toSubmodule := 0
-     isClosed' := isClosed_singleton }⟩
+@[simp] lemma coe_comap (f : E →L[R] F) (C : ProperCone R F) : (C.comap f : Set E) = f ⁻¹' C := rfl
 
-instance : Inhabited (ProperCone 𝕜 E) :=
-  ⟨0⟩
+lemma comap_comap (g : F →L[R] G) (f : E →L[R] F) (C : ProperCone R G) :
+    (C.comap g).comap f = C.comap (g.comp f) := rfl
 
-@[simp]
-theorem mem_zero (x : E) : x ∈ (0 : ProperCone 𝕜 E) ↔ x = 0 :=
-  Iff.rfl
+lemma mem_comap {C : ProperCone R F} {f : E →L[R] F} : x ∈ C.comap f ↔ f x ∈ C := .rfl
 
-@[simp, norm_cast]
-theorem coe_zero : ↑(0 : ProperCone 𝕜 E) = (0 : ConvexCone 𝕜 E) :=
-  rfl
+variable [ContinuousAdd F] [ContinuousConstSMul R F]
 
-theorem pointed_zero : ((0 : ProperCone 𝕜 E) : ConvexCone 𝕜 E).Pointed := by
-  simp [ConvexCone.pointed_zero]
+/-- The closure of image of a proper cone under a linear map is a proper cone.
 
-end Module
+We use continuous maps here to match `ProperCone.comap`. -/
+abbrev map (f : E →L[R] F) (C : ProperCone R E) : ProperCone R F :=
+  ClosedSubmodule.map (f.restrictScalars R≥0) C
 
-section InnerProductSpace
-
-variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
-variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
-variable {G : Type*} [NormedAddCommGroup G] [InnerProductSpace ℝ G]
-
-protected theorem pointed (K : ProperCone ℝ E) : (K : ConvexCone ℝ E).Pointed :=
-  zero_mem K.toPointedCone
-
-/-- The closure of image of a proper cone under a continuous `ℝ`-linear map is a proper cone. We
-use continuous maps here so that the comap of f is also a map between proper cones. -/
-noncomputable def map (f : E →L[ℝ] F) (K : ProperCone ℝ E) : ProperCone ℝ F where
-  toSubmodule := PointedCone.closure (PointedCone.map (f : E →ₗ[ℝ] F) ↑K)
-  isClosed' := isClosed_closure
+@[simp] lemma map_id (C : ProperCone R F) : C.map (.id _ _) = C := ClosedSubmodule.map_id _
 
 @[simp, norm_cast]
-theorem coe_map (f : E →L[ℝ] F) (K : ProperCone ℝ E) :
-    ↑(K.map f) = (PointedCone.map (f : E →ₗ[ℝ] F) ↑K).closure :=
-  rfl
+lemma coe_map (f : E →L[R] F) (C : ProperCone R E) :
+    C.map f = (C.toPointedCone.map (f : E →ₗ[R] F)).closure := rfl
 
 @[simp]
-theorem mem_map {f : E →L[ℝ] F} {K : ProperCone ℝ E} {y : F} :
-    y ∈ K.map f ↔ y ∈ (PointedCone.map (f : E →ₗ[ℝ] F) ↑K).closure :=
-  Iff.rfl
+lemma mem_map {f : E →L[R] F} {C : ProperCone R E} {y : F} :
+    y ∈ C.map f ↔ y ∈ (C.toPointedCone.map (f : E →ₗ[R] F)).closure := .rfl
 
-@[simp]
-theorem map_id (K : ProperCone ℝ E) : K.map (ContinuousLinearMap.id ℝ E) = K :=
-  ProperCone.toPointedCone_injective <| by simpa using IsClosed.closure_eq K.isClosed
-
-/-- The preimage of a proper cone under a continuous `ℝ`-linear map is a proper cone. -/
-noncomputable def comap (f : E →L[ℝ] F) (S : ProperCone ℝ F) : ProperCone ℝ E where
-  toSubmodule := PointedCone.comap (f : E →ₗ[ℝ] F) S
-  isClosed' := by
-    rw [PointedCone.comap]
-    apply IsClosed.preimage f.2 S.isClosed
-
-@[simp]
-theorem coe_comap (f : E →L[ℝ] F) (S : ProperCone ℝ F) : (S.comap f : Set E) = f ⁻¹' S :=
-  rfl
+end Module
 
-@[simp]
-theorem comap_id (S : ConvexCone ℝ E) : S.comap LinearMap.id = S :=
-  SetLike.coe_injective preimage_id
+section PositiveCone
+variable {E : Type*} [AddCommGroup E] [TopologicalSpace E] [Module R E] [PartialOrder E]
+  [IsOrderedAddMonoid E] [OrderedSMul R E] [OrderClosedTopology E] {x : E}
 
-theorem comap_comap (g : F →L[ℝ] G) (f : E →L[ℝ] F) (S : ProperCone ℝ G) :
-    (S.comap g).comap f = S.comap (g.comp f) :=
-  SetLike.coe_injective <| by congr
+variable (R E) in
+/-- The positive cone is the proper cone formed by the set of nonnegative elements in an ordered
+module. -/
+@[simps!]
+def positive : ProperCone R E where
+  toSubmodule := PointedCone.positive R E
+  isClosed' := isClosed_Ici
 
-@[simp]
-theorem mem_comap {f : E →L[ℝ] F} {S : ProperCone ℝ F} {x : E} : x ∈ S.comap f ↔ f x ∈ S :=
-  Iff.rfl
+@[simp] lemma mem_positive : x ∈ positive R E ↔ 0 ≤ x := .rfl
+@[simp] lemma toPointedCone_positive : (positive R E).toPointedCone = .positive R E := rfl
 
-end InnerProductSpace
+end PositiveCone
 end ProperCone

Mathlib/Analysis/Convex/Cone/InnerDual.lean

@@ -250,7 +250,7 @@ theorem hyperplane_separation (K : ProperCone ℝ H) {f : H →L[ℝ] F} {b : F}
   mp := by
     -- suppose `b ∈ K.map f`
     simp only [mem_map, PointedCone.mem_closure, PointedCone.coe_map, ContinuousLinearMap.coe_coe,
-      mem_closure_iff_seq_limit, mem_image, SetLike.mem_coe, mem_coe, mem_dual,
+      mem_closure_iff_seq_limit, mem_image, SetLike.mem_coe, mem_dual,
       ContinuousLinearMap.adjoint_inner_right, forall_exists_index, and_imp]
     -- there is a sequence `seq : ℕ → F` in the image of `f` that converges to `b`
     rintro seq hmem htends y hinner