Documentation

TauCeti.Geometry.Convex.Cone.Face.Simplicial

The face lattice of a simplicial cone #

A simplicial cone is the cone hull of a linearly independent family v : ι → M. Because the coefficients of a conical combination of a linearly independent family are unique, the faces of such a cone are exactly the subcones spanned by subfamilies: the face lattice of PointedCone.hull R (Set.range v) is the powerset of ι.

Both halves of the correspondence use the description of the cone hull of a subfamily as the set of conical combinations supported on that subfamily. That a face is spanned by the generators it contains holds for any generating set, and the family-indexed form PointedCone.Face.eq_hull_image is a reindexing of PointedCone.IsFaceOf.eq_hull_inter_of_eq_hull. The converse, that every subfamily spans a face, is where linear independence enters: if a • x + y has no v j component for j outside a subset A, then neither does x, because the two nonnegative contributions to the j-th coefficient cannot cancel.

Linear independence cannot be dropped. The cone in ℝ² spanned by (1, 0), (1, 1) and (0, 1) has four faces, not the eight cones spanned by subsets of that family, since the ray through (1, 1) is not a face; and the cone spanned by (1, 0) and (-1, 0) is a line whose only face is itself.

Main declarations #

References #

source
theorem PointedCone.mem_hull_image_iff_linearCombination {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] {v : ι → M} {A : Set ι} {x : M} [AddCommMonoid M] [Module R M] :
x ∈ hull R (v '' A) ↔ ∃ c ∈ Finsupp.supported R R A, (∀ (j : ι), 0 ≤ c j) ∧ (Finsupp.linearCombination R v) c = x

An element of the cone hull of a subfamily v '' A is exactly a conical combination of the family v whose coefficients are supported on A. This is the conical analogue of Finsupp.mem_span_image_iff_linearCombination, with nonnegative coefficients.

source
theorem PointedCone.apply_mem_hull_image_iff {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] {v : ι → M} {A : Set ι} [AddCommMonoid M] [Module R M] [Nontrivial R] (hv : LinearIndependent R v) {j : ι} :
v j ∈ hull R (v '' A) ↔ j ∈ A

A member of a linearly independent family lies in the cone spanned by a subfamily exactly when it is one of the vectors of that subfamily.

source
theorem PointedCone.isFaceOf_hull_image {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] {v : ι → M} [AddCommGroup M] [Module R M] {C : PointedCone R M} [NoZeroDivisors R] (hv : LinearIndependent R v) (hC : C = hull R (Set.range v)) (A : Set ι) :
(hull R (v '' A)).IsFaceOf C

A subfamily of a linearly independent family spans a face of the cone generated by the whole family: the coefficients of a conical combination are unique, and a positive combination cannot cancel the coefficients outside the subfamily.

source
theorem PointedCone.salient_hull_range {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] {v : ι → M} [AddCommGroup M] [Module R M] (hv : LinearIndependent R v) :
(↑(hull R (Set.range v))).Salient

The cone hull of a linearly independent family is salient.

source
theorem PointedCone.Face.eq_hull_image {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] {v : ι → M} [AddCommGroup M] [Module R M] {C : PointedCone R M} (F : C.Face) (hC : C = hull R (Set.range v)) :
↑F = hull R (v '' {j : ι | v j ∈ F})

A face of a cone generated by a family v is the cone spanned by the members of v that it contains.

source
def PointedCone.faceOrderIsoSet {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] {v : ι → M} [AddCommGroup M] [Module R M] {C : PointedCone R M} [Nontrivial R] [NoZeroDivisors R] (hv : LinearIndependent R v) (hC : C = hull R (Set.range v)) :
C.Face ≃o Set ι

The face lattice of the cone hull of a linearly independent family v : ι → M is the lattice of subsets of ι: a face is recorded by the set of indices whose vectors it contains, and a set of indices spans the corresponding face.

Instances For
    source
    @[simp]
    theorem PointedCone.faceOrderIsoSet_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] {v : ι → M} [AddCommGroup M] [Module R M] {C : PointedCone R M} [Nontrivial R] [NoZeroDivisors R] (hv : LinearIndependent R v) (hC : C = hull R (Set.range v)) (F : C.Face) :
    (faceOrderIsoSet hv hC) F = {j : ι | v j ∈ F}
    source
    @[simp]
    theorem PointedCone.faceOrderIsoSet_symm_apply_toPointedCone {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] {v : ι → M} [AddCommGroup M] [Module R M] {C : PointedCone R M} [Nontrivial R] [NoZeroDivisors R] (hv : LinearIndependent R v) (hC : C = hull R (Set.range v)) (A : Set ι) :
    ↑((faceOrderIsoSet hv hC).symm A) = hull R (v '' A)
    source
    theorem TauCeti.finrank_span_face_eq_card_faceOrderIsoSet {V : Type u_1} [AddCommGroup V] [Module ℝ V] {C : PointedCone ℝ V} {ι : Type u_2} (v : ι → V) (hv : LinearIndependent ℝ v) (hcone : C = PointedCone.hull ℝ (Set.range v)) (G : C.Face) :
    Module.finrank ℝ ↥(Submodule.span ℝ ↑↑G) = Nat.card { a : ι // a ∈ (PointedCone.faceOrderIsoSet hv hcone) G }

    The real dimension of a face of a cone generated by a linearly independent family equals the number of generators in the subset corresponding to that face. When that subset is infinite, both sides are 0.