Primitive generators of toric rays

A rational salient ray in an integral lattice contains a unique primitive lattice vector pointing along it. This file characterizes that vector as the primitive generator and provides a canonical choice for each ray of a toric cone.

Primitive generators give canonical integral vectors for the rays of a toric cone. They are the vectors which enter the definition of a regular cone and, later, its affine monomial coordinates.

Main declarations

• TauCeti.Toric.IsPrimitiveGenerator: a primitive lattice vector on a ray.
• TauCeti.Toric.IsToricCone.existsUnique_primitiveGenerator: every ray of a toric cone in an integral lattice has a unique primitive generator.
• TauCeti.Toric.primitiveGenerator: the resulting canonical lattice vector, with membership, nonvanishing, and primitivity lemmas.
• TauCeti.Toric.IsPrimitiveGenerator.unique: two primitive generators of the same salient ray in an integral lattice are equal.
• TauCeti.Toric.isPrimitiveGenerator_faceEmbedding and TauCeti.Toric.primitiveGenerator_faceEmbedding: being a primitive generator of a ray, and the canonical primitive generator, do not depend on which cone the ray is viewed as a face of.
• TauCeti.Toric.IsPrimitiveGenerator.prodInl and TauCeti.Toric.IsPrimitiveGenerator.prodInr: primitive generators remain primitive generators under the two inclusions into a product cone.

References

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

def TauCeti.Toric.IsPrimitiveGenerator {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] (i : N →+ V) {σ : PointedCone ℝ V} (ρ : ToricRay σ) (v : N) : Prop

A primitive lattice generator of a ray is a primitive lattice vector pointing along the ray.

theorem TauCeti.Toric.isPrimitiveGenerator_iff {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {ρ : ToricRay σ} {v : N} : IsPrimitiveGenerator i ρ v ↔ i v ∈ ρ ∧ IsPrimitive v

The characteristic property of a primitive generator.

theorem TauCeti.Toric.IsPrimitiveGenerator.mem {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {ρ : ToricRay σ} {v : N} (h : IsPrimitiveGenerator i ρ v) : i v ∈ ρ

A primitive generator points along its ray.

theorem TauCeti.Toric.IsPrimitiveGenerator.isPrimitive {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {ρ : ToricRay σ} {v : N} (h : IsPrimitiveGenerator i ρ v) : IsPrimitive v

A primitive generator is primitive.

theorem TauCeti.Toric.IsPrimitiveGenerator.ne_zero {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {ρ : ToricRay σ} {v : N} (h : IsPrimitiveGenerator i ρ v) : v ≠ 0

A primitive generator is nonzero.

@[simp]

theorem TauCeti.Toric.isPrimitiveGenerator_faceEmbedding {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hτ : τ.IsFaceOf σ) (ρ : ToricRay τ) {v : N} : IsPrimitiveGenerator i ((ToricRay.faceEmbedding hτ) ρ) v ↔ IsPrimitiveGenerator i ρ v

Being a primitive generator of a ray mentions only the cone underlying the ray, so it is unaffected by viewing a ray of a face as a ray of the ambient cone.

theorem TauCeti.Toric.IsPrimitiveGenerator.prodInl {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {N' : Type u_3} {V' : Type u_4} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} {τ : PointedCone ℝ V'} {ρ : ToricRay σ} {v : N} (hρ : IsPrimitiveGenerator i ρ v) (hτ : (↑τ).Salient) : IsPrimitiveGenerator (i.prodMap i') (ToricRay.prodInl hτ ρ) (v, 0)

A primitive generator remains a primitive generator under inclusion from the first factor of a product cone.

theorem TauCeti.Toric.IsPrimitiveGenerator.prodInr {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {N' : Type u_3} {V' : Type u_4} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} {τ : PointedCone ℝ V'} {ρ : ToricRay τ} {v : N'} (hρ : IsPrimitiveGenerator i' ρ v) (hσ : (↑σ).Salient) : IsPrimitiveGenerator (i.prodMap i') (ToricRay.prodInr hσ ρ) (0, v)

A primitive generator remains a primitive generator under inclusion from the second factor of a product cone.

theorem TauCeti.Toric.IsPrimitiveGenerator.unique {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {ρ : ToricRay σ} {v w : N} (hi : IsIntegralLattice i) (hρ : (↑ρ.toPointedCone).Salient) (hv : IsPrimitiveGenerator i ρ v) (hw : IsPrimitiveGenerator i ρ w) : v = w

A salient ray in an integral lattice has at most one primitive generator.

theorem TauCeti.Toric.IsToricCone.existsUnique_primitiveGenerator {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {ρ : ToricRay σ} (hρ : IsToricCone i ρ.toPointedCone) (hi : IsIntegralLattice i) : ∃! v : N, IsPrimitiveGenerator i ρ v

Every toric ray in an integral lattice has a unique primitive generator.

noncomputable def TauCeti.Toric.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 σ) (ρ : ToricRay σ) : N

The canonical primitive lattice generator of a ray of a toric cone.

theorem TauCeti.Toric.isPrimitiveGenerator_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 σ) (ρ : ToricRay σ) : IsPrimitiveGenerator i ρ (primitiveGenerator hi hσ ρ)

The canonical primitive generator satisfies the defining primitive-generator property.

@[simp]

theorem TauCeti.Toric.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 σ) (ρ : ToricRay σ) : i (primitiveGenerator hi hσ ρ) ∈ ρ

The image of the primitive generator lies on its ray.

@[simp]

theorem TauCeti.Toric.primitiveGenerator_isPrimitive {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 σ) (ρ : ToricRay σ) : IsPrimitive (primitiveGenerator hi hσ ρ)

The primitive generator is primitive.

@[simp]

theorem TauCeti.Toric.primitiveGenerator_ne_zero {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 σ) (ρ : ToricRay σ) : primitiveGenerator hi hσ ρ ≠ 0

The primitive generator is nonzero.

theorem TauCeti.Toric.IsPrimitiveGenerator.eq_primitiveGenerator {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {ρ : ToricRay σ} {v : N} (hv : IsPrimitiveGenerator i ρ v) (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) : v = primitiveGenerator hi hσ ρ

Every primitive generator of a ray is its canonical primitive generator.

@[simp]

theorem TauCeti.Toric.isPrimitiveGenerator_iff_eq_primitiveGenerator {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {v : N} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) (ρ : ToricRay σ) : IsPrimitiveGenerator i ρ v ↔ v = primitiveGenerator hi hσ ρ

A lattice vector is a primitive generator of a ray exactly when it is the canonical one.

@[simp]

theorem TauCeti.Toric.primitiveGenerator_faceEmbedding {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 ℝ V} (hτ : τ.IsFaceOf σ) (ρ : ToricRay τ) : primitiveGenerator hi hσ ((ToricRay.faceEmbedding hτ) ρ) = primitiveGenerator hi ⋯ ρ

The canonical primitive generator of a ray of a face τ of a toric cone σ is its canonical primitive generator as a ray of σ.