The sum of the coordinates in a basis

For a basis b, the linear functional Module.Basis.sumCoords b sends a vector to the sum of its coordinates. For the standard basis of a monoid algebra this is the augmentation. This file records its image and kernel.

Main statements

• Module.Basis.sumCoords_surjective: the coordinate sum is surjective when the index type is nonempty.
• Module.Basis.exists_repr_ne_of_ne_zero_of_sumCoords_eq_zero: a nonzero vector whose coordinates sum to zero has two distinct coordinates, if the number of basis vectors is a regular element of the scalars.
• Module.Basis.ker_sumCoords_eq_span: the kernel of the coordinate sum is spanned by the differences of the basis vectors from a fixed one.

theorem Module.Basis.sumCoords_surjective {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Nonempty ι] (b : Basis ι R M) : Function.Surjective ⇑b.sumCoords

The sum of the coordinates is surjective when the index type is nonempty.

theorem Module.Basis.exists_repr_ne_of_ne_zero_of_sumCoords_eq_zero {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b : Basis ι R M) {v : M} (hcard : IsLeftRegular ↑(Fintype.card ι)) (hv0 : v ≠ 0) (hv : b.sumCoords v = 0) : ∃ (i : ι) (j : ι), i ≠ j ∧ (b.repr v) i ≠ (b.repr v) j

A nonzero vector whose coordinates sum to zero has two different coordinates, provided the number of basis vectors is a regular element of the scalars.

No nonemptiness assumption on ι is needed.

theorem Module.Basis.ker_sumCoords_eq_span {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] (b : Basis ι R M) (i₀ : ι) : b.sumCoords.ker = Submodule.span R (Set.range fun (i : ι) => b i - b i₀)

The kernel of the coordinate sum is spanned by the differences of the basis vectors from a fixed one.