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 := ⋯ }
Instances For
@[implicit_reducible]
instance
Convexity.convexSpaceSelf
{R : Type u_2}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
:
ConvexSpace R R
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]
:
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
Instances
@[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)
:
theorem
Convexity.IsModuleConvexSpace.ofModule
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[AddCommMonoid M]
[Module R M]
:
instance
Convexity.isModuleConvexSpace_self
{R : Type u_2}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing 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 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 in a module can be expressed as a sum.
@[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
@[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)
:
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)
:
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)
:
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.StdSimplex.isAffineMap_weights
(R : Type u_2)
(I : Type u_5)
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
: