Unimodular elements: unit rescaling and coordinate vectors over a local ring

Complements to Mathlib.LinearAlgebra.Unimodular. Unimodularity of an element v of an R-module (some linear functional takes the value 1 at v) is preserved by multiplication by a unit, so each unit multiple of a unimodular vector can be used as a generator when constructing projective orbit morphisms. A coordinate vector v : ι → R with a unit coordinate is unimodular. Over a local ring the converse holds for finitely many coordinates: v is unimodular exactly when one of its coordinates is a unit. This is the form in which homogeneous coordinates of points of projective schemes over a local ring are normalised.

Main results

• TauCeti.Module.isUnimodular_units_smul: multiplication by a unit preserves unimodularity.
• TauCeti.Module.isUnimodular_of_isUnit_apply: a coordinate vector with a unit coordinate is unimodular.
• TauCeti.Module.isUnimodular_iff_exists_isUnit: over a local ring, a coordinate vector with finitely many coordinates is unimodular if and only if one of its coordinates is a unit.

theorem TauCeti.Module.isUnimodular_units_smul {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (c : Rˣ) {m : M} (hm : Module.IsUnimodular R m) : Module.IsUnimodular R (c • m)

Multiplication by a unit preserves unimodularity.

theorem TauCeti.Module.isUnimodular_of_isUnit_apply {R : Type u_1} [Semiring R] {ι : Type u_3} {v : ι → R} {i : ι} (hi : IsUnit (v i)) : Module.IsUnimodular R v

A coordinate vector one of whose coordinates is a unit is unimodular.

theorem TauCeti.Module.isUnimodular_iff_exists_isUnit {R : Type u_1} {ι : Type u_2} [CommSemiring R] [IsLocalRing R] [Finite ι] {v : ι → R} : Module.IsUnimodular R v ↔ ∃ (i : ι), IsUnit (v i)

Over a local ring, a coordinate vector with finitely many coordinates is unimodular if and only if one of its coordinates is a unit.