feat(Geometry/Convex): modules are convex spaces

Author: YaelDillies

Mathlib.lean

@@ -4511,6 +4511,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/Data/Finsupp/Defs.lean

@@ -234,17 +234,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
 
@@ -255,7 +255,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

@@ -302,9 +302,20 @@ lemma sConvexComb_map (w : StdSimplex R I) (f : I → 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,98 @@
+/-
+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 semimodule over an ordered semiring 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.
+
+## Implementation notes
+
+It is sadly impossible to make `ConvexSpace.ofModule` 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`.
+-/
+
+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. -/
+@[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
+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

Mathlib/Geometry/Convex/ConvexSpace/Prod.lean

@@ -49,6 +49,16 @@ lemma snd_iConvexComb (w : StdSimplex R I) (f : I → X × Y) :
     (w.iConvexComb f).snd = w.iConvexComb (fun i ↦ (f i).snd) :=
   isAffineMap_snd.map_iConvexComb ..
 
+@[simp]
+lemma fst_convexCombPair (a b : R) (ha hb hab) (x y : X × Y) :
+    (convexCombPair a b ha hb hab x y).fst = convexCombPair a b ha hb hab x.fst y.fst :=
+  isAffineMap_fst.map_convexCombPair ..
+
+@[simp]
+lemma snd_convexCombPair (a b : R) (ha hb hab) (x y : X × Y) :
+    (convexCombPair a b ha hb hab x y).snd = convexCombPair a b ha hb hab x.snd y.snd :=
+  isAffineMap_snd.map_convexCombPair ..
+
 end Prod
 
 namespace Pi
@@ -57,7 +67,7 @@ variable {ι : Type*} {X : ι → Type*} [∀ i, ConvexSpace R (X i)] {i : ι}
 instance : ConvexSpace R (∀ i, X i) := .mk
   (fun w i ↦ w.iConvexComb (· i))
   (by simp)
-  (by simp [Function.comp_def, iConvexComb_assoc])
+  (by simp [iConvexComb_assoc])
 
 @[simp]
 lemma sConvexComb_apply (w : StdSimplex R (∀ i, X i)) (i : ι) :
@@ -71,4 +81,41 @@ lemma isAffineMap_eval : IsAffineMap R (· i : (∀ i, X i) → X i) where
 lemma iConvexComb_apply (w : StdSimplex R I) (f : I → ∀ i, X i) (i : ι) :
     w.iConvexComb f i = w.iConvexComb (fun j ↦ f j i) := isAffineMap_eval.map_iConvexComb ..
 
+@[simp]
+lemma convexCombPair_apply (a b : R) (ha hb hab) (f g : ∀ i, X i) (i : ι) :
+    convexCombPair a b ha hb hab f g i = convexCombPair a b ha hb hab (f i) (g i) :=
+  isAffineMap_eval.map_convexCombPair ..
+
 end Pi
+
+namespace Finsupp
+variable {ι : Type*} {X : Type*} [Zero X] [ConvexSpace R X] {i : ι}
+
+instance : ConvexSpace R (ι →₀ X) := .mk
+  (fun w ↦ by
+    classical
+    refine .onFinset (w.weights.support.biUnion Finsupp.support) (fun i ↦ w.iConvexComb (· i)) ?_
+    rintro i hi
+    contrapose! hi
+    simp_all)
+  (by simp)
+  (fun w ↦ by ext; simp [iConvexComb_assoc])
+
+@[simp]
+lemma sConvexComb_apply (w : StdSimplex R (ι →₀ X)) (i : ι) :
+    w.sConvexComb i = w.iConvexComb (· i) := rfl
+
+@[fun_prop]
+lemma isAffineMap_eval : IsAffineMap R (· i : (ι →₀ X) → X) where
+  map_sConvexComb _ := sConvexComb_apply ..
+
+@[simp]
+lemma iConvexComb_apply (w : StdSimplex R I) (f : I → ι →₀ X) (i : ι) :
+    w.iConvexComb f i = w.iConvexComb (fun j ↦ f j i) := isAffineMap_eval.map_iConvexComb ..
+
+@[simp]
+lemma convexCombPair_apply (a b : R) (ha hb hab) (f g : ι →₀ X) (i : ι) :
+    convexCombPair a b ha hb hab f g i = convexCombPair a b ha hb hab (f i) (g i) :=
+  isAffineMap_eval.map_convexCombPair ..
+
+end Finsupp