Documentation

TauCeti.Geometry.Toric.Algebraic.Ray.Face

The faces of a regular cone are indexed by subsets of its rays #

A regular cone is the cone hull of the images of its primitive ray generators, and those images are part of a real basis of the ambient space. The faces of such a cone are therefore exactly the cones spanned by subfamilies of the primitive ray generators, and the assignment is an order isomorphism between Mathlib's face lattice of the cone and the powerset of its ray type.

Under this isomorphism a face corresponds to the set of its own rays, so a face of a regular cone is determined by, and can be prescribed by, the rays of the ambient cone that it contains. This is the combinatorial input of the orbit description of an affine toric chart: the rays of a regular cone index the coordinates of the mixed chart, a face is cut out by demanding that the coordinates of its rays vanish, and the face lattice must match the lattice of such coordinate conditions.

The subset-of-rays existence theorem is also provided directly for simplicial cones. Regularity is used only through simpliciality, and simpliciality cannot be dropped: the cone over a square in ℝ³, spanned by (1, 0, 1), (0, 1, 1), (-1, 0, 1) and (0, -1, 1), is salient with four rays, but the cone spanned by two opposite rays is not a face, so its ten faces do not exhaust the sixteen subsets of its rays.

Conversely, the cone spanned by the images of some vectors of an integral basis is regular: its rays are indexed by those vectors, which are primitive, and the basis extends them.

Main declarations #

References #

source
noncomputable def TauCeti.Toric.toricRayEquivOfLinearIndependent {V : Type u_2} [AddCommGroup V] [Module ℝ V] {C : PointedCone ℝ V} {ι : Type u_3} (v : ι → V) (hv : LinearIndependent ℝ v) (hcone : C = PointedCone.hull ℝ (Set.range v)) :
ToricRay C ≃ ι

The rays of the cone hull of a linearly independent family v : ι → V are indexed by ι: each ray is spanned by exactly one member of the family. The member attached to a ray is characterised by TauCeti.Toric.apply_mem_iff_toricRayEquivOfLinearIndependent.

Instances For
    source
    @[simp]
    theorem TauCeti.Toric.apply_mem_iff_toricRayEquivOfLinearIndependent {V : Type u_2} [AddCommGroup V] [Module ℝ V] {C : PointedCone ℝ V} {ι : Type u_3} (v : ι → V) (hv : LinearIndependent ℝ v) (hcone : C = PointedCone.hull ℝ (Set.range v)) (ρ : ToricRay C) (a : ι) :
    v a ∈ ρ ↔ a = (toricRayEquivOfLinearIndependent v hv hcone) ρ

    A member of a linearly independent family lies on a ray of the cone it generates exactly when it is the member indexing that ray.

    source
    theorem TauCeti.Toric.finrank_span_face_eq_card_rays_of_isSimplicial {V : Type u_2} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} (hσ : σ.IsSimplicial) (F : σ.Face) :
    Module.finrank ℝ ↥(Submodule.span ℝ ↑↑F) = Nat.card (ToricRay ↑F)

    The real dimension of a face of a simplicial cone is its number of rays.

    source
    theorem TauCeti.Toric.exists_face_rays_eq_of_isSimplicial {V : Type u_2} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} (hσ : σ.IsSimplicial) (A : Set (ToricRay σ)) :
    ∃ (F : σ.Face), ∀ (ρ : ToricRay σ), ρ.toPointedCone ≤ ↑F ↔ ρ ∈ A

    Any subset of the rays of a simplicial cone is exactly the set of rays contained in a face. The empty subset gives the zero face.

    source
    noncomputable def TauCeti.Toric.IsRegularCone.faceOrderIso {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 σ) :
    σ.Face ≃o Set (ToricRay σ)

    The face lattice of a regular cone is the lattice of subsets of its rays: a face is recorded by the set of rays it contains, and a set of rays spans the corresponding face.

    Instances For
      source
      theorem TauCeti.Toric.IsRegularCone.mem_faceOrderIso_iff {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 σ) (F : σ.Face) (ρ : ToricRay σ) :
      ρ ∈ (faceOrderIso hi hσ) F ↔ i (primitiveGenerator hi ⋯ ρ) ∈ F

      A ray of a regular cone lies in the subset attached to a face exactly when the image of its primitive generator lies in that face. This is not a simp lemma: faceOrderIso_apply rewrites the left-hand side, whose simp normal form is containment of the ray in the face.

      source
      @[simp]
      theorem TauCeti.Toric.IsRegularCone.faceOrderIso_symm_apply_toPointedCone {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 σ) (A : Set (ToricRay σ)) :
      ↑((faceOrderIso hi hσ).symm A) = PointedCone.hull ℝ (⇑i '' primitiveGenerator hi ⋯ '' A)

      The face of a regular cone attached to a subset of its rays is the cone spanned by the images of the primitive generators of those rays.

      source
      @[simp]
      theorem TauCeti.Toric.IsRegularCone.faceOrderIso_apply {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 σ) (F : σ.Face) :
      (faceOrderIso hi hσ) F = Set.range ⇑(ToricRay.faceEmbedding ⋯)

      The subset of rays attached to a face of a regular cone is the set of rays of that face.

      source
      theorem TauCeti.Toric.IsRegularCone.faceOrderIso_toricRay {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 σ) (ρ : ToricRay σ) :
      (faceOrderIso hi hσ) ↑ρ = {ρ}

      A ray of a regular cone, viewed as a face, contains no other ray. This is not a simp lemma: faceOrderIso_apply rewrites its left-hand side.

      source
      theorem TauCeti.Toric.IsRegularCone.finrank_span_face_eq_card_rays {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 σ) (F : σ.Face) :
      Module.finrank ℝ ↥(Submodule.span ℝ ↑↑F) = Nat.card { ρ : ToricRay σ // ρ ∈ (faceOrderIso hi hσ) F }

      The real dimension of a face of a regular cone is the number of rays it contains.

      Cones spanned by part of an integral basis #

      source
      theorem TauCeti.Toric.isRegularCone_hull_image_basis {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) {κ : Type u_3} (b : Module.Basis κ ℤ N) (A : Set κ) :
      IsRegularCone i (PointedCone.hull ℝ (⇑i '' ⇑b '' A))

      The cone spanned by the images of some vectors of an integral basis is regular, the basis extending its primitive ray generators. The cones of the standard fans, such as the coordinate cones of affine space and the cones of projective space, are of this form.