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 coneFis a face of the pointed coneC.
Implementation notes #
- We do not use
IsExtremeas a definition because this is an affine notion and does not allow the flexibility necessary to deal wth 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_leftholds whenever for everyx ∈ Rthere is ay ∈ Rwith1 ≤ 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)
:
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.
Instances For
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)
:
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)
:
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)
:
@[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)
:
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)
:
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)
:
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)
:
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)
:
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 : ι)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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.