Face

This file defines the concept of a face of a pointed cone. It also defines the complete lattice structure on the collection of all faces of such a cone.

Main definitions

• Face C: the face lattice of C.
• Face.prod: the product of two faces of pointed cones, together with projections fst and snd.
• Face.prodOrderIso: proves that the face lattices of a product cone is the product of the face lattices of the individual cones.

Implementation notes

This is separate from faces of general convex sets in affine spaces, since the empty set is not a face of a convex cone, but of the corresponding convex set. The notion we use here allows a clean correspondence between the face lattice of convex sets and their homogenization cones.

structure PointedCone.Face {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] (C : PointedCone R M) extends Submodule (Nonneg R) M : Type u_2

The face lattice of a pointed cone C.

• carrier : Set M
• add_mem' {a b : M} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• smul_mem' (c : Nonneg R) {x : M} : x ∈ self.carrier → c • x ∈ self.carrier
• isFaceOf : IsFaceOf self.toSubmodule C

@[reducible, inline]

abbrev PointedCone.Face.toPointedCone {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C : PointedCone R M} (F : C.Face) : PointedCone R M

Converts a face of a pointed cone into a pointed cone.

Equations

• ↑F = F.toSubmodule

@[instance_reducible]

instance PointedCone.Face.instCoeOut {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C : PointedCone R M} : CoeOut C.Face (PointedCone R M)

Equations

• PointedCone.Face.instCoeOut = { coe := PointedCone.Face.toPointedCone }

@[instance_reducible]

instance PointedCone.Face.instSetLike {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C : PointedCone R M} : SetLike C.Face M

Equations

• PointedCone.Face.instSetLike = { coe := fun (C_1 : C.Face) => ↑↑C_1, coe_injective := ⋯ }

@[instance_reducible]

instance PointedCone.Face.instPartialOrder {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C : PointedCone R M} : PartialOrder C.Face

Equations

• PointedCone.Face.instPartialOrder = PartialOrder.ofSetLike C.Face M

theorem PointedCone.Face.toPointedCone_le {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C : PointedCone R M} {F : C.Face} : ↑F ≤ C

theorem PointedCone.Face.ext {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C : PointedCone R M} {F₁ F₂ : C.Face} (h : ∀ (x : M), x ∈ F₁ ↔ x ∈ F₂) : F₁ = F₂

theorem PointedCone.Face.ext_iff {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C : PointedCone R M} {F₁ F₂ : C.Face} : F₁ = F₂ ↔ ∀ (x : M), x ∈ F₁ ↔ x ∈ F₂

@[simp]

theorem PointedCone.Face.toPointedCone_le_toPointedCone {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C : PointedCone R M} {F₁ F₂ : C.Face} : ↑F₁ ≤ ↑F₂ ↔ F₁ ≤ F₂

@[simp]

theorem PointedCone.Face.toPointedCone_lt_toPointedCone {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C : PointedCone R M} {F₁ F₂ : C.Face} : ↑F₁ < ↑F₂ ↔ F₁ < F₂

@[simp]

theorem PointedCone.Face.mem_toPointedCone {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C : PointedCone R M} {F : C.Face} (x : M) : x ∈ ↑F ↔ x ∈ F

Infimum, supremum and lattice

@[instance_reducible]

instance PointedCone.Face.instMin {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C : PointedCone R M} : Min C.Face

The infimum of two faces F₁, F₂ of C is the intersection of the cones F₁ and F₂.

Equations

• PointedCone.Face.instMin = { min := fun (F₁ F₂ : C.Face) => { toSubmodule := ↑F₁ ⊓ ↑F₂, isFaceOf := ⋯ } }

@[instance_reducible]

instance PointedCone.Face.instInfSet {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C : PointedCone R M} : InfSet C.Face

Equations

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

@[instance_reducible]

instance PointedCone.Face.instSemilatticeInf {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C : PointedCone R M} : SemilatticeInf C.Face

Equations

• PointedCone.Face.instSemilatticeInf = { toPartialOrder := PointedCone.Face.instPartialOrder, inf := min, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

@[instance_reducible]

instance PointedCone.Face.instCompleteSemilatticeInf {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C : PointedCone R M} : CompleteSemilatticeInf C.Face

Equations

• PointedCone.Face.instCompleteSemilatticeInf = { toPartialOrder := PointedCone.Face.instSemilatticeInf.toPartialOrder, toInfSet := PointedCone.Face.instInfSet, isGLB_sInf := ⋯ }

@[instance_reducible]

instance PointedCone.Face.instCompleteLattice {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C : PointedCone R M} : CompleteLattice C.Face

Equations

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

@[instance_reducible]

instance PointedCone.Face.instInhabited {R : Type u_1} {M : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] {C : PointedCone R M} : Inhabited C.Face

Equations

• PointedCone.Face.instInhabited = { default := ⊤ }

theorem PointedCone.Face.lineal_eq_bot {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

The bottom face of C is its lineality space.

Product

def PointedCone.Face.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₁ : PointedCone R M} {C₂ : PointedCone R N} (F₁ : C₁.Face) (F₂ : C₂.Face) : Face (Submodule.prod C₁ C₂)

The face of C₁ × C₂ obtained by taking the (submodule) product of faces F₁ ≤ C₁ and F₂ ≤ C₂.

Equations

• F₁.prod F₂ = { toSubmodule := F₁.prod F₂.toSubmodule, isFaceOf := ⋯ }

def PointedCone.Face.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 : Face (Submodule.prod C₁ C₂)) : C₁.Face

The face of C₁ obtained by projecting to the first component of a face F ≤ C₁ × C₂.

Equations

• F.fst = { toSubmodule := PointedCone.map (LinearMap.fst R M N) F.toSubmodule, isFaceOf := ⋯ }

def PointedCone.Face.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 : Face (Submodule.prod C₁ C₂)) : C₂.Face

The face of C₁ obtained by projecting to the second component of a face F ≤ C₁ × C₂.

Equations

• F.snd = { toSubmodule := PointedCone.map (LinearMap.snd R M N) F.toSubmodule, isFaceOf := ⋯ }

@[simp]

theorem PointedCone.Face.fst_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₁ : PointedCone R M} {C₂ : PointedCone R N} (F₁ : C₁.Face) (F₂ : C₂.Face) : (F₁.prod F₂).fst = F₁

@[simp]

theorem PointedCone.Face.snd_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₁ : PointedCone R M} {C₂ : PointedCone R N} (F₁ : C₁.Face) (F₂ : C₂.Face) : (F₁.prod F₂).snd = F₂

theorem PointedCone.Face.fst_prod_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} (G : Face (Submodule.prod C₁ C₂)) : G.fst.prod G.snd = G

theorem PointedCone.Face.prod_mono {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₁ F₁' : C₁.Face} {F₂ F₂' : C₂.Face} (h₁ : F₁ ≤ F₁') (h₂ : F₂ ≤ F₂') : F₁.prod F₂ ≤ F₁'.prod F₂'

def PointedCone.Face.prodOrderIso {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) (D : PointedCone R N) : Face (Submodule.prod C D) ≃o C.Face × D.Face

The face lattice of the product of two cones is isomorphic to the product of their face lattices.

Equations

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