Pointed cones

A pointed cone is defined to be a submodule of a module where the scalars are restricted to be nonnegative. This is equivalent to saying that, as a set, a pointed cone is a convex cone which contains 0. This is a bundled version of ConvexCone.Pointed. We choose the submodule definition as it allows us to use the Module API to work with convex cones.

@[reducible, inline]

abbrev PointedCone (R : Type u_5) (E : Type u_6) [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] : Type u_6

A pointed cone is a submodule of a module with scalars restricted to being nonnegative.

Equations

• PointedCone R E = Submodule { c : R // 0 ≤ c } E

@[reducible, inline]

abbrev PointedCone.ofSubmodule {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] (S : Submodule R E) : PointedCone R E

A submodule is a pointed cone.

Equations

• ↑S = Submodule.restrictScalars { c : R // 0 ≤ c } S

@[implicit_reducible]

instance PointedCone.instCoeSubmodule {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] : Coe (Submodule R E) (PointedCone R E)

Equations

• PointedCone.instCoeSubmodule = { coe := PointedCone.ofSubmodule }

@[simp]

theorem PointedCone.coe_ofSubmodule {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] (S : Submodule R E) : ↑↑S = ↑S

theorem PointedCone.mem_ofSubmodule_iff {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] {S : Submodule R E} {x : E} : x ∈ ↑S ↔ x ∈ S

theorem PointedCone.ofSubmodule_inj {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] {S T : Submodule R E} : ↑S = ↑T ↔ S = T

@[reducible, inline]

abbrev PointedCone.ofSubmoduleEmbedding {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] : Submodule R E ↪o PointedCone R E

Coercion from submodules to pointed cones as an order embedding.

Equations

• PointedCone.ofSubmoduleEmbedding = Submodule.restrictScalarsEmbedding { c : R // 0 ≤ c } R E

@[reducible, inline]

abbrev PointedCone.ofSubmoduleLatticeHom {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] : CompleteLatticeHom (Submodule R E) (PointedCone R E)

Coercion from submodules to pointed cones as a lattice homomorphism.

Equations

• PointedCone.ofSubmoduleLatticeHom = Submodule.restrictScalarsLatticeHom { c : R // 0 ≤ c } R E

theorem PointedCone.ofSubmodule_inf {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] (S T : Submodule R E) : ↑(S ⊓ T) = ↑S ⊓ ↑T

theorem PointedCone.ofSubmodule_sup {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] (S T : Submodule R E) : ↑(S ⊔ T) = ↑S ⊔ ↑T

theorem PointedCone.ofSubmodule_sInf {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] (s : Set (Submodule R E)) : ↑(sInf s) = sInf (ofSubmodule '' s)

theorem PointedCone.ofSubmodule_iInf {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] (s : Set (Submodule R E)) : ↑(⨅ S ∈ s, S) = ⨅ S ∈ s, ↑S

theorem PointedCone.ofSubmodule_sSup {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] (s : Set (Submodule R E)) : ↑(sSup s) = sSup (ofSubmodule '' s)

theorem PointedCone.ofSubmodule_iSup {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] (s : Set (Submodule R E)) : ↑(⨆ S ∈ s, S) = ⨆ S ∈ s, ↑S

def PointedCone.toConvexCone {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] (C : PointedCone R E) : ConvexCone R E

Every pointed cone is a convex cone.

Equations

• ↑C = { carrier := ↑C, smul_mem' := ⋯, add_mem' := ⋯ }

@[implicit_reducible]

instance PointedCone.instCoeConvexCone {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] : Coe (PointedCone R E) (ConvexCone R E)

Equations

• PointedCone.instCoeConvexCone = { coe := PointedCone.toConvexCone }

theorem PointedCone.toConvexCone_injective {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] : Function.Injective toConvexCone

@[simp]

theorem PointedCone.pointed_toConvexCone {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] (C : PointedCone R E) : (↑C).Pointed

@[simp]

theorem PointedCone.mem_toConvexCone {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] {C : PointedCone R E} {x : E} : x ∈ ↑C ↔ x ∈ C

theorem PointedCone.ext {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] {C₁ C₂ : PointedCone R E} (h : ∀ (x : E), x ∈ C₁ ↔ x ∈ C₂) : C₁ = C₂

theorem PointedCone.ext_iff {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] {C₁ C₂ : PointedCone R E} : C₁ = C₂ ↔ ∀ (x : E), x ∈ C₁ ↔ x ∈ C₂

theorem PointedCone.convex {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] (C : PointedCone R E) : Convex R ↑C

@[implicit_reducible]

instance PointedCone.instZero {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] (C : PointedCone R E) : Zero ↥C

Equations

• C.instZero = { zero := ⟨0, ⋯⟩ }

theorem PointedCone.smul_mem {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] {x : E} {r : R} (C : PointedCone R E) (hr : 0 ≤ r) (hx : x ∈ C) : r • x ∈ C

def ConvexCone.toPointedCone {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] (C : ConvexCone R E) (hC : C.Pointed) : PointedCone R E

The PointedCone constructed from a pointed ConvexCone.

Equations

• C.toPointedCone hC = { carrier := ↑C, add_mem' := ⋯, zero_mem' := hC, smul_mem' := ⋯ }

@[simp]

theorem ConvexCone.mem_toPointedCone {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] {C : ConvexCone R E} (hC : C.Pointed) (x : E) : x ∈ C.toPointedCone hC ↔ x ∈ C

@[simp]

theorem ConvexCone.coe_toPointedCone {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] (C : ConvexCone R E) (hC : C.Pointed) : ↑(C.toPointedCone hC) = C

@[simp]

theorem ConvexCone.toPointedCone_top {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] : ⊤.toPointedCone trivial = ⊤

instance PointedCone.canLift {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] : CanLift (ConvexCone R E) (PointedCone R E) toConvexCone ConvexCone.Pointed

def PointedCone.ofConeComb {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] (C : Set E) (nonempty : C.Nonempty) (coneComb : ∀ x ∈ C, ∀ y ∈ C, ∀ (a : R), 0 ≤ a → ∀ (b : R), 0 ≤ b → a • x + b • y ∈ C) : PointedCone R E

Construct a pointed cone from closure under two-element conical combinations. I.e., a nonempty set closed under two-element conical combinations is a pointed cone.

Equations

• PointedCone.ofConeComb C nonempty coneComb = Submodule.ofLinearComb C nonempty ⋯

@[reducible, inline]

abbrev PointedCone.hull (R : Type u_1) {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] (s : Set E) : PointedCone R E

The cone hull of a set s is the smallest pointed cone that contains s.

Pointed cones being defined as submodules over nonnegative scalars, this is implemented as the submodule span of s w.r.t. nonnegative scalars.

Equations

• PointedCone.hull R s = Submodule.span { c : R // 0 ≤ c } s

theorem PointedCone.subset_hull {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] {s : Set E} : s ⊆ ↑(hull R s)

@[deprecated PointedCone.subset_hull "`PointedCone.span` was renamed to `PointedCone.hull`" (since := "2026-03-22")]

theorem PointedCone.subset_span {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] {s : Set E} : s ⊆ ↑(hull R s)

Alias of PointedCone.subset_hull.

theorem PointedCone.mem_hull_set {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] {x : E} {s : Set E} : x ∈ hull R s ↔ ∃ (c : E →₀ R), ↑c.support ⊆ s ∧ (∀ (y : E), 0 ≤ c y) ∧ (c.sum fun (m : E) (r : R) => r • m) = x

Elements of the cone hull are expressible as conical combination of elements from s.

@[deprecated PointedCone.mem_hull_set "`PointedCone.span` was renamed to `PointedCone.hull`" (since := "2026-03-22")]

theorem PointedCone.mem_span_set {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] {x : E} {s : Set E} : x ∈ hull R s ↔ ∃ (c : E →₀ R), ↑c.support ⊆ s ∧ (∀ (y : E), 0 ≤ c y) ∧ (c.sum fun (m : E) (r : R) => r • m) = x

Alias of PointedCone.mem_hull_set.

---

Elements of the cone hull are expressible as conical combination of elements from s.

Maps between pointed cones

There is already a definition of maps between submodules, Submodule.map. In our case, these maps are induced from linear maps between the ambient modules that are linear over nonnegative scalars. Such maps are unlikely to be of any use in practice. So, we construct some API to define maps between pointed cones induced from linear maps between the ambient modules that are linear over all scalars.

def PointedCone.map {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] (f : E →ₗ[R] F) (C : PointedCone R E) : PointedCone R F

The image of a pointed cone under an R-linear map is a pointed cone.

Equations

• PointedCone.map f C = Submodule.map (↑{ c : R // 0 ≤ c } f) C

@[simp]

theorem PointedCone.toConvexCone_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] (C : PointedCone R E) (f : E →ₗ[R] F) : ↑(map f C) = ConvexCone.map f ↑C

@[simp]

theorem PointedCone.coe_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] (C : PointedCone R E) (f : E →ₗ[R] F) : ↑(map f C) = ⇑f '' ↑C

@[simp]

theorem PointedCone.mem_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] {f : E →ₗ[R] F} {C : PointedCone R E} {y : F} : y ∈ map f C ↔ ∃ x ∈ C, f x = y

theorem PointedCone.map_map {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] [AddCommMonoid G] [Module R G] (g : F →ₗ[R] G) (f : E →ₗ[R] F) (C : PointedCone R E) : map g (map f C) = map (g ∘ₗ f) C

@[simp]

theorem PointedCone.map_id {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] (C : PointedCone R E) : map LinearMap.id C = C

def PointedCone.comap {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] (f : E →ₗ[R] F) (C : PointedCone R F) : PointedCone R E

The preimage of a pointed cone under an R-linear map is a pointed cone.

Equations

• PointedCone.comap f C = Submodule.comap (↑{ c : R // 0 ≤ c } f) C

@[simp]

theorem PointedCone.coe_comap {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] (f : E →ₗ[R] F) (C : PointedCone R F) : ↑(comap f C) = ⇑f ⁻¹' ↑C

@[simp]

theorem PointedCone.comap_id {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] (C : PointedCone R E) : comap LinearMap.id C = C

theorem PointedCone.comap_comap {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] [AddCommMonoid G] [Module R G] (g : F →ₗ[R] G) (f : E →ₗ[R] F) (C : PointedCone R G) : comap f (comap g C) = comap (g ∘ₗ f) C

@[simp]

theorem PointedCone.mem_comap {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] {f : E →ₗ[R] F} {C : PointedCone R F} {x : E} : x ∈ comap f C ↔ f x ∈ C

def PointedCone.positive (R : Type u_1) (E : Type u_2) [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [PartialOrder E] [IsOrderedAddMonoid E] [Module R E] [PosSMulMono R E] : PointedCone R E

The positive cone is the pointed cone formed by the set of nonnegative elements in an ordered module.

Equations

• PointedCone.positive R E = (ConvexCone.positive R E).toPointedCone ⋯

@[simp]

theorem PointedCone.mem_positive (R : Type u_1) (E : Type u_2) [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [PartialOrder E] [IsOrderedAddMonoid E] [Module R E] [PosSMulMono R E] {x : E} : x ∈ positive R E ↔ 0 ≤ x

@[simp]

theorem PointedCone.toConvexCone_positive (R : Type u_1) (E : Type u_2) [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [PartialOrder E] [IsOrderedAddMonoid E] [Module R E] [PosSMulMono R E] : ↑(positive R E) = ConvexCone.positive R E

theorem PointedCone.to_isOrderedModule {R : Type u_1} {E : Type u_2} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module R E] (C : PointedCone R E) (h : ∀ (x y : E), x ≤ y ↔ y - x ∈ C) : IsOrderedModule R E

Constructs an ordered module given an ordered group, a cone, and a proof that the order relation is the one defined by the cone.

def PointedCone.lineal {R : Type u_1} {E : Type u_2} [Ring R] [LinearOrder R] [IsOrderedRing R] [AddCommGroup E] [Module R E] (C : PointedCone R E) : Submodule R E

The lineality space of a cone C is the submodule given by C ⊓ -C.

Equations

• C.lineal = { toAddSubmonoid := C.support.toAddSubmonoid, smul_mem' := ⋯ }

@[simp]

theorem PointedCone.coe_lineal {R : Type u_1} {E : Type u_2} [Ring R] [LinearOrder R] [IsOrderedRing R] [AddCommGroup E] [Module R E] (C : PointedCone R E) : ↑C.lineal = ↑C ∩ -↑C

@[simp]

theorem PointedCone.ofSubmodule_lineal {R : Type u_1} {E : Type u_2} [Ring R] [LinearOrder R] [IsOrderedRing R] [AddCommGroup E] [Module R E] (C : PointedCone R E) : ↑C.lineal = C ⊓ -C

@[simp]

theorem PointedCone.mem_lineal {R : Type u_1} {E : Type u_2} [Ring R] [LinearOrder R] [IsOrderedRing R] [AddCommGroup E] [Module R E] {C : PointedCone R E} {x : E} : x ∈ C.lineal ↔ x ∈ C ∧ -x ∈ C

@[simp]

theorem PointedCone.support_eq {R : Type u_1} {E : Type u_2} [Ring R] [LinearOrder R] [IsOrderedRing R] [AddCommGroup E] [Module R E] {C : PointedCone R E} : C.support = C.lineal.toAddSubgroup

theorem PointedCone.gc_ofSubmodule_lineal {R : Type u_1} {E : Type u_2} [Ring R] [LinearOrder R] [IsOrderedRing R] [AddCommGroup E] [Module R E] : GaloisConnection ofSubmodule lineal

The lineality space of a cone is the largest submodule contained in the cone.

theorem PointedCone.lineal_le {R : Type u_1} {E : Type u_2} [Ring R] [LinearOrder R] [IsOrderedRing R] [AddCommGroup E] [Module R E] (C : PointedCone R E) : ↑C.lineal ≤ C

theorem PointedCone.lineal_eq_sSup {R : Type u_1} {E : Type u_2} [Ring R] [LinearOrder R] [IsOrderedRing R] [AddCommGroup E] [Module R E] (C : PointedCone R E) : C.lineal = sSup {S : Submodule R E | ↑S ≤ C}

theorem PointedCone.salient_iff_inter_neg_eq_singleton {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup E] [Module R E] (C : PointedCone R E) : (↑C).Salient ↔ ↑C ∩ -↑C = {0}

A pointed cone is salient iff the intersection of the cone with its negative is the set {0}.