Primitive vectors in integer modules

A vector in an integer module is primitive when an integer-valued linear functional takes the value one on it. This basis-free condition says that the cyclic submodule generated by the vector splits off a copy of ℤ. It is invariant under linear equivalence and under changing the sign of the vector.

For a free integer module, every nonzero vector is a positive integer multiple of a primitive vector. This is the coordinate-free form of dividing a nonzero integer vector by the greatest common divisor of its coordinates. It supplies primitive representatives whenever a rational ray is initially described by arbitrary nonzero lattice vectors.

Main declarations

• TauCeti.IsPrimitive: some integer-valued linear functional takes the value one on the vector.
• TauCeti.IsPrimitive.eq_one_of_eq_nsmul: a natural multiplier of a primitive vector is one.
• LinearEquiv.isPrimitive_iff: primitivity is invariant under integer-linear equivalences.
• TauCeti.exists_eq_zsmul_isPrimitive: a nonzero vector in a free integer module is a positive integer multiple of a primitive vector.
• Module.Basis.isPrimitive: a vector of an integral basis is primitive.
• TauCeti.IsPrimitive.exists_basis: conversely, a primitive vector of a finite free integer module belongs to some integral basis of it.

def TauCeti.IsPrimitive {M : Type u_1} [AddCommGroup M] [Module ℤ M] (v : M) : Prop

A vector v in an integer module is primitive when some integer-valued linear functional sends it to 1. Equivalently, the cyclic submodule generated by v splits off a copy of ℤ.

Equations

• TauCeti.IsPrimitive v = ∃ (f : M →ₗ[ℤ] ℤ), f v = 1

theorem TauCeti.isPrimitive_def {M : Type u_1} [AddCommGroup M] [Module ℤ M] {v : M} : IsPrimitive v ↔ ∃ (f : M →ₗ[ℤ] ℤ), f v = 1

A vector is primitive exactly when an integer-valued linear functional takes the value one on it. This is the introduction and elimination interface for IsPrimitive.

theorem TauCeti.IsPrimitive.ne_zero {M : Type u_1} [AddCommGroup M] [Module ℤ M] {v : M} (h : IsPrimitive v) : v ≠ 0

A primitive vector is nonzero.

theorem TauCeti.IsPrimitive.eq_one_of_eq_nsmul {M : Type u_1} [AddCommGroup M] [Module ℤ M] {v w : M} (hv : IsPrimitive v) {m : ℕ} (hvw : v = m • w) : m = 1

A primitive vector cannot be a nontrivial natural multiple of another vector.

@[simp]

theorem TauCeti.not_isPrimitive_zero {M : Type u_1} [AddCommGroup M] [Module ℤ M] : ¬IsPrimitive 0

The zero vector is not primitive.

theorem TauCeti.IsPrimitive.neg {M : Type u_1} [AddCommGroup M] [Module ℤ M] {v : M} (h : IsPrimitive v) : IsPrimitive (-v)

Primitivity is unchanged by the sign action v ↦ -v.

@[simp]

theorem TauCeti.isPrimitive_neg {M : Type u_1} [AddCommGroup M] [Module ℤ M] {v : M} : IsPrimitive (-v) ↔ IsPrimitive v

Primitivity is invariant under negation.

theorem Module.Basis.isPrimitive {ι : Type u_1} {M : Type u_2} [AddCommGroup M] [Module ℤ M] (b : Basis ι ℤ M) (j : ι) : TauCeti.IsPrimitive (b j)

A vector of an integral basis is primitive.

@[simp]

theorem LinearEquiv.isPrimitive_iff {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] [Module ℤ M] [Module ℤ N] (φ : M ≃ₗ[ℤ] N) {v : M} : TauCeti.IsPrimitive (φ v) ↔ TauCeti.IsPrimitive v

Primitivity transports along an integer-linear equivalence.

theorem TauCeti.exists_eq_zsmul_isPrimitive {M : Type u_1} [AddCommGroup M] [Module ℤ M] [Module.Free ℤ M] {v : M} (hv : v ≠ 0) : ∃ (d : ℤ) (w : M), 0 < d ∧ IsPrimitive w ∧ v = d • w

Every nonzero vector in a free integer module is a positive integer multiple of a primitive vector. The multiplier is the greatest common divisor of the coordinates in any integral basis.

theorem TauCeti.IsPrimitive.exists_basis {M : Type u_1} [AddCommGroup M] [Module ℤ M] [Module.Free ℤ M] [Module.Finite ℤ M] {v : M} (hv : IsPrimitive v) : ∃ (n : ℕ) (b : Module.Basis (Fin n) ℤ M) (j : Fin n), b j = v

A primitive vector of a finite free integer module belongs to an integral basis of it.