Documentation

TauCeti.Geometry.Toric.Algebraic.Ray.Generation

Toric cones are generated by their primitive rays #

A salient finitely generated cone is the join of its rays. For a toric cone in an integral lattice each ray is spanned by its primitive generator, so the cone is the cone hull of its finitely many primitive ray generators. This is the description of a toric cone that the later constructions consume: an integral character is nonnegative on the cone exactly when it is nonnegative on each primitive ray generator, and the primitive ray generators of a regular cone are part of an integral basis, hence linearly independent, so a regular cone is simplicial.

Main declarations #

References #

source
theorem TauCeti.Toric.ToricRay.iSup_toPointedCone {V : Type u_2} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} (hσ : Submodule.FG σ) (hsal : (↑σ).Salient) :
⨆ (ρ : ToricRay σ), ρ.toPointedCone = σ

A salient finitely generated pointed cone is the join of its rays.

source
theorem TauCeti.Toric.ToricRay.nonempty_of_ne_bot {V : Type u_2} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} (hσ : Submodule.FG σ) (hsal : (↑σ).Salient) (hσ0 : σ ≠ ⊥) :
Nonempty (ToricRay σ)

A nonzero salient finitely generated pointed cone has a ray.

source
theorem TauCeti.Toric.ToricRay.le_iff_forall_mem_faceFinset {V : Type u_2} [AddCommGroup V] [Module ℝ V] {σ τ F : PointedCone ℝ V} (hστ : σ.IsFaceOf τ) (hσ : Submodule.FG σ) (hsal : (↑σ).Salient) :
σ ≤ F ↔ ∀ ρ ∈ faceFinset hστ hσ, ρ.toPointedCone ≤ F

A salient finitely generated face σ of a cone τ lies in a cone F exactly when every ray of τ contained in σ does, since σ is the join of its rays.

source
theorem TauCeti.Toric.ToricRay.exists_mem_faceFinset_not_le_of_not_le {V : Type u_2} [AddCommGroup V] [Module ℝ V] {σ τ F : PointedCone ℝ V} (hστ : σ.IsFaceOf τ) (hσ : Submodule.FG σ) (hsal : (↑σ).Salient) (hσF : ¬σ ≤ F) :
∃ ρ ∈ faceFinset hστ hσ, ¬ρ.toPointedCone ≤ F

A salient finitely generated face σ of a cone τ not contained in a cone F contains a ray of τ not contained in F.

source
theorem TauCeti.Toric.ToricRay.faceFinset_nonempty {V : Type u_2} [AddCommGroup V] [Module ℝ V] {σ τ : PointedCone ℝ V} (hστ : σ.IsFaceOf τ) (hσ : Submodule.FG σ) (hsal : (↑σ).Salient) (hσ0 : σ ≠ ⊥) :
(faceFinset hστ hσ).Nonempty

A nonzero salient finitely generated face of a cone contains a ray of the cone.

source
theorem TauCeti.Toric.IsToricCone.hull_primitiveGenerator {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) :
PointedCone.hull ℝ (⇑i '' Set.range (primitiveGenerator hi hσ)) = σ

A toric cone in an integral lattice is the cone hull of its primitive ray generators.

source
theorem TauCeti.Toric.IsToricCone.le_of_isFaceOf_of_sum_primitiveGenerator_mem {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {F : PointedCone ℝ V} (hF : F.IsFaceOf σ) (hu : i (∑ ρ ∈ ToricRay.faceFinset ⋯ ⋯, primitiveGenerator hi hσ ρ) ∈ F) :
σ ≤ F

A face of a toric cone σ containing the sum of the primitive generators of all rays of σ contains σ: by the face property it contains every primitive generator, and these span σ.

source
theorem TauCeti.Toric.mem_dualSemigroup_iff_primitiveGenerator {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) (m : N →+ ℤ) :
m ∈ dualSemigroup hi σ ↔ ∀ (ρ : ToricRay σ), 0 ≤ m (primitiveGenerator hi hσ ρ)

An integral character lies in the dual semigroup of a toric cone exactly when it is nonnegative on every primitive ray generator.

source
theorem TauCeti.Toric.mem_dualSemigroup_iff_of_isPrimitiveGenerator {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {v : ToricRay σ → N} (hv : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (v ρ)) (m : N →+ ℤ) :
m ∈ dualSemigroup hi σ ↔ ∀ (ρ : ToricRay σ), 0 ≤ m (v ρ)

An integral character lies in the dual semigroup of a toric cone exactly when it is nonnegative on a chosen primitive generator of each ray.

source
theorem TauCeti.Toric.IsRegularCone.linearIndependent_primitiveGenerator {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsRegularCone i σ) :
LinearIndependent ℝ fun (ρ : ToricRay σ) => i (primitiveGenerator hi ⋯ ρ)

The images of the primitive ray generators of a regular cone are linearly independent over the reals: they are part of an integral basis of the lattice, whose image is a real basis of the ambient space.

source
theorem TauCeti.Toric.IsRegularCone.isSimplicial {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsRegularCone i σ) :
σ.IsSimplicial

A regular cone is simplicial: it is the cone hull of its primitive ray generators, which are part of an integral basis and hence linearly independent over the reals.