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.

@[implicit_reducible]

def Convexity.ConvexSpace.ofModule {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] : ConvexSpace R M

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.

Equations

• Convexity.ConvexSpace.ofModule = { sConvexComb := fun (w : Convexity.StdSimplex R M) => w.weights.sum fun (m : M) (r : R) => r • m, sConvexComb_single := ⋯, assoc := ⋯ }

@[implicit_reducible]

instance Convexity.convexSpaceSelf {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : ConvexSpace R R

Equations

• Convexity.convexSpaceSelf = Convexity.ConvexSpace.ofModule

class Convexity.IsModuleConvexSpace (R : Type u_2) (M : Type u_3) [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [ConvexSpace R M] : Prop

Typeclass for a convex space structure on a module to be given by weighted sums.

• sConvexComb_eq_sum (w : StdSimplex R M) : sConvexComb w = w.weights.sum fun (m : M) (r : R) => r • m

@[deprecated Convexity.IsModuleConvexSpace.sConvexComb_eq_sum (since := "2026-04-03")]

theorem convexCombination_eq_sum {R : Type u_2} {M : Type u_3} {inst✝ : Semiring R} {inst✝¹ : PartialOrder R} {inst✝² : IsStrictOrderedRing R} {inst✝³ : AddCommMonoid M} {inst✝⁴ : Module R M} {inst✝⁵ : Convexity.ConvexSpace R M} [self : Convexity.IsModuleConvexSpace R M] (w : Convexity.StdSimplex R M) : Convexity.sConvexComb w = w.weights.sum fun (m : M) (r : R) => r • m

Alias of Convexity.IsModuleConvexSpace.sConvexComb_eq_sum.

theorem Convexity.IsModuleConvexSpace.ofModule {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] : IsModuleConvexSpace R M

instance Convexity.isModuleConvexSpace_self {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : IsModuleConvexSpace R R

@[simp]

theorem Convexity.iConvexComb_eq_sum {R : Type u_2} {M : Type u_3} {I : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [ConvexSpace R M] [IsModuleConvexSpace R M] (w : StdSimplex R I) (f : I → M) : iConvexComb w f = w.weights.sum fun (i : I) (r : R) => r • f i

iConvexComb in a module can be expressed as a sum.

@[simp]

theorem Convexity.convexCombPair_eq_sum {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [ConvexSpace R M] [IsModuleConvexSpace R M] (a b : R) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (x y : M) : convexCombPair a b ha hb hab x y = a • x + b • y

convexCombPair in a module can be expressed as a sum.

theorem Convexity.IsAffineMap.map_sum_weights {R : Type u_2} {M : Type u_3} {N : Type u_4} {I : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M → N} [ConvexSpace R M] [IsModuleConvexSpace R M] [ConvexSpace R N] [IsModuleConvexSpace R N] (hf : IsAffineMap R f) (w : StdSimplex R I) (g : I → M) : f (w.weights.sum fun (i : I) (r : R) => r • g i) = w.weights.sum fun (i : I) (r : R) => r • f (g i)

theorem Convexity.IsAffineMap.map_smul_add_smul {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M → N} [ConvexSpace R M] [IsModuleConvexSpace R M] [ConvexSpace R N] [IsModuleConvexSpace R N] {a b : R} (hf : IsAffineMap R f) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (x y : M) : f (a • x + b • y) = a • f x + b • f y

@[simp]

theorem Convexity.isConvexSet_coe {F : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [SetLike F M] [AddSubmonoidClass F M] [SMulMemClass F R M] [ConvexSpace R M] [IsModuleConvexSpace R M] (S : F) : IsConvexSet R ↑S

@[implicit_reducible]

noncomputable instance Convexity.instConvexSpaceSubtypeMem {F : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [SetLike F M] [AddSubmonoidClass F M] [SMulMemClass F R M] [ConvexSpace R M] [IsModuleConvexSpace R M] (S : F) : ConvexSpace R ↥S

Equations

• Convexity.instConvexSpaceSubtypeMem S = Convexity.ConvexSpace.subtype ↑S ⋯

@[simp]

theorem Convexity.subtypeVal_submodule_sConvexComb {F : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [SetLike F M] [AddSubmonoidClass F M] [SMulMemClass F R M] [ConvexSpace R M] [IsModuleConvexSpace R M] (S : F) (w : StdSimplex R ↥S) : ↑(sConvexComb w) = iConvexComb w Subtype.val

theorem Convexity.subtypeVal_submodule_iConvexComb {F : Type u_1} {R : Type u_2} {M : Type u_3} {I : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [SetLike F M] [AddSubmonoidClass F M] [SMulMemClass F R M] [ConvexSpace R M] [IsModuleConvexSpace R M] (S : F) (w : StdSimplex R I) (f : I → ↥S) : ↑(iConvexComb w f) = iConvexComb w fun (i : I) => ↑(f i)

theorem Convexity.subtypeVal_submodule_convexCombPair {F : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [SetLike F M] [AddSubmonoidClass F M] [SMulMemClass F R M] [ConvexSpace R M] [IsModuleConvexSpace R M] (S : F) (a b : R) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (x y : ↥S) : ↑(convexCombPair a b ha hb hab x y) = convexCombPair a b ha hb hab ↑x ↑y

instance Convexity.instIsModuleConvexSpaceSubtypeMem {F : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [SetLike F M] [AddSubmonoidClass F M] [SMulMemClass F R M] [ConvexSpace R M] [IsModuleConvexSpace R M] (S : F) : IsModuleConvexSpace R ↥S

instance Convexity.instIsModuleConvexSpaceProd {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [ConvexSpace R M] [IsModuleConvexSpace R M] [ConvexSpace R N] [IsModuleConvexSpace R N] : IsModuleConvexSpace R (M × N)

instance Convexity.instIsModuleConvexSpaceForall {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_6} {M : ι → Type u_7} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → ConvexSpace R (M i)] [∀ (i : ι), IsModuleConvexSpace R (M i)] : IsModuleConvexSpace R ((i : ι) → M i)

instance Convexity.instIsModuleConvexSpaceFinsupp {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [ConvexSpace R M] [IsModuleConvexSpace R M] {ι : Type u_6} : IsModuleConvexSpace R (ι →₀ M)

theorem Convexity.IsAffineMap.add {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f g : M → N} [ConvexSpace R M] [IsModuleConvexSpace R M] [ConvexSpace R N] [IsModuleConvexSpace R N] (hf : IsAffineMap R f) (hg : IsAffineMap R g) : IsAffineMap R (f + g)

theorem Convexity.IsAffineMap.fun_add {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f g : M → N} [ConvexSpace R M] [IsModuleConvexSpace R M] [ConvexSpace R N] [IsModuleConvexSpace R N] (hf : IsAffineMap R f) (hg : IsAffineMap R g) : IsAffineMap R fun (i : M) => f i + g i

Eta-expanded form of Convexity.IsAffineMap.add

theorem Convexity.IsStarConvexSet.add {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [ConvexSpace R M] [IsModuleConvexSpace R M] {x y : M} {s t : Set M} (hs : IsStarConvexSet R x s) (ht : IsStarConvexSet R y t) : IsStarConvexSet R (x + y) (s + t)

theorem Convexity.StdSimplex.isAffineMap_weights (R : Type u_2) (I : Type u_5) [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : IsAffineMap R weights

theorem Convexity.IsAffineMap.neg {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [ConvexSpace R M] [IsModuleConvexSpace R M] [ConvexSpace R N] [IsModuleConvexSpace R N] {f : M → N} (hf : IsAffineMap R f) : IsAffineMap R (-f)

theorem Convexity.IsAffineMap.fun_neg {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [ConvexSpace R M] [IsModuleConvexSpace R M] [ConvexSpace R N] [IsModuleConvexSpace R N] {f : M → N} (hf : IsAffineMap R f) : IsAffineMap R fun (i : M) => -f i

Eta-expanded form of Convexity.IsAffineMap.neg

theorem Convexity.IsAffineMap.sub {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [ConvexSpace R M] [IsModuleConvexSpace R M] [ConvexSpace R N] [IsModuleConvexSpace R N] {f g : M → N} (hf : IsAffineMap R f) (hg : IsAffineMap R g) : IsAffineMap R (f - g)

theorem Convexity.IsAffineMap.fun_sub {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [ConvexSpace R M] [IsModuleConvexSpace R M] [ConvexSpace R N] [IsModuleConvexSpace R N] {f g : M → N} (hf : IsAffineMap R f) (hg : IsAffineMap R g) : IsAffineMap R fun (i : M) => f i - g i

Eta-expanded form of Convexity.IsAffineMap.sub

theorem Convexity.IsStarConvexSet.neg {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] [ConvexSpace R M] [IsModuleConvexSpace R M] {x : M} {s : Set M} (hs : IsStarConvexSet R x s) : IsStarConvexSet R (-x) (-s)

theorem Convexity.IsStarConvexSet.sub {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] [ConvexSpace R M] [IsModuleConvexSpace R M] {x y : M} {s t : Set M} (hs : IsStarConvexSet R x s) (ht : IsStarConvexSet R y t) : IsStarConvexSet R (x - y) (s - t)