Unimodular elements and completion to a basis

An element v of a module is unimodular if some linear functional takes the value 1 at v. For a free module this is equivalent to the coordinates of v in any basis generating the unit ideal (for M = ℤⁿ: the gcd of the coordinates is 1, i.e. v is a primitive vector).

Main definitions

• Module.IsUnimodular R v: some linear functional takes the value 1 at v.

Main results

• Module.Basis.span_repr_eq_range_applyₗ: the coordinates of v in a basis generate the ideal of values taken at v by the linear functionals;
• Module.Basis.isUnimodular_iff_span_repr_eq_top: the coordinate characterisation of unimodularity in the free case;
• Module.IsUnimodular.exists_basis_zero_eq: a unimodular vector of a rank-two module can be completed to a basis;
• Module.Free.isUnimodular_one: in a nonzero algebra that is free as a module, 1 is unimodular.

References

• T. Y. Lam, Serre's Problem on Projective Modules.

def Module.IsUnimodular (R : Type u_1) [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (v : M) : Prop

An element v of an R-module is unimodular if some linear functional takes the value 1 at v.

Equations

• Module.IsUnimodular R v = ∃ (f : M →ₗ[R] R), f v = 1

theorem Module.isUnimodular_iff {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {v : M} : IsUnimodular R v ↔ ∃ (f : M →ₗ[R] R), f v = 1

theorem Module.isUnimodular_of_apply_eq_one {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {v : M} {f : M →ₗ[R] R} (hf : f v = 1) : IsUnimodular R v

theorem Module.Basis.span_repr_eq_range_applyₗ {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {ι : Type u_3} (b : Basis ι R M) (v : M) : Ideal.span (Set.range ⇑(b.repr v)) = (LinearMap.applyₗ v).range

The coordinates of v in a basis b generate the ideal of values taken at v by the linear functionals on M. In particular this ideal does not depend on b.

theorem Module.Basis.isUnimodular_iff_span_repr_eq_top {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {ι : Type u_3} {b : Basis ι R M} {v : M} : IsUnimodular R v ↔ Ideal.span (Set.range ⇑(b.repr v)) = ⊤

Coordinate characterisation of unimodularity in the free case: given a basis b, the coordinates of v generate the unit ideal iff v is unimodular.

theorem Module.Free.isUnimodular_one {R : Type u_1} [CommRing R] {A : Type u_2} [Ring A] [Nontrivial A] [Algebra R A] [Free R A] : IsUnimodular R 1

In a nonzero algebra that is free as a module, 1 is unimodular.

theorem Module.IsUnimodular.exists_basis_zero_eq {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Free R M] (hM : finrank R M = 2) {v : M} (hv : IsUnimodular R v) : ∃ (e : Basis (Fin 2) R M), e 0 = v

A unimodular vector of a rank-two module can be completed to a basis: it is the first vector of a basis.