Tensor products of cones

Given ordered modules M and N, there are in general several distinct possible orderings of the tensor product module M ⊗ N. Since the ordering of an ordered module can be represented by its cone of nonnegative elements, there are likewise multiple ways to construct a cone in M ⊗ N from cones in M and N. Such constructions are referred to as tensor products of cones.

"Sufficiently nice" candidates for tensor products of cones are bounded by the minimal and maximal tensor products. These products are generally distinct but coincide in special cases.

We define the minimal and maximal tensor products of pointed cones:

• minTensorProduct C₁ C₂: all conical combinations of elementary tensor products x ⊗ₜ y with x ∈ C₁ and y ∈ C₂.
• maxTensorProduct C₁ C₂: the dual cone of the minimal tensor product of the dual cones.

Main results

• minTensorProduct_le_maxTensorProduct: the minimal tensor product is less than or equal to the maximal tensor product

Notation

• no special notation defined
• x, y, z are elements of the (original) cones
• φ, ψ are elements of the dual cones

References

• Aubrun et al. Entangleability of cones

noncomputable def PointedCone.minTensorProduct {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {G : Type u_2} [AddCommGroup G] [Module R G] {H : Type u_3} [AddCommGroup H] [Module R H] (C₁ : PointedCone R G) (C₂ : PointedCone R H) : PointedCone R (TensorProduct R G H)

The minimal tensor product of two cones is given by all conical combinations of elementary tensor products x ⊗ₜ y with x ∈ C₁ and y ∈ C₂.

Equations

• C₁.minTensorProduct C₂ = PointedCone.span R (Set.image2 (fun (x1 : G) (x2 : H) => x1 ⊗ₜ[R] x2) ↑C₁ ↑C₂)

noncomputable def PointedCone.maxTensorProduct {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {G : Type u_2} [AddCommGroup G] [Module R G] {H : Type u_3} [AddCommGroup H] [Module R H] (C₁ : PointedCone R G) (C₂ : PointedCone R H) : PointedCone R (TensorProduct R G H)

The maximal tensor product of two cones is the dual (pointed cone) of the minimal tensor product of the dual cones.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PointedCone.mem_maxTensorProduct {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {G : Type u_2} [AddCommGroup G] [Module R G] {H : Type u_3} [AddCommGroup H] [Module R H] {C₁ : PointedCone R G} {C₂ : PointedCone R H} {z : TensorProduct R G H} : z ∈ C₁.maxTensorProduct C₂ ↔ ∀ φ ∈ dual (Module.dualPairing R G).flip ↑C₁, ∀ ψ ∈ dual (Module.dualPairing R H).flip ↑C₂, 0 ≤ ((TensorProduct.dualDistrib R G H) (φ ⊗ₜ[R] ψ)) z

Characterization of the maximal tensor product: z lies in maxTensorProduct C₁ C₂ iff all pairings with elementary dual tensors are nonnegative.

theorem PointedCone.tmul_mem_maxTensorProduct {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {G : Type u_2} [AddCommGroup G] [Module R G] {H : Type u_3} [AddCommGroup H] [Module R H] {x : G} {y : H} {C₁ : PointedCone R G} {C₂ : PointedCone R H} (hx : x ∈ C₁) (hy : y ∈ C₂) : x ⊗ₜ[R] y ∈ C₁.maxTensorProduct C₂

Elementary tensors are members of the maximal tensor product.

theorem PointedCone.tmul_mem_minTensorProduct {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {G : Type u_2} [AddCommGroup G] [Module R G] {H : Type u_3} [AddCommGroup H] [Module R H] {x : G} {y : H} {C₁ : PointedCone R G} {C₂ : PointedCone R H} (hx : x ∈ C₁) (hy : y ∈ C₂) : x ⊗ₜ[R] y ∈ C₁.minTensorProduct C₂

Elementary tensors are members of the minimal tensor product.

theorem PointedCone.tmul_subset_maxTensorProduct {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {G : Type u_2} [AddCommGroup G] [Module R G] {H : Type u_3} [AddCommGroup H] [Module R H] (C₁ : PointedCone R G) (C₂ : PointedCone R H) : Set.image2 (fun (x1 : G) (x2 : H) => x1 ⊗ₜ[R] x2) ↑C₁ ↑C₂ ⊆ ↑(C₁.maxTensorProduct C₂)

The maximal tensor product contains the set of all elementary tensors.

theorem PointedCone.tmul_subset_minTensorProduct {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {G : Type u_2} [AddCommGroup G] [Module R G] {H : Type u_3} [AddCommGroup H] [Module R H] (C₁ : PointedCone R G) (C₂ : PointedCone R H) : Set.image2 (fun (x1 : G) (x2 : H) => x1 ⊗ₜ[R] x2) ↑C₁ ↑C₂ ⊆ ↑(C₁.minTensorProduct C₂)

The minimal tensor product contains the set of all elementary tensors.

theorem PointedCone.minTensorProduct_le_maxTensorProduct {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {G : Type u_2} [AddCommGroup G] [Module R G] {H : Type u_3} [AddCommGroup H] [Module R H] (C₁ : PointedCone R G) (C₂ : PointedCone R H) : C₁.minTensorProduct C₂ ≤ C₁.maxTensorProduct C₂

The minimal tensor product is less than or equal to the maximal tensor product.