Salience of images and products of cones, and the line spanned by a ray

Mathlib's ConvexCone.Salient records that a convex cone contains no line. This file proves the two closure properties of salience that concern standard cone constructions, the image under an injective linear map and the product of two pointed cones, together with the salience of the cone hull of a single vector. It also computes the dimension of the linear span of the cone hull of a single nonzero vector, which is the one-dimensionality making such a cone a ray, and the invariance of that dimension under multiplying a cone by the zero cone. None of these statements involves a lattice, so they belong to the generic convex-cone API rather than to any consumer of it.

Main declarations

• ConvexCone.Salient.map: the image of a salient convex cone under an injective linear map is salient.
• ConvexCone.Salient.prod: a product of salient pointed cones is salient.
• PointedCone.salient_hull_singleton: the cone hull of a single vector is salient.
• PointedCone.finrank_span_coe_hull_singleton: the cone hull of a nonzero vector spans a line.
• PointedCone.finrank_span_coe_prod_bot and PointedCone.finrank_span_coe_bot_prod: multiplying a pointed cone by the zero cone leaves the dimension of the span of the cone unchanged.

theorem ConvexCone.Salient.map {R : Type u_1} {V : Type u_2} {V' : Type u_3} [Semiring R] [PartialOrder R] [AddCommGroup V] [AddCommGroup V'] [Module R V] [Module R V'] {C : ConvexCone R V} {g : V →ₗ[R] V'} (hC : C.Salient) (hg : Function.Injective ⇑g) : (ConvexCone.map g C).Salient

The image of a salient convex cone under an injective linear map is salient.

theorem ConvexCone.Salient.prod {R : Type u_1} {V : Type u_2} {V' : Type u_3} [Semiring R] [PartialOrder R] [AddCommGroup V] [AddCommGroup V'] [Module R V] [Module R V'] [IsOrderedRing R] {σ : PointedCone R V} {τ : PointedCone R V'} (hσ : (↑σ).Salient) (hτ : (↑τ).Salient) : (↑(Submodule.prod σ τ)).Salient

A product of salient pointed cones is salient.

theorem PointedCone.salient_hull_singleton {R : Type u_1} {V : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [NoZeroSMulDivisors R V] (x : V) : (↑(R ∙₊ x)).Salient

The cone hull of a single vector is salient.

theorem PointedCone.finrank_span_coe_hull_singleton {R : Type u_1} {V : Type u_2} [DivisionRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] {x : V} (hx : x ≠ 0) : Module.finrank R ↥(Submodule.span R ↑(R ∙₊ x)) = 1

The linear span of the cone hull of a nonzero vector is the line it spans, of dimension one. Passing from the cone hull to the linear span extends scalars from the nonnegative elements of the ordered division ring to the ring itself.

theorem PointedCone.finrank_span_coe_prod_bot {R : Type u_1} {V : Type u_2} {V' : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid V] [Module R V] [AddCommMonoid V'] [Module R V'] (p : PointedCone R V) : Module.finrank R ↥(Submodule.span R ↑(Submodule.prod p ⊥)) = Module.finrank R ↥(Submodule.span R ↑p)

Multiplying a pointed cone by the zero cone in the second factor leaves the dimension of its span unchanged. In particular, a ray of the first factor remains one-dimensional in the product.

theorem PointedCone.finrank_span_coe_bot_prod {R : Type u_1} {V : Type u_2} {V' : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid V] [Module R V] [AddCommMonoid V'] [Module R V'] (q : PointedCone R V') : Module.finrank R ↥(Submodule.span R ↑(Submodule.prod ⊥ q)) = Module.finrank R ↥(Submodule.span R ↑q)

Multiplying a pointed cone by the zero cone in the first factor leaves the dimension of its span unchanged. In particular, a ray of the second factor remains one-dimensional in the product.

theorem LinearMap.mapsTo_bot_pointedCone {R : Type u_1} {V : Type u_2} {V' : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid V] [Module R V] [AddCommMonoid V'] [Module R V'] (g : V →ₗ[R] V') : Set.MapsTo ⇑g ↑⊥ ↑⊥

A linear map sends the zero cone to the zero cone.