Tensor Products of Pointed Cones

This file proves that the minimal and maximal tensor products of pointed cones in finite-dimensional real vector spaces are equal when one cone is simplicial and generating and the other is proper (pointed and closed).

Finite-dimensionality of the proper cone ambient space is by explicit declaration and is required for the topDualPairing_isContPerfPair instance (in Topology.Algebra.Module.TopDualPairing). The simplicial and generating cone ambient space is implicitly finite dimensional by the simplicial and generating assumption.

This file uses topDualPairing (the canonical pairing of a vector space and its topological dual) to avoid explicit topology assumptions on Module.Dual.

The proof relies on the following result:

• Bipolar theorem (ProperCone.dual_dual_flip): The double dual of a proper cone is itself.

This requires:

• Local convexity and Hausdorff separation (for Hahn-Banach)
• A continuous perfect pairing between the module and its dual.

Main results

• PointedCone.minTensorProduct_eq_max_of_simplicial_generating_left: If C₁ is simplicial and generating and C₂ is proper, then the minimal and maximal tensor products are equal.

• PointedCone.minTensorProduct_eq_max_of_simplicial_generating_right: If C₁ is a proper cone and C₂ is a simplicial and generating cone, then their minimal and maximal tensor products are equal.

References

• Aubrun et al. Entangleability of cones

Equality of minimal and maximal tensor products

theorem PointedCone.basis_coord_mem_dual {R : Type u_1} {M : Type u_2} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {ι : Type u_3} (b : Module.Basis ι R M) (C : PointedCone R M) (hC : ↑C ⊆ ↑(hull R (Set.range ⇑b))) (i : ι) : b.coord i ∈ dual (Module.dualPairing R M).flip ↑C

If a pointed cone C is contained in the conic hull of a basis b, then the coordinate functionals of b lie in the dual cone of C.

theorem PointedCone.minTensorProduct_eq_max_of_simplicial_generating_left {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [T2Space F] [FiniteDimensional ℝ F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] (C₁ : PointedCone ℝ E) (C₂ : ProperCone ℝ F) (h₁_simp : C₁.IsSimplicial) (h₁_gen : Submodule.span ℝ ↑C₁ = ⊤) : C₁.minTensorProduct ↑C₂ = C₁.maxTensorProduct ↑C₂

If C₁ is a simplicial and generating cone and C₂ is a proper cone, then their minimal and maximal tensor products are equal.

theorem PointedCone.minTensorProduct_eq_max_of_simplicial_generating_right {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [T2Space F] [FiniteDimensional ℝ F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] (C₁ : ProperCone ℝ F) (C₂ : PointedCone ℝ E) (h₂_simp : C₂.IsSimplicial) (h₂_gen : Submodule.span ℝ ↑C₂ = ⊤) : (↑C₁).minTensorProduct C₂ = (↑C₁).maxTensorProduct C₂

If C₁ is a proper cone and C₂ is a simplicial and generating cone, then their minimal and maximal tensor products are equal.