feat(Geometry/Convex): modules are convex spaces (#39531)

Show that every semimodule over an ordered semiring is a convex space.

It is sadly impossible to make this a global instance since it creates diamonds with structural instances such as `ConvexSpace R X → ConvexSpace R Y → ConvexSpace R (X × Y)` because `(∑ i, f i).fst = ∑ i, (f i).fst` isn't defeq, ultimately because `Finset.sum` isn't a field of `AddCommMonoid`.

Author: YaelDillies

Mathlib.lean

@@ -4516,6 +4516,7 @@ public import Mathlib.Geometry.Convex.Cone.Simplicial
 public import Mathlib.Geometry.Convex.Cone.TensorProduct
 public import Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
 public import Mathlib.Geometry.Convex.ConvexSpace.Defs
+public import Mathlib.Geometry.Convex.ConvexSpace.Module
 public import Mathlib.Geometry.Convex.ConvexSpace.Prod
 public import Mathlib.Geometry.Diffeology.Basic
 public import Mathlib.Geometry.Euclidean.Altitude

Mathlib/Analysis/Convex/MetricSpace.lean

@@ -9,6 +9,7 @@ public import Mathlib.Analysis.Convex.Combination
 public import Mathlib.Analysis.Normed.Group.AddTorsor
 public import Mathlib.Analysis.Normed.Module.Basic
 public import Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
+public import Mathlib.Geometry.Convex.ConvexSpace.Module
 
 /-!
 
@@ -40,11 +41,9 @@ public section
 
 namespace Convexity
 
-attribute [local instance] AddTorsor.toConvexSpace
-
 open ConvexSpace
 
-variable {I X : Type*} [ConvexSpace ℝ X] [MetricSpace X]
+variable {I X : Type*}
 
 variable (X) in
 /-- A convex metric space is a real convex space with a compatible metric structure.
@@ -56,19 +55,19 @@ In particular, convex subsets of normed affine spaces are convex metric spaces.
 Note that there is a separate notion of
 [convex metric spaces](https://en.wikipedia.org/wiki/Convex_metric_space) in the literature
 that has little to do with this definition. -/
-class IsConvexDist : Prop where
+class IsConvexDist [inst₁ : ConvexSpace ℝ X] [inst₂ : MetricSpace X] : Prop where
   /-- Use `dist_iConvexComb_le` instead. -/
-  dist_iConvexComb_fst_snd_le (f : StdSimplex ℝ (X × X)) :
+  dist_iConvexComb_fst_snd_le [inst₁] [inst₂] (f : StdSimplex ℝ (X × X)) :
     dist (f.iConvexComb Prod.fst) (f.iConvexComb Prod.snd) ≤ f.iConvexComb fun x ↦ dist x.1 x.2
 
 @[deprecated (since := "2026-05-15")] alias IsConvexMetricSpace := IsConvexDist
 
-variable [IsConvexDist X]
+variable [ConvexSpace ℝ X] [MetricSpace X] [IsConvexDist X]
 
 /-- `dist(∑ tᵢ xᵢ, ∑ tᵢ yᵢ) ≤ ∑ tᵢ dist(xᵢ, yᵢ)` -/
 lemma dist_iConvexComb_le {ι : Type*} (f : StdSimplex ℝ ι) (x y : ι → X) :
     dist (f.iConvexComb x) (f.iConvexComb y) ≤ f.iConvexComb fun i ↦ dist (x i) (y i) := by
-  simpa [iConvexComb_map, Function.comp_def]
+  simpa [iConvexComb_map, Finsupp.sum_mapDomain_index, add_mul]
     using IsConvexDist.dist_iConvexComb_fst_snd_le (f.map fun i ↦ (x i, y i))
 
 @[deprecated (since := "2026-05-15")] alias dist_convexCombination_right_le := dist_iConvexComb_le
@@ -257,13 +256,13 @@ lemma continuous_convexCombPair' [BoundedSpace X]
 @[deprecated (since := "2026-05-15")]
 alias continuous_convexComboPair' := continuous_convexCombPair'
 
+variable {R E : Type*} [LinearOrder R] [Field R] [IsStrictOrderedRing R] [AddCommGroup E]
+  [Module R E] [ConvexSpace R E] [IsModuleConvexSpace R E] {S : Set E}
+
 /-- A convex subset of a vector space is a convex space. -/
 -- TODO: this should generalize to arbitrary convex space once `Convex` is redefined.
 @[expose, implicit_reducible]
-noncomputable def ConvexSpace.ofConvex
-    {R E : Type*} [LinearOrder R] [Field R] [IsStrictOrderedRing R]
-      [AddCommGroup E] [Module R E] {S : Set E} (H : Convex R S) :
-    ConvexSpace R S where
+noncomputable def ConvexSpace.ofConvex (H : Convex R S) : ConvexSpace R S where
   sConvexComb f :=
     ⟨sConvexComb (f.map (↑)), by
     simpa [sConvexComb_eq_sum, StdSimplex.map, Finsupp.sum_mapDomain_index, add_smul] using
@@ -273,52 +272,49 @@ noncomputable def ConvexSpace.ofConvex
       StdSimplex.join, Finsupp.sum_sum_index, Finsupp.sum_smul_index, mul_smul, Finsupp.smul_sum]
   sConvexComb_single x := by simp [sConvexComb_eq_sum, ← StdSimplex.mk_single, StdSimplex.map]
 
-lemma isAffineMap_coe {R E : Type*} [LinearOrder R] [Field R] [IsStrictOrderedRing R]
-      [AddCommGroup E] [Module R E] (S : Set E) (H : Convex R S) :
+lemma isAffineMap_coe (S : Set E) (H : Convex R S) :
     letI : ConvexSpace R S := .ofConvex H
     IsAffineMap R ((↑) : S → E) :=
   letI : ConvexSpace R S := .ofConvex H
   ⟨fun _ ↦ rfl⟩
 
 @[simp]
-lemma ConvexSpace.ofConvex.coe_sConvexComb
-      {R E : Type*} [LinearOrder R] [Field R] [IsStrictOrderedRing R]
-      [AddCommGroup E] [Module R E] (S : Set E) (H : Convex R S) (f : StdSimplex R S) :
+lemma ConvexSpace.ofConvex.coe_sConvexComb (S : Set E) (H : Convex R S) (f : StdSimplex R S) :
     letI : ConvexSpace R S := .ofConvex H
     (↑f.sConvexComb : E) = (f.map (↑)).sConvexComb :=
   rfl
 
 @[simp]
-lemma ConvexSpace.ofConvex.coe_iConvexComb
-      {R I E : Type*} [LinearOrder R] [Field R] [IsStrictOrderedRing R]
-      [AddCommGroup E] [Module R E] (S : Set E) (H : Convex R S) (f : StdSimplex R I) (g : I → S) :
+lemma ConvexSpace.ofConvex.coe_iConvexComb (S : Set E) (H : Convex R S) (f : StdSimplex R I)
+     (g : I → S) :
     letI : ConvexSpace R S := .ofConvex H
     (↑(f.iConvexComb g) : E) = f.iConvexComb fun x ↦ ↑(g x) :=
   letI : ConvexSpace R S := .ofConvex H
   (isAffineMap_coe S H).map_iConvexComb f g
 
+attribute [local instance] AddTorsor.toConvexSpace in
 instance (priority := low) {V P : Type*}
     [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] :
     IsConvexDist P where
   dist_iConvexComb_fst_snd_le f := by
     let p : P := Nonempty.some inferInstance
-    simp only [AddTorsor.iConvexComb_eq_affineCombination, ge_iff_le]
+    simp only [AddTorsor.iConvexComb_eq_affineCombination]
     rw [Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _ f.total p,
-      Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _ f.total p,
-      Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _ f.total 0]
+      Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _ f.total p]
     suffices ‖f.weights.sum fun a b ↦ b • (a.1 -ᵥ a.2)‖ ≤
       f.weights.sum fun a b ↦ b * ‖a.1 -ᵥ a.2‖ by
       simpa [dist_eq_norm_vsub, Finsupp.sum, ← Finset.sum_sub_distrib, ← smul_sub]
     grw [Finsupp.sum, Finsupp.sum, norm_sum_le]
     simp [norm_smul, abs_eq_self.mpr (f.nonneg _)]
 
 instance IsConvexDist.of_convex {E : Type*} [NormedAddCommGroup E]
-    [NormedSpace ℝ E] {S : Set E} (H : Convex ℝ S) :
+    [NormedSpace ℝ E] [ConvexSpace ℝ E] [IsModuleConvexSpace ℝ E] [IsConvexDist E] {S : Set E}
+    (H : Convex ℝ S) :
     letI : ConvexSpace ℝ S := .ofConvex H
     IsConvexDist S := by
   letI : ConvexSpace ℝ S := .ofConvex H
   refine ⟨fun f ↦ ?_⟩
   convert dist_iConvexComb_fst_snd_le (X := E) (f.map fun x ↦ (x.1, x.2)) <;>
-    simp [Subtype.dist_eq, iConvexComb_map, Function.comp_def]
+    simp [Subtype.dist_eq, Finsupp.sum_mapDomain_index, add_mul, add_smul]
 
 end Convexity

Mathlib/Data/Finsupp/Defs.lean

@@ -227,17 +227,17 @@ section OnFinset
 variable [Zero M]
 
 /-- The (not exposed) support of `Finsupp.onFinset`. -/
-@[no_expose] def onFinset_support (s : Finset α) (f : α → M) : Finset α :=
+@[no_expose] def onFinsetSupport (s : Finset α) (f : α → M) : Finset α :=
   haveI := Classical.decEq M
   {a ∈ s | f a ≠ 0}
 
 /-- `Finsupp.onFinset s f hf` is the finsupp function representing `f` restricted to the finset `s`.
 The function must be `0` outside of `s`. Use this when the set needs to be filtered anyways,
 otherwise a better set representation is often available. -/
 def onFinset (s : Finset α) (f : α → M) (hf : ∀ a, f a ≠ 0 → a ∈ s) : α →₀ M where
-  support := onFinset_support s f
+  support := onFinsetSupport s f
   toFun := f
-  mem_support_toFun := by simpa [onFinset_support]
+  mem_support_toFun := by simpa [onFinsetSupport]
 
 @[simp, norm_cast] lemma coe_onFinset (s : Finset α) (f : α → M) (hf) : onFinset s f hf = f := rfl
 
@@ -248,7 +248,9 @@ theorem onFinset_apply {s : Finset α} {f : α → M} {hf a} : (onFinset s f hf
 theorem support_onFinset [DecidableEq M] {s : Finset α} {f : α → M}
     (hf : ∀ a : α, f a ≠ 0 → a ∈ s) :
     (Finsupp.onFinset s f hf).support = {a ∈ s | f a ≠ 0} := by
-  dsimp [onFinset]; rw [onFinset_support]; congr
+  dsimp [onFinset]; rw [onFinsetSupport]; congr
+
+@[simp] lemma onFinset_support (f : α →₀ M) : onFinset f.support f (by simp) = f := by ext; simp
 
 @[simp]
 theorem support_onFinset_subset {s : Finset α} {f : α → M} {hf} :

Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean

@@ -16,8 +16,8 @@ This file shows that every affine space is a convex space.
 
 ## Main results
 
-* `AddTorsor.instConvexSpace`: An affine space over a module is a convex space.
-* `AddTorsor.convexCombination_eq_affineCombination`: The convex combination equals the affine
+* `AddTorsor.toConvexSpace`: An affine space over a module is a convex space.
+* `AddTorsor.sConvexComb_eq_affineCombination`: The convex combination equals the affine
   combination.
 * `AddTorsor.convexCombPair_eq_lineMap`: Binary convex combinations are given by `lineMap`.
 -/
@@ -158,33 +158,3 @@ theorem convexCombPair_eq_lineMap (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t)
   simp [vsub_self]
 
 end AddTorsor
-
-open Finsupp
-
-namespace Convexity
-
-attribute [local instance] AddTorsor.toConvexSpace
-
-theorem sConvexComb_eq_sum (f : StdSimplex R V) :
-    f.sConvexComb = f.weights.sum fun i r ↦ r • i := by
-  simp [AddTorsor.sConvexComb_eq_affineCombination,
-    Finset.affineCombination_eq_linear_combination _ _ _ f.total, Finsupp.sum]
-
-@[deprecated (since := "2026-04-03")]
-alias _root_.convexCombination_eq_sum := sConvexComb_eq_sum
-
-theorem iConvexComb_eq_sum (f : StdSimplex R I) (g : I → V) :
-    f.iConvexComb g = f.weights.sum fun i r ↦ r • g i := by
-  simp [iConvexComb, sConvexComb_eq_sum, add_smul, sum_mapDomain_index]
-
-theorem convexCombPair_eq_add
-    {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : V) :
-    convexCombPair s t hs ht h x y = s • x + t • y := by
-  classical
-  simp [convexCombPair, sConvexComb_eq_sum, sum_add_index, add_smul]
-
-variable (R I) in
-lemma StdSimplex.isAffineMap_weights : IsAffineMap R (weights (R := R) (M := I)) where
-  map_sConvexComb s := by simp [sConvexComb_eq_sum, StdSimplex.map, sum_mapDomain_index, add_smul]
-
-end Convexity

Mathlib/Geometry/Convex/ConvexSpace/Defs.lean

@@ -292,19 +292,30 @@ lemma sConvexComb_map (w : StdSimplex R I) (f : I → M) :
 @[simp] lemma iConvexComb_single (i : I) (f : I → M) :
     (single (R := R) i).iConvexComb f = f i := by simp [iConvexComb]
 
-@[simp] lemma iConvexComb_id (s : StdSimplex R M) :
-    s.iConvexComb id = s.sConvexComb := by simp [iConvexComb]
+lemma iConvexComb_id (w : StdSimplex R M) : w.iConvexComb id = w.sConvexComb := by
+  simp [iConvexComb]
 
-@[simp] lemma iConvexComb_id' (s : StdSimplex R M) :
-    s.iConvexComb (fun x ↦ x) = s.sConvexComb := iConvexComb_id s
+@[simp] lemma iConvexComb_id' (w : StdSimplex R M) :
+    w.iConvexComb (fun x ↦ x) = w.sConvexComb := iConvexComb_id _
 
 @[simp] lemma iConvexComb_map (s : StdSimplex R I) (f : I → J) (g : J → M) :
     (s.map f).iConvexComb g = s.iConvexComb (g ∘ f) := by
   simp only [iConvexComb, map_comp]
 
-lemma iConvexComb_congr (s : StdSimplex R I) (f : I ≃ J) (g : I → M) :
+@[congr] lemma iConvexComb_congr {w : StdSimplex R I} {f g : I → M}
+    (hfg : ∀ i, w.weights i ≠ 0 → f i = g i) :
+    w.iConvexComb f = w.iConvexComb g := by
+  refine congr(sConvexComb $(?_))
+  ext i
+  simp only [weights_map]
+  -- TODO: This should just be `congr! 2 with i hi`.
+  congr 1
+  refine Finsupp.mapDomain_congr fun i hi ↦ ?_
+  exact hfg i (by simpa using hi)
+
+lemma iConvexComb_reindex (s : StdSimplex R I) (f : I ≃ J) (g : I → M) :
     s.iConvexComb g = (s.map f).iConvexComb (g ∘ f.symm) := by
-  simp [iConvexComb_map, Function.comp_def]
+  simp [iConvexComb_map]
 
 /-- Flattening nested `iConvexComb`s.
 
@@ -347,7 +358,7 @@ lemma iConvexComb_comm (f : StdSimplex R I) (g : StdSimplex R J)
     (e : I → J → M) :
     f.iConvexComb (fun i ↦ g.iConvexComb (e i)) =
       g.iConvexComb fun j ↦ f.iConvexComb fun i ↦ e i j := by
-  rw [iConvexComb_assoc', iConvexComb_assoc', iConvexComb_congr _ (.prodComm ..)]
+  rw [iConvexComb_assoc', iConvexComb_assoc', iConvexComb_reindex _ (.prodComm ..)]
   congr
   suffices (f.map fun x ↦ g.map (Prod.mk · x)).sConvexComb =
       (g.map (f.map ∘ Prod.mk)).sConvexComb by
@@ -494,7 +505,7 @@ lemma iConvexComb_convexCombPair_comm (f : StdSimplex R I) (e₁ e₂ : I → M)
     f.iConvexComb (fun x ↦ convexCombPair s t hs ht h (e₁ x) (e₂ x)) =
       convexCombPair s t hs ht h (f.iConvexComb e₁) (f.iConvexComb e₂) := by
   simp only [convexCombPair_def]
-  convert (iConvexComb_comm (.duple 0 1 hs ht h) f ![e₁, e₂]).symm with i j j
+  convert (iConvexComb_comm (.duple 0 1 hs ht h) f ![e₁, e₂]).symm with i _ j _ j
   · fin_cases j <;> simp
   · fin_cases j <;> simp
 

Mathlib/Geometry/Convex/ConvexSpace/Module.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2026 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+module
+
+public import Mathlib.Geometry.Convex.ConvexSpace.Prod
+public import Mathlib.LinearAlgebra.AffineSpace.Combination
+public import Mathlib.LinearAlgebra.AffineSpace.AffineMap
+
+/-!
+# Modules are convex spaces
+
+This file shows that every module over ordered coefficients is a convex space.
+
+## Main declarations
+
+* `ConvexSpace.ofModule`: A semimodule space over a semiring is a convex space.
+* `convexSpaceSelf`: A semiring is a convex space over itself.
+* `IsModuleConvexSpace`: Predicate for a convex space and module structures to be compatible.
+-/
+
+public section
+
+namespace Convexity
+variable {R M N I : Type*} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R]
+  [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N]
+
+/-- Any semimodule over an ordered semiring is a convex space.
+
+This is not an instance because it creates a diamond with structural instances such as
+`ConvexSpace R X → ConvexSpace R Y → ConvexSpace R (X × Y)` because
+`(∑ i, f i).fst = ∑ i, (f i).fst` isn't defeq, ultimately because `Finset.sum` isn't a field of
+`AddCommMonoid` but derived from them through recursion. -/
+@[expose, implicit_reducible]
+def ConvexSpace.ofModule : ConvexSpace R M where
+  sConvexComb w := w.weights.sum fun m r ↦ r • m
+  sConvexComb_single := by simp
+  assoc := by
+    simp [Finsupp.sum_mapDomain_index, add_smul, Finsupp.sum_sum_index, Finsupp.sum_smul_index,
+      mul_smul, Finsupp.smul_sum]
+
+instance convexSpaceSelf : ConvexSpace R R := .ofModule
+
+variable (R M) [ConvexSpace R M] in
+/-- Typeclass for a convex space structure on a module to be given by weighted sums. -/
+class IsModuleConvexSpace : Prop where
+  sConvexComb_eq_sum (w : StdSimplex R M) : w.sConvexComb = w.weights.sum fun m r ↦ r • m
+
+export IsModuleConvexSpace (sConvexComb_eq_sum)
+attribute [simp] sConvexComb_eq_sum
+
+@[deprecated (since := "2026-04-03")]
+alias _root_.convexCombination_eq_sum := sConvexComb_eq_sum
+
+attribute [local instance] ConvexSpace.ofModule in
+protected lemma IsModuleConvexSpace.ofModule : IsModuleConvexSpace R M where
+  sConvexComb_eq_sum _ := rfl
+
+instance isModuleConvexSpace_self : IsModuleConvexSpace R R := .ofModule
+
+section IsModuleConvexSpace
+variable [ConvexSpace R M] [IsModuleConvexSpace R M]
+
+/-- `iConvexComb` in a module can be expressed as a sum. -/
+@[simp]
+lemma iConvexComb_eq_sum (w : StdSimplex R I) (f : I → M) :
+    w.iConvexComb f = w.weights.sum fun i r ↦ r • f i := by
+  simp [iConvexComb, sConvexComb_eq_sum, Finsupp.sum_mapDomain_index, add_smul]
+
+/-- `convexCombPair` in a module can be expressed as a sum. -/
+@[simp]
+lemma convexCombPair_eq_sum (a b : R) (ha hb hab) (x y : M) :
+    convexCombPair a b ha hb hab x y = a • x + b • y := by
+  classical simp [convexCombPair, sConvexComb_eq_sum, Finsupp.sum_add_index, add_smul]
+
+instance [ConvexSpace R N] [IsModuleConvexSpace R N] : IsModuleConvexSpace R (M × N) where
+  sConvexComb_eq_sum w := by ext <;> simp [Finsupp.sum, Prod.fst_sum, Prod.snd_sum]
+
+instance {ι : Type*} {M : ι → Type*} [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
+    [∀ i, ConvexSpace R (M i)] [∀ i, IsModuleConvexSpace R (M i)] :
+    IsModuleConvexSpace R (∀ i, M i) where
+  sConvexComb_eq_sum w := by ext; simp [Finsupp.sum]
+
+instance {ι : Type*} : IsModuleConvexSpace R (ι →₀ M) where
+  sConvexComb_eq_sum w := by ext; simp [Finsupp.sum]
+
+end IsModuleConvexSpace
+
+variable (R I) in
+lemma StdSimplex.isAffineMap_weights : IsAffineMap R (weights (R := R) (M := I)) where
+  map_sConvexComb s := by simp [sConvexComb_eq_sum, Finsupp.sum_mapDomain_index, add_smul]
+
+end Convexity