Faces of pointed cones

This file defines what it means for a pointed cone to be a face of another pointed cone and establishes basic properties of this relation. A subcone F of a cone C is a face if any two points in C that have a positive combination in F are also in F.

Main declarations

• IsFaceOf F C: States that the pointed cone F is a face of the pointed cone C.

Implementation notes

• We do not use IsExtreme as a definition because this is an affine notion and does not allow the flexibility necessary to deal with cones over general rings. E.g. the cone of positive integers has no proper subset that are extreme. We prove that every face is an extreme set of its cone.
• Most results proven over a division ring hold more generally over an Archimedean ring. In particular, iff_mem_of_add_mem_left holds whenever for every x ∈ R there is a y ∈ R with 1 ≤ x * y.

structure PointedCone.IsFaceOf {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] (F C : PointedCone R M) : Prop

A sub-cone F of a pointed cone C is a face of C if any two points of C with a strictly positive combination in F are also in F.

• le : F ≤ C
• mem_of_smul_add_mem {x y : M} {a : R} : x ∈ C → y ∈ C → 0 < a → a • x + y ∈ F → x ∈ F

theorem PointedCone.isFaceOf_iff {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] (F C : PointedCone R M) : F.IsFaceOf C ↔ F ≤ C ∧ ∀ {x y : M} {a : R}, x ∈ C → y ∈ C → 0 < a → a • x + y ∈ F → x ∈ F

theorem PointedCone.IsFaceOf.mem_of_smul_add_smul_mem_left {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F : PointedCone R M} {x y : M} {a b : R} (hF : F.IsFaceOf C) (hx : x ∈ C) (hy : y ∈ C) (ha : 0 < a) (hb : 0 < b) (h : a • x + b • y ∈ F) : x ∈ F

theorem PointedCone.IsFaceOf.mem_of_smul_add_smul_mem_right {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F : PointedCone R M} {x y : M} {a b : R} (hF : F.IsFaceOf C) (hx : x ∈ C) (hy : y ∈ C) (ha : 0 < a) (hb : 0 < b) (h : a • x + b • y ∈ F) : y ∈ F

@[simp]

theorem PointedCone.IsFaceOf.refl {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] (C : PointedCone R M) : C.IsFaceOf C

A pointed cone C is a face of itself.

theorem PointedCone.IsFaceOf.rfl {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C : PointedCone R M} : C.IsFaceOf C

theorem PointedCone.IsFaceOf.isFaceOf_iff_le {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F₁ F₂ : PointedCone R M} (h₁ : F₁.IsFaceOf C) (h₂ : F₂.IsFaceOf C) : F₁.IsFaceOf F₂ ↔ F₁ ≤ F₂

A face of a cone is a face of another if and only if they are contained in each other.

theorem PointedCone.IsFaceOf.isExtreme {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F : PointedCone R M} (h : F.IsFaceOf C) : IsExtreme R ↑C ↑F

A face of a cone is an extreme subset of the cone.

theorem PointedCone.IsFaceOf.inf {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C₁ C₂ F₁ F₂ : PointedCone R M} (h₁ : F₁.IsFaceOf C₁) (h₂ : F₂.IsFaceOf C₂) : (F₁ ⊓ F₂).IsFaceOf (C₁ ⊓ C₂)

The intersection of two faces of two cones is a face of the intersection of the cones.

theorem PointedCone.IsFaceOf.inf_left {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F₁ F₂ : PointedCone R M} (h₁ : F₁.IsFaceOf C) (h₂ : F₂.IsFaceOf C) : (F₁ ⊓ F₂).IsFaceOf C

The intersection of two faces of a cone is a face of the cone.

theorem PointedCone.IsFaceOf.inf_right {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C₁ C₂ F : PointedCone R M} (h₁ : F.IsFaceOf C₁) (h₂ : F.IsFaceOf C₂) : F.IsFaceOf (C₁ ⊓ C₂)

If a cone is a face of two cones simultaneously, then it's also a face of their intersection.

theorem PointedCone.IsFaceOf.sInf {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C : PointedCone R M} (F : Set (PointedCone R M)) (h : ∀ f ∈ F, f.IsFaceOf C) : (C ⊓ sInf F).IsFaceOf C

theorem PointedCone.IsFaceOf.mem_of_add_mem_left {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F : PointedCone R M} (hF : F.IsFaceOf C) {x y : M} (hx : x ∈ C) (hy : y ∈ C) (hxy : x + y ∈ F) : x ∈ F

theorem PointedCone.IsFaceOf.mem_of_add_mem_right {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F : PointedCone R M} (hF : F.IsFaceOf C) {x y : M} (hx : x ∈ C) (hy : y ∈ C) (hxy : x + y ∈ F) : y ∈ F

theorem PointedCone.IsFaceOf.add_mem_iff_mem {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F : PointedCone R M} (hF : F.IsFaceOf C) {x y : M} (hx : x ∈ C) (hy : y ∈ C) : x + y ∈ F ↔ x ∈ F ∧ y ∈ F

theorem PointedCone.IsFaceOf.mem_of_sum_mem {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F : PointedCone R M} {ι : Type u_4} [Fintype ι] {f : ι → M} (hF : F.IsFaceOf C) (hsC : ∀ (i : ι), f i ∈ C) (hs : ∑ i : ι, f i ∈ F) (i : ι) : f i ∈ F

If the sum of points of a cone is in a face, then all the points are in the face.

theorem PointedCone.IsFaceOf.sum_mem_iff_mem {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F : PointedCone R M} {ι : Type u_4} [Fintype ι] {f : ι → M} (hF : F.IsFaceOf C) (hsC : ∀ (i : ι), f i ∈ C) : ∑ i : ι, f i ∈ F ↔ ∀ (i : ι), f i ∈ F

theorem PointedCone.IsFaceOf.mem_of_sum_smul_mem {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F : PointedCone R M} {ι : Type u_4} [Fintype ι] {f : ι → M} {c : ι → R} (hF : F.IsFaceOf C) (hsC : ∀ (i : ι), f i ∈ C) (hc : ∀ (i : ι), 0 ≤ c i) (hs : ∑ i : ι, c i • f i ∈ F) (i : ι) (hci : 0 < c i) : f i ∈ F

If the positive combination of points of a cone is in a face, then all the points are in the face.

theorem PointedCone.IsFaceOf.trans {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F₁ F₂ : PointedCone R M} (h₁ : F₂.IsFaceOf F₁) (h₂ : F₁.IsFaceOf C) : F₂.IsFaceOf C

The face of a face of a cone is also a face of the cone.

theorem PointedCone.IsFaceOf.map {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F : PointedCone R M} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Injective ⇑f) (hF : F.IsFaceOf C) : (map f F).IsFaceOf (map f C)

The image of a face of a cone under an injective linear map is a face of the image of the cone.

theorem PointedCone.IsFaceOf.map_equiv {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F : PointedCone R M} [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) (hF : F.IsFaceOf C) : (map (↑e) F).IsFaceOf (map (↑e) C)

The image of a face of a cone under an equivalence is a face of the image of the cone.

theorem PointedCone.IsFaceOf.of_map_injective {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F : PointedCone R M} [AddCommGroup N] [Module R N] {f : M →ₗ[R] N} (hf : Function.Injective ⇑f) (hc : (map f F).IsFaceOf (map f C)) : F.IsFaceOf C

theorem PointedCone.IsFaceOf.comap {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F : PointedCone R M} [AddCommGroup N] [Module R N] (f : N →ₗ[R] M) (hF : F.IsFaceOf C) : (comap f F).IsFaceOf (comap f C)

The comap of a face of a cone under a linear map is a face of the comap of the cone.

theorem PointedCone.IsFaceOf.of_comap_surjective {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F : PointedCone R M} [AddCommGroup N] [Module R N] {f : N →ₗ[R] M} (hf : Function.Surjective ⇑f) (hc : (comap f F).IsFaceOf (comap f C)) : F.IsFaceOf C

theorem PointedCone.isFaceOf_map_iff {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F : PointedCone R M} [AddCommGroup N] [Module R N] {f : M →ₗ[R] N} (hf : Function.Injective ⇑f) : (map f F).IsFaceOf (map f C) ↔ F.IsFaceOf C

The image of a cone F under an injective linear map is a face of the image of another cone C if and only if F is a face of C.

theorem PointedCone.isFaceOf_comap_iff {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F : PointedCone R M} [AddCommGroup N] [Module R N] {f : N →ₗ[R] M} (hf : Function.Surjective ⇑f) : (comap f F).IsFaceOf (comap f C) ↔ F.IsFaceOf C

The comap of a cone F under a surjective linear map is a face of the comap of another cone F if and only if F is a face of C.

theorem PointedCone.IsFaceOf.of_mem_of_add_mem_left {R : Type u_1} {M : Type u_2} [DivisionRing R] [LinearOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F : PointedCone R M} (h₁ : F ≤ C) (h₂ : ∀ {x y : M}, x ∈ C → y ∈ C → x + y ∈ F → x ∈ F) : F.IsFaceOf C

theorem PointedCone.IsFaceOf.lineal {R : Type u_1} {M : Type u_2} [DivisionRing R] [LinearOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] (C : PointedCone R M) : (↑C.lineal).IsFaceOf C

The lineality space of a cone is a face.

theorem PointedCone.IsFaceOf.lineal_le {R : Type u_1} {M : Type u_2} [DivisionRing R] [LinearOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F : PointedCone R M} (hF : F.IsFaceOf C) : ↑C.lineal ≤ F

The lineality space of a cone lies in every face.

theorem PointedCone.IsFaceOf.lineal_congr {R : Type u_1} {M : Type u_2} [DivisionRing R] [LinearOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C F : PointedCone R M} (hF : F.IsFaceOf C) : F.lineal = C.lineal

The lineality space of a face of a cone agrees with the lineality space of the cone.

theorem PointedCone.IsFaceOf.prod {R : Type u_1} {M : Type u_2} {N : Type u_3} [DivisionRing R] [LinearOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {C₁ F₁ : PointedCone R M} {C₂ F₂ : PointedCone R N} (hF₁ : F₁.IsFaceOf C₁) (hF₂ : F₂.IsFaceOf C₂) : IsFaceOf (Submodule.prod F₁ F₂) (Submodule.prod C₁ C₂)

The product of two faces of two cones is a face of the product of the cones.

theorem PointedCone.IsFaceOf.fst {R : Type u_1} {M : Type u_2} {N : Type u_3} [DivisionRing R] [LinearOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {C₁ : PointedCone R M} {C₂ : PointedCone R N} {F : PointedCone R (M × N)} (hF : F.IsFaceOf (Submodule.prod C₁ C₂)) : (map (LinearMap.fst R M N) F).IsFaceOf C₁

The projection of a face of a product cone onto the first component is a face of the projection of the product cone onto the first component.

theorem PointedCone.IsFaceOf.snd {R : Type u_1} {M : Type u_2} {N : Type u_3} [DivisionRing R] [LinearOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {C₁ : PointedCone R M} {C₂ : PointedCone R N} {F : PointedCone R (M × N)} (hF : F.IsFaceOf (Submodule.prod C₁ C₂)) : (map (LinearMap.snd R M N) F).IsFaceOf C₂

The projection of a face of a product cone onto the second component is a face of the projection of the product cone onto the second component.