Rays of toric cones

A ray of a cone is a one-dimensional face. This file defines the ray type on Mathlib's face lattice and proves the finiteness needed to index the primitive ray generators of a toric cone: finite generation of the ambient cone alone already bounds the rays. It also records the geometric content of one-dimensionality: every nonzero point of a salient ray spans it as a pointed cone.

Main declarations

• TauCeti.Toric.ToricRay: the one-dimensional faces of a pointed cone.
• TauCeti.Toric.ToricRay.finite_of_fg: a finitely generated pointed cone, and hence a toric cone, has finitely many rays.
• TauCeti.Toric.ToricRay.exists_mem_ne_zero: every ray contains a nonzero point.
• TauCeti.Toric.ToricRay.eq_hull_singleton: every nonzero point of a salient ray generates that ray.
• TauCeti.Toric.ToricRay.toPointedCone_le_toPointedCone_iff: in a salient cone, a ray contained in another ray equals it.
• TauCeti.Toric.ToricRay.instIsEmptyBot: the zero cone has no rays.
• TauCeti.Toric.ToricRay.faceEmbedding and TauCeti.Toric.ToricRay.range_faceEmbedding: the rays of a face of a cone are exactly the rays of the cone contained in that face.
• TauCeti.Toric.ToricRay.faceFinset: the finite set of rays of a cone contained in a finitely generated face.
• TauCeti.Toric.ToricRay.hullSingleton and TauCeti.Toric.ToricRay.eq_hullSingleton: the cone spanned by a nonzero vector is its own only ray.
• TauCeti.Toric.ToricRay.map_fst_eq_bot_of_map_snd_ne_bot, TauCeti.Toric.ToricRay.prodRayFst, TauCeti.Toric.ToricRay.prodRaySnd, TauCeti.Toric.ToricRay.prodInl, TauCeti.Toric.ToricRay.prodInr and TauCeti.Toric.ToricRay.prodSplit: the rays of a product of salient cones are exactly the rays of the two factors.

References

The ray description is from §1.2 of W. Fulton, Introduction to Toric Varieties, and §1.2 of D. Cox, J. Little and H. Schenck, Toric Varieties.

@[reducible, inline]

abbrev TauCeti.Toric.ToricRay {V : Type u_1} [AddCommGroup V] [Module ℝ V] (σ : PointedCone ℝ V) : Type u_1

A ray of a pointed cone is a face whose linear span has real dimension one.

@[reducible, inline]

abbrev TauCeti.Toric.ToricRay.toPointedCone {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} (ρ : ToricRay σ) : PointedCone ℝ V

The pointed cone underlying a ray.

@[instance_reducible]

instance TauCeti.Toric.ToricRay.instSetLike {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} : SetLike (ToricRay σ) V

Rays are viewed as sets of vectors: membership x ∈ ρ and the coercion (ρ : Set V) both refer to the pointed cone ρ.toPointedCone underlying the ray, and two rays with the same points are equal.

@[simp]

theorem TauCeti.Toric.ToricRay.finrank_span {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} (ρ : ToricRay σ) : Module.finrank ℝ ↥(Submodule.span ℝ ↑ρ) = 1

The span of the cone underlying a ray has real dimension one.

theorem TauCeti.Toric.ToricRay.toPointedCone_ne_bot {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} (ρ : ToricRay σ) : ρ.toPointedCone ≠ ⊥

A ray is not the zero pointed cone.

theorem TauCeti.Toric.ToricRay.exists_mem_ne_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} (ρ : ToricRay σ) : ∃ x ∈ ρ, x ≠ 0

Every ray contains a nonzero point.

theorem TauCeti.Toric.ToricRay.eq_hull_singleton {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} (ρ : ToricRay σ) (hρ : (↑ρ.toPointedCone).Salient) {x : V} (hx : x ∈ ρ) (hx0 : x ≠ 0) : ρ.toPointedCone = ℝ ∙₊ x

Every nonzero point of a salient ray generates it as a pointed cone. Only the ray itself has to be salient; for a ray of a salient ambient cone this follows from ConvexCone.Salient.anti along the face inclusion.

The zero cone

instance TauCeti.Toric.ToricRay.instIsEmptyBot {V : Type u_1} [AddCommGroup V] [Module ℝ V] : IsEmpty (ToricRay ⊥)

The zero cone has no rays: its only face is itself, whose span is zero-dimensional.

Rays of a face

def TauCeti.Toric.ToricRay.faceEmbedding {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ τ : PointedCone ℝ V} (hτ : τ.IsFaceOf σ) : ToricRay τ ↪ ToricRay σ

A ray of a face τ of a cone σ is a ray of σ: a face of a face is a face, and one-dimensionality of the span does not mention the ambient cone.

@[simp]

theorem TauCeti.Toric.ToricRay.toPointedCone_faceEmbedding {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ τ : PointedCone ℝ V} (hτ : τ.IsFaceOf σ) (ρ : ToricRay τ) : ((faceEmbedding hτ) ρ).toPointedCone = ρ.toPointedCone

@[simp]

theorem TauCeti.Toric.ToricRay.mem_faceEmbedding {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ τ : PointedCone ℝ V} (hτ : τ.IsFaceOf σ) (ρ : ToricRay τ) {x : V} : x ∈ (faceEmbedding hτ) ρ ↔ x ∈ ρ

@[simp]

theorem TauCeti.Toric.ToricRay.range_faceEmbedding {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ τ : PointedCone ℝ V} (hτ : τ.IsFaceOf σ) : Set.range ⇑(faceEmbedding hτ) = {ρ : ToricRay σ | ρ.toPointedCone ≤ τ}

The rays of a face τ of σ are exactly the rays of σ that are contained in τ: a face of σ contained in τ is a face of τ, and one-dimensionality does not mention the ambient cone.

The ray spanned by a vector

def TauCeti.Toric.ToricRay.hullSingleton {V : Type u_1} [AddCommGroup V] [Module ℝ V] {x : V} (hx : x ≠ 0) : ToricRay (ℝ ∙₊ x)

The cone spanned by a nonzero vector is a ray of itself, and by TauCeti.Toric.ToricRay.eq_hullSingleton its only one.

theorem TauCeti.Toric.ToricRay.toPointedCone_hullSingleton {V : Type u_1} [AddCommGroup V] [Module ℝ V] {x : V} (hx : x ≠ 0) : (hullSingleton hx).toPointedCone = ℝ ∙₊ x

@[simp]

theorem TauCeti.Toric.ToricRay.mem_hullSingleton {V : Type u_1} [AddCommGroup V] [Module ℝ V] {x : V} (hx : x ≠ 0) {y : V} : y ∈ hullSingleton hx ↔ y ∈ ℝ ∙₊ x

Membership in the ray spanned by a vector is membership in its underlying cone.

@[simp]

theorem TauCeti.Toric.ToricRay.toPointedCone_eq_of_hull_singleton {V : Type u_1} [AddCommGroup V] [Module ℝ V] {x : V} (ρ : ToricRay (ℝ ∙₊ x)) : ρ.toPointedCone = ℝ ∙₊ x

A ray of the cone spanned by a vector is the whole cone: a proper face of that cone misses the spanning vector, hence is the zero cone, which is not a ray.

theorem TauCeti.Toric.ToricRay.eq_hullSingleton {V : Type u_1} [AddCommGroup V] [Module ℝ V] {x : V} (hx : x ≠ 0) (ρ : ToricRay (ℝ ∙₊ x)) : ρ = hullSingleton hx

The cone spanned by a nonzero vector has exactly one ray.

theorem TauCeti.Toric.ToricRay.toPointedCone_injective {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} : Function.Injective toPointedCone

Two rays with the same underlying cone are equal.

theorem TauCeti.Toric.ToricRay.eq_of_toPointedCone_le {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} (hσ : (↑σ).Salient) {ν ρ : ToricRay σ} (h : ν.toPointedCone ≤ ρ.toPointedCone) : ν = ρ

In a salient cone, a ray contained in another ray is equal to it: both are spanned by any nonzero point of the smaller one.

theorem TauCeti.Toric.ToricRay.toPointedCone_le_toPointedCone_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} (hσ : (↑σ).Salient) {ν ρ : ToricRay σ} : ν.toPointedCone ≤ ρ.toPointedCone ↔ ν = ρ

In a salient cone, containment of rays is equality.

Rays of a product

theorem TauCeti.Toric.ToricRay.map_fst_eq_bot_of_map_snd_ne_bot {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {V' : Type u_2} [AddCommGroup V'] [Module ℝ V'] {τ : PointedCone ℝ V'} (G : ToricRay (Submodule.prod σ τ)) (hG : (↑G.toPointedCone).Salient) (h : PointedCone.map (LinearMap.snd ℝ V V') G.toPointedCone ≠ ⊥) : PointedCone.map (LinearMap.fst ℝ V V') G.toPointedCone = ⊥

A salient ray of a product of cones cannot project nontrivially to both factors: if its projection to the second factor is nonzero, then its projection to the first factor is zero.

theorem TauCeti.Toric.ToricRay.finrank_span_map_fst_eq_one {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {V' : Type u_2} [AddCommGroup V'] [Module ℝ V'] {τ : PointedCone ℝ V'} (G : ToricRay (Submodule.prod σ τ)) (hG : (↑G.toPointedCone).Salient) (h : PointedCone.map (LinearMap.snd ℝ V V') G.toPointedCone = ⊥) : Module.finrank ℝ ↥(Submodule.span ℝ ↑(PointedCone.map (LinearMap.fst ℝ V V') G.toPointedCone)) = 1

The projection to the first factor of a salient ray of a product of cones whose projection to the second factor is the zero cone is one-dimensional, hence a ray of that factor.

theorem TauCeti.Toric.ToricRay.finrank_span_map_snd_eq_one {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {V' : Type u_2} [AddCommGroup V'] [Module ℝ V'] {τ : PointedCone ℝ V'} (G : ToricRay (Submodule.prod σ τ)) (hG : (↑G.toPointedCone).Salient) (h : PointedCone.map (LinearMap.snd ℝ V V') G.toPointedCone ≠ ⊥) : Module.finrank ℝ ↥(Submodule.span ℝ ↑(PointedCone.map (LinearMap.snd ℝ V V') G.toPointedCone)) = 1

The projection to the second factor of a salient ray of a product of cones whose projection to the second factor is not the zero cone is one-dimensional, hence a ray of that factor.

noncomputable def TauCeti.Toric.ToricRay.prodRayFst {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {V' : Type u_2} [AddCommGroup V'] [Module ℝ V'] {τ : PointedCone ℝ V'} (G : ToricRay (Submodule.prod σ τ)) (hG : (↑G.toPointedCone).Salient) (h : PointedCone.map (LinearMap.snd ℝ V V') G.toPointedCone = ⊥) : ToricRay σ

The ray of the first factor underlying a salient ray of a product of cones whose projection to the second factor is the zero cone.

@[simp]

theorem TauCeti.Toric.ToricRay.toPointedCone_prodRayFst {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {V' : Type u_2} [AddCommGroup V'] [Module ℝ V'] {τ : PointedCone ℝ V'} (G : ToricRay (Submodule.prod σ τ)) (hG : (↑G.toPointedCone).Salient) (h : PointedCone.map (LinearMap.snd ℝ V V') G.toPointedCone = ⊥) : (G.prodRayFst hG h).toPointedCone = PointedCone.map (LinearMap.fst ℝ V V') G.toPointedCone

@[simp]

theorem TauCeti.Toric.ToricRay.mem_prodRayFst {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {V' : Type u_2} [AddCommGroup V'] [Module ℝ V'] {τ : PointedCone ℝ V'} (G : ToricRay (Submodule.prod σ τ)) (hG : (↑G.toPointedCone).Salient) (h : PointedCone.map (LinearMap.snd ℝ V V') G.toPointedCone = ⊥) {x : V} : x ∈ G.prodRayFst hG h ↔ x ∈ PointedCone.map (LinearMap.fst ℝ V V') G.toPointedCone

noncomputable def TauCeti.Toric.ToricRay.prodRaySnd {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {V' : Type u_2} [AddCommGroup V'] [Module ℝ V'] {τ : PointedCone ℝ V'} (G : ToricRay (Submodule.prod σ τ)) (hG : (↑G.toPointedCone).Salient) (h : PointedCone.map (LinearMap.snd ℝ V V') G.toPointedCone ≠ ⊥) : ToricRay τ

The ray of the second factor underlying a salient ray of a product of cones whose projection to the second factor is not the zero cone.

@[simp]

theorem TauCeti.Toric.ToricRay.toPointedCone_prodRaySnd {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {V' : Type u_2} [AddCommGroup V'] [Module ℝ V'] {τ : PointedCone ℝ V'} (G : ToricRay (Submodule.prod σ τ)) (hG : (↑G.toPointedCone).Salient) (h : PointedCone.map (LinearMap.snd ℝ V V') G.toPointedCone ≠ ⊥) : (G.prodRaySnd hG h).toPointedCone = PointedCone.map (LinearMap.snd ℝ V V') G.toPointedCone

@[simp]

theorem TauCeti.Toric.ToricRay.mem_prodRaySnd {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {V' : Type u_2} [AddCommGroup V'] [Module ℝ V'] {τ : PointedCone ℝ V'} (G : ToricRay (Submodule.prod σ τ)) (hG : (↑G.toPointedCone).Salient) (h : PointedCone.map (LinearMap.snd ℝ V V') G.toPointedCone ≠ ⊥) {x : V'} : x ∈ G.prodRaySnd hG h ↔ x ∈ PointedCone.map (LinearMap.snd ℝ V V') G.toPointedCone

theorem TauCeti.Toric.ToricRay.prod_ext {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {V' : Type u_2} [AddCommGroup V'] [Module ℝ V'] {τ : PointedCone ℝ V'} {G H : ToricRay (Submodule.prod σ τ)} (h₁ : PointedCone.map (LinearMap.fst ℝ V V') G.toPointedCone = PointedCone.map (LinearMap.fst ℝ V V') H.toPointedCone) (h₂ : PointedCone.map (LinearMap.snd ℝ V V') G.toPointedCone = PointedCone.map (LinearMap.snd ℝ V V') H.toPointedCone) : G = H

A ray of a product of cones is determined by its two projections.

def TauCeti.Toric.ToricRay.prodInl {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {V' : Type u_2} [AddCommGroup V'] [Module ℝ V'] {τ : PointedCone ℝ V'} (hτ : (↑τ).Salient) (ρ : ToricRay σ) : ToricRay (Submodule.prod σ τ)

A ray of the first factor included as a ray of the product by taking its product with the zero cone in the second factor.

@[simp]

theorem TauCeti.Toric.ToricRay.toPointedCone_prodInl {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {V' : Type u_2} [AddCommGroup V'] [Module ℝ V'] {τ : PointedCone ℝ V'} (hτ : (↑τ).Salient) (ρ : ToricRay σ) : (prodInl hτ ρ).toPointedCone = Submodule.prod ρ.toPointedCone ⊥

@[simp]

theorem TauCeti.Toric.ToricRay.mem_prodInl {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {V' : Type u_2} [AddCommGroup V'] [Module ℝ V'] {τ : PointedCone ℝ V'} (hτ : (↑τ).Salient) (ρ : ToricRay σ) {x : V × V'} : x ∈ prodInl hτ ρ ↔ x.1 ∈ ρ ∧ x.2 = 0

Membership in a ray included from the first factor is coordinatewise.

def TauCeti.Toric.ToricRay.prodInr {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {V' : Type u_2} [AddCommGroup V'] [Module ℝ V'] {τ : PointedCone ℝ V'} (hσ : (↑σ).Salient) (ρ : ToricRay τ) : ToricRay (Submodule.prod σ τ)

A ray of the second factor included as a ray of the product by taking the product of the zero cone in the first factor with that ray.

@[simp]

theorem TauCeti.Toric.ToricRay.toPointedCone_prodInr {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {V' : Type u_2} [AddCommGroup V'] [Module ℝ V'] {τ : PointedCone ℝ V'} (hσ : (↑σ).Salient) (ρ : ToricRay τ) : (prodInr hσ ρ).toPointedCone = Submodule.prod ⊥ ρ.toPointedCone

@[simp]

theorem TauCeti.Toric.ToricRay.mem_prodInr {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {V' : Type u_2} [AddCommGroup V'] [Module ℝ V'] {τ : PointedCone ℝ V'} (hσ : (↑σ).Salient) (ρ : ToricRay τ) {x : V × V'} : x ∈ prodInr hσ ρ ↔ x.1 = 0 ∧ x.2 ∈ ρ

Membership in a ray included from the second factor is coordinatewise.

noncomputable def TauCeti.Toric.ToricRay.prodSplit {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {V' : Type u_2} [AddCommGroup V'] [Module ℝ V'] {τ : PointedCone ℝ V'} (hσ : (↑σ).Salient) (hτ : (↑τ).Salient) : ToricRay (Submodule.prod σ τ) ≃ ToricRay σ ⊕ ToricRay τ

The decomposition of the rays of a product of salient cones: the rays of σ.prod τ are exactly the rays of the two factors, a ray of a factor corresponding to its product with the zero cone. The two cases of the forward map are computed by TauCeti.Toric.ToricRay.prodSplit_eq_inl and TauCeti.Toric.ToricRay.prodSplit_eq_inr.

@[simp]

theorem TauCeti.Toric.ToricRay.prodSplit_eq_inl {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {V' : Type u_2} [AddCommGroup V'] [Module ℝ V'] {τ : PointedCone ℝ V'} (hσ : (↑σ).Salient) (hτ : (↑τ).Salient) (G : ToricRay (Submodule.prod σ τ)) (h : PointedCone.map (LinearMap.snd ℝ V V') G.toPointedCone = ⊥) : (prodSplit hσ hτ) G = Sum.inl (G.prodRayFst ⋯ h)

@[simp]

theorem TauCeti.Toric.ToricRay.prodSplit_eq_inr {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {V' : Type u_2} [AddCommGroup V'] [Module ℝ V'] {τ : PointedCone ℝ V'} (hσ : (↑σ).Salient) (hτ : (↑τ).Salient) (G : ToricRay (Submodule.prod σ τ)) (h : PointedCone.map (LinearMap.snd ℝ V V') G.toPointedCone ≠ ⊥) : (prodSplit hσ hτ) G = Sum.inr (G.prodRaySnd ⋯ h)

@[simp]

theorem TauCeti.Toric.ToricRay.prodSplit_symm_inl {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {V' : Type u_2} [AddCommGroup V'] [Module ℝ V'] {τ : PointedCone ℝ V'} (hσ : (↑σ).Salient) (hτ : (↑τ).Salient) (ρ : ToricRay σ) : (prodSplit hσ hτ).symm (Sum.inl ρ) = prodInl hτ ρ

@[simp]

theorem TauCeti.Toric.ToricRay.prodSplit_symm_inr {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} {V' : Type u_2} [AddCommGroup V'] [Module ℝ V'] {τ : PointedCone ℝ V'} (hσ : (↑σ).Salient) (hτ : (↑τ).Salient) (ρ : ToricRay τ) : (prodSplit hσ hτ).symm (Sum.inr ρ) = prodInr hσ ρ

theorem TauCeti.Toric.ToricRay.finite_of_fg {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} (hσ : Submodule.FG σ) : Finite (ToricRay σ)

A finitely generated pointed cone has finitely many rays. In fact finite generation alone makes its entire face lattice finite; this is inherited by the subtype of one-dimensional faces.

noncomputable def TauCeti.Toric.ToricRay.faceFinset {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ τ : PointedCone ℝ V} (hτ : τ.IsFaceOf σ) (hfg : Submodule.FG τ) : Finset (ToricRay σ)

The rays of a cone σ contained in a finitely generated face τ, as a finite set: the image of the rays of τ under faceEmbedding.

@[simp]

theorem TauCeti.Toric.ToricRay.mem_faceFinset {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ τ : PointedCone ℝ V} (hτ : τ.IsFaceOf σ) (hfg : Submodule.FG τ) {ρ : ToricRay σ} : ρ ∈ faceFinset hτ hfg ↔ ρ.toPointedCone ≤ τ

A ray of σ lies in faceFinset of a face τ exactly when it is contained in τ.

theorem TauCeti.Toric.ToricRay.faceEmbedding_mem_faceFinset {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ τ : PointedCone ℝ V} (hτ : τ.IsFaceOf σ) (hfg : Submodule.FG τ) (ρ : ToricRay τ) : (faceEmbedding hτ) ρ ∈ faceFinset hτ hfg

A ray of a face τ of σ, viewed as a ray of σ, lies in faceFinset of τ.

theorem TauCeti.Toric.ToricRay.faceFinset_eq_map {V : Type u_1} [AddCommGroup V] [Module ℝ V] {σ τ υ : PointedCone ℝ V} (hτ : τ.IsFaceOf σ) (hυτ : υ.IsFaceOf τ) (hυσ : υ.IsFaceOf σ) (hfg : Submodule.FG υ) : faceFinset hυσ hfg = Finset.map (faceEmbedding hτ) (faceFinset hυτ hfg)

For faces υ ≤ τ ≤ σ, the rays of σ contained in υ are the rays of τ contained in υ, viewed as rays of σ.