Lifting linear independence from k to k[X]

Let M be a k[X]-module. A family in M that is linearly independent over k need not be linearly independent over k[X]. It is, provided X acts injectively on the k[X]-span of the family and the k-span of the family meets X times its k[X]-span only in zero: a relation over k[X] then has vanishing constant terms, so it can be divided by X indefinitely.

Main results

• LinearIndependent.polynomial: a k-linearly independent family is k[X]-linearly independent if X is injective on its k[X]-span and its k-span meets X times that span only in zero.

theorem LinearIndependent.polynomial {k : Type u_1} {M : Type u_2} {ι : Type u_3} [Ring k] [AddCommGroup M] [Module k M] [Module (Polynomial k) M] [IsScalarTower k (Polynomial k) M] {b : ι → M} (hli : LinearIndependent k b) (hreg : ∀ x ∈ Submodule.span (Polynomial k) (Set.range b), Polynomial.X • x = 0 → x = 0) (hdisj : ∀ z ∈ Submodule.span k (Set.range b), ∀ y ∈ Submodule.span (Polynomial k) (Set.range b), z = Polynomial.X • y → z = 0) : LinearIndependent (Polynomial k) b

A family that is linearly independent over k is linearly independent over k[X], provided X acts injectively on its k[X]-span and its k-span meets X times its k[X]-span only in zero. A relation over k[X] then has vanishing constant terms, so it can be divided by X indefinitely.