Lattice points of cones

The inverse image of a cone under an additive map is an additive monoid of lattice points. Membership is unchanged by multiplication by a positive integer. In particular, when a positive multiple of a primitive vector lies in the cone, the primitive vector itself lies in the cone. These statements require neither rationality nor salience, and the additive map need not be injective. The monoid construction allows ordered semirings; the positive-multiple characterizations use an ordered field.

Adapted from Mei/Geometry/Convex/Cone/LatticePoints.lean in yuma-mizuno-lean/Mei, commit 3d2e9c869ee44c41ae9c7b5c6e2042898430d0ca (Apache 2.0).

def PointedCone.latticePoints {R : Type u_1} {N : Type u_2} {V : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid N] [AddCommMonoid V] [Module R V] (σ : PointedCone R V) (i : N →+ V) : AddSubmonoid N

The additive monoid of vectors whose images under i belong to σ.

theorem PointedCone.latticePoints_def {R : Type u_1} {N : Type u_2} {V : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid N] [AddCommMonoid V] [Module R V] (σ : PointedCone R V) (i : N →+ V) : σ.latticePoints i = AddSubmonoid.comap i σ.toAddSubmonoid

The lattice-point monoid is the inverse image of the cone's additive monoid.

@[simp]

theorem PointedCone.mem_latticePoints {R : Type u_1} {N : Type u_2} {V : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid N] [AddCommMonoid V] [Module R V] {σ : PointedCone R V} {i : N →+ V} {n : N} : n ∈ σ.latticePoints i ↔ i n ∈ σ

A vector is a lattice point of a cone exactly when its image belongs to the cone.

theorem PointedCone.latticePoints_mono {R : Type u_1} {N : Type u_2} {V : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid N] [AddCommMonoid V] [Module R V] {σ τ : PointedCone R V} (h : σ ≤ τ) (i : N →+ V) : σ.latticePoints i ≤ τ.latticePoints i

Enlarging the cone enlarges its lattice-point monoid.

theorem PointedCone.latticePoints_monotone {R : Type u_1} {N : Type u_2} {V : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid N] [AddCommMonoid V] [Module R V] (i : N →+ V) : Monotone fun (σ : PointedCone R V) => σ.latticePoints i

The lattice-point monoid is monotone in the cone.

@[simp]

theorem PointedCone.latticePoints_inf {R : Type u_1} {N : Type u_2} {V : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid N] [AddCommMonoid V] [Module R V] (σ τ : PointedCone R V) (i : N →+ V) : (σ ⊓ τ).latticePoints i = σ.latticePoints i ⊓ τ.latticePoints i

Lattice points commute with intersection of cones.

theorem PointedCone.nsmul_mem_latticePoints_iff {N : Type u_2} [AddCommMonoid N] {K : Type u_4} {W : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommMonoid W] [Module K W] (σ : PointedCone K W) (i : N →+ W) {a : ℕ} (ha : 0 < a) (n : N) : a • n ∈ σ.latticePoints i ↔ n ∈ σ.latticePoints i

A positive natural multiple belongs to the lattice-point monoid exactly when the original vector does.

theorem PointedCone.zsmul_mem_latticePoints_iff {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {G : Type u_6} {U : Type u_7} [AddCommGroup G] [AddCommGroup U] [Module K U] (σ : PointedCone K U) (i : G →+ U) {a : ℤ} (ha : 0 < a) (n : G) : a • n ∈ σ.latticePoints i ↔ n ∈ σ.latticePoints i

A positive integer multiple belongs to the lattice-point monoid exactly when the original vector does.