Documentation

Mathlib.Geometry.Convex.Cone.DualFinite

Duals of finitely generated cones #

This file defines the notion of dually finitely generated cones. A cone is dually finitely generated (or DualFG for short) if it is the dual of a finite set, or equivalently, of a finitely generated cone. In geometric terms, a cone is dually finitely generated if it can be written as the intersection of finitely many halfspaces. This is also known as an H-cone. This is the counterpart to FG (finitely generated) which states that the cone is the conic hull of a finite set, or a V-cone.

In finite dimensional vector spaces, FG is equivalent to DualFG by the Minkowski-Weyl theorem. In this case, V- and H-cones are known as polyhedral cones.

Main declarations #

source
def PointedCone.DualFG {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : M →ₗ[R] N →ₗ[R] R) (C : PointedCone R N) :
Prop

A cone is dually finitely generated (DualFG) if it is the dual of a finite set. Equivalently, the cone can be written as the intersection of finitely many halfspace. It is also known as an H-cone. This is the counterpart to FG (finitely generated) which states that the cone is the span of a finite set, or a V-cone.

Equations
Instances For
    source
    @[simp]
    theorem PointedCone.DualFG.top {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} :
    DualFG p ⊤

    The top cone is dually finitely generated.

    source
    theorem PointedCone.DualFG.exists_fg_dual {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} {C : PointedCone R N} (hC : DualFG p C) :
    ∃ (D : PointedCone R M), Submodule.FG D ∧ dual p ↑D = C

    A dually finitely generated cone is the dual of a finitely generated cone.

    source
    theorem PointedCone.DualFG.iff_exists_fg_dual {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} {C : PointedCone R N} :
    DualFG p C ↔ ∃ (D : PointedCone R M), Submodule.FG D ∧ dual p ↑D = C

    A cone is dually finitely generated if and only if it is the dual of a finitely generated cone.

    source
    theorem PointedCone.DualFG.id {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} {C : PointedCone R N} (hC : DualFG p C) :
    DualFG LinearMap.id C

    A dually finitely generated cone is dually finitely generated w.r.t. the identity pairing.

    source
    theorem PointedCone.DualFG.dual_of_finset {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : M →ₗ[R] N →ₗ[R] R) (s : Finset M) :
    DualFG p (dual p ↑s)

    The dual of a finite set is dually finitely generated.

    source
    theorem PointedCone.DualFG.dual_of_finite {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : M →ₗ[R] N →ₗ[R] R) {s : Set M} (hs : s.Finite) :
    DualFG p (dual p s)

    The dual of a finite set is dually finitely generated.

    source
    theorem PointedCone.DualFG.dual_of_fg {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : M →ₗ[R] N →ₗ[R] R) {C : PointedCone R M} (hC : Submodule.FG C) :
    DualFG p (dual p ↑C)

    The dual of a finitely generated cone is dually finitely generated.

    source
    theorem PointedCone.FG.dual_dualfg {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : M →ₗ[R] N →ₗ[R] R) {C : PointedCone R M} (hC : Submodule.FG C) :
    DualFG p (dual p ↑C)

    Alias of PointedCone.DualFG.dual_of_fg.

    The dual of a finitely generated cone is dually finitely generated.

    source
    theorem PointedCone.DualFG.inf {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} {C D : PointedCone R N} (hC : DualFG p C) (hD : DualFG p D) :
    DualFG p (C ⊓ D)

    The intersection of two dually finitely generated cones is again dually finitely generated.

    source
    @[simp]
    theorem PointedCone.DualFG.dual_dual_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} {C : PointedCone R N} (hC : DualFG p C) :
    dual p ↑(dual p.flip ↑C) = C

    The double dual of a dually finitely generated cone is the cone itself.

    source
    @[simp]
    theorem PointedCone.DualFG.dual_flip_dual {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} {C : PointedCone R M} (hC : DualFG p.flip C) :
    dual p.flip ↑(dual p ↑C) = C

    The double dual of a dually finitely generated cone is the cone itself.