Faces cut out by nonnegative linear functionals

A linear functional φ that is nonnegative on a pointed cone C cuts out the face C ⊓ ker φ of C. This file records that fact and the finiteness property that makes such faces useful for localization: if C is finitely generated, then any functional ψ that is nonnegative on the face C ⊓ ker φ becomes nonnegative on all of C after adding a sufficiently large multiple of φ. Conversely, a face F of the cone hull of a set s is cut out by any functional that is nonnegative on s and vanishes at exactly the members of s lying in F.

The second statement is what identifies the dual of the face with the dual of C enlarged by -φ. In toric geometry it shows that the semigroup of characters of the face σ ∩ m^⊥ is obtained from that of σ by adjoining -m, so the affine chart of the face is the localization of the chart of σ away from the monomial of m. Finite generation cannot be dropped: the cone in ℝ² generated by all vectors (1, t) with t ≥ 0 meets the kernel of φ (x, y) = x only in 0, so ψ (x, y) = -y is nonnegative on that face, yet ψ + n • φ is negative at (1, n + 1).

Main declarations

• PointedCone.isFaceOf_inf_ker: a functional nonnegative on C cuts out a face of C.
• PointedCone.inf_ker_add: the face cut out by a sum of nonnegative functionals is the intersection of the faces they cut out.
• PointedCone.inf_ker_eq_of_eq_hull: a functional nonnegative on a generating set and vanishing at exactly the generators in a face F cuts out F.
• PointedCone.FG.exists_nonneg_add_nsmul: on a finitely generated cone, a functional nonnegative on the face cut out by φ becomes nonnegative after adding a multiple of φ.

Every face of a finitely generated cone is exposed by a nonnegative linear functional, including cones with lineality and the full face. The construction uses Tucker’s theorem over an arbitrary linearly ordered field. Over real normed spaces it gives Mathlib’s continuous-functional IsExposed predicate; conversely, any nonempty exposed subset of a cone over a linearly ordered field with an arbitrary topology is a cone face.

The finite-generation exposure results are adapted from Mei/Geometry/Convex/Cone/Face/Exposed.lean at Mei commit 7f1e4c7.

References

• W. Fulton, Introduction to Toric Varieties, §§1.2–1.3.
• D. Cox, J. Little and H. Schenck, Toric Varieties, §1.2 and §1.3.

theorem PointedCone.inf_ker_add {R : Type u_1} {M : Type u_2} [AddCommMonoid M] [Semiring R] [PartialOrder R] [IsOrderedRing R] [Module R M] {C : PointedCone R M} {φ ψ : Module.Dual R M} (hφ : ∀ x ∈ C, 0 ≤ φ x) (hψ : ∀ x ∈ C, 0 ≤ ψ x) : C ⊓ ↑(LinearMap.ker (φ + ψ)) = C ⊓ ↑(LinearMap.ker φ) ⊓ (C ⊓ ↑(LinearMap.ker ψ))

If two linear functionals φ and ψ are nonnegative on a pointed cone C, the face cut out by φ + ψ is the intersection of the faces cut out by φ and by ψ.

theorem PointedCone.isFaceOf_inf_ker {R : Type u_1} {M : Type u_2} [AddCommGroup M] [Semiring R] [PartialOrder R] [IsOrderedRing R] [NoZeroDivisors R] [Module R M] {C : PointedCone R M} {φ : Module.Dual R M} (hφ : ∀ x ∈ C, 0 ≤ φ x) : (C ⊓ ↑(LinearMap.ker φ)).IsFaceOf C

A linear functional that is nonnegative on a pointed cone cuts out a face of the cone.

theorem PointedCone.inf_ker_eq_of_eq_hull {R : Type u_1} {M : Type u_2} [AddCommGroup M] [Semiring R] [PartialOrder R] [IsOrderedRing R] [NoZeroDivisors R] [Module R M] {C F : PointedCone R M} {s : Set M} (hC : C = hull R s) (hF : F.IsFaceOf C) {φ : Module.Dual R M} (hφ : ∀ x ∈ s, 0 ≤ φ x) (hφF : ∀ x ∈ s, φ x = 0 ↔ x ∈ F) : C ⊓ ↑(LinearMap.ker φ) = F

Let F be a face of the cone hull C of a set s. A linear functional that is nonnegative on s and vanishes at exactly those members of s which lie in F cuts out F from C.

theorem PointedCone.FG.exists_nonneg_add_nsmul {R : Type u_1} {M : Type u_2} [AddCommMonoid M] [Ring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] [Module R M] {C : PointedCone R M} (hC : Submodule.FG C) {φ ψ : Module.Dual R M} (hφ : ∀ x ∈ C, 0 ≤ φ x) (hψ : ∀ x ∈ C, φ x = 0 → 0 ≤ ψ x) : ∃ (n : ℕ), ∀ x ∈ C, 0 ≤ ψ x + n • φ x

On a finitely generated pointed cone C, let φ be nonnegative on C and let ψ be nonnegative on the face C ⊓ ker φ. Then ψ + n • φ is nonnegative on C for some natural number n.

theorem PointedCone.IsFaceOf.exists_nonneg_linear_inf_ker {K : Type u_1} {V : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommGroup V] [Module K V] {C F : PointedCone K V} (hF : F.IsFaceOf C) (hC : Submodule.FG C) : ∃ (f : Module.Dual K V), (∀ x ∈ C, 0 ≤ f x) ∧ C ⊓ ↑(LinearMap.ker f) = F

Every face of a finitely generated cone is cut out by a linear functional nonnegative on the cone. Cones with lineality and the full face are included.

theorem PointedCone.IsFaceOf.exists_nonneg_linear_zero_iff {K : Type u_1} {V : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommGroup V] [Module K V] {C F : PointedCone K V} (hF : F.IsFaceOf C) (hC : Submodule.FG C) : ∃ (f : Module.Dual K V), (∀ x ∈ C, 0 ≤ f x) ∧ ∀ x ∈ C, f x = 0 ↔ x ∈ F

The exposing functional vanishes precisely on the chosen face, among all points of the original finitely generated cone.

theorem IsExposed.exists_isFaceOf_coe_eq {K : Type u_1} {V : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [TopologicalSpace K] [AddCommGroup V] [TopologicalSpace V] [Module K V] {C : PointedCone K V} {S : Set V} (hS : IsExposed K (↑C) S) (hne : S.Nonempty) : ∃ (F : PointedCone K V), F.IsFaceOf C ∧ ↑F = S

Every nonempty exposed subset of a pointed cone is the carrier of a cone face. No finite-generation or closedness assumption is needed in this direction.

theorem PointedCone.IsFaceOf.isExposed_of_fg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {C F : PointedCone ℝ V} (hF : F.IsFaceOf C) (hC : Submodule.FG C) : IsExposed ℝ ↑C ↑F

Every face of a finitely generated cone in a real normed space is exposed in Mathlib's continuous-functional sense. Finite generation provides continuity on the span of the generators, and Hahn–Banach extends the exposing functional.