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.
Instances For
@[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.
Instances For
@[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)
@[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]
:
Coercion from submodules to pointed cones as an order embedding.
Instances For
@[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.
Instances For
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.
Instances For
@[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)
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
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.
Instances For
@[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.instCanLiftConvexConeToConvexConePointed
{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.
Instances For
@[simp]
theorem
PointedCone.coe_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)
:
↑(ofConeComb C nonempty coneComb) = C
@[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.
Instances For
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}
:
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}
:
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.
Instances For
@[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)
:
@[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)
:
@[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.
Instances For
@[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)
:
@[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)
:
@[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.
Instances For
@[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}
:
@[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.
Instances For
@[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)
:
@[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)
:
@[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}
:
@[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]
:
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)
:
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)
:
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)
:
A pointed cone is salient iff the intersection of the cone with its negative
is the set {0}.