An injective polynomial matrix over K(t) remains injective at some integer specialization. Clearing a left inverse's denominators gives the assertion without selecting minors or assuming a generic-rank principle.
theorem
CCDN.ratFunc_matrix_common_denominator
{K : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Field K]
[Finite ι]
[Finite κ]
(B : Matrix ι κ (RatFunc K))
:
∃ (q : Polynomial K) (C : Matrix ι κ (Polynomial K)),
q ≠ 0 ∧ ∀ (i : ι) (j : κ),
(algebraMap (Polynomial K) (RatFunc K)) (C i j) = (algebraMap (Polynomial K) (RatFunc K)) q * B i j
Clear all entries of a rational-function matrix with one nonzero polynomial denominator.
theorem
CCDN.polynomial_matrix_injective_specialization
{K : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Field K]
[CharZero K]
[Finite ι]
[Fintype κ]
(A : Matrix ι κ (Polynomial K))
(hA : Function.Injective ⇑(A.map ⇑(algebraMap (Polynomial K) (RatFunc K))).mulVecLin)
:
∃ (k : ℕ), Function.Injective ⇑(A.map ⇑(Polynomial.evalRingHom ↑k)).mulVecLin
Full column rank over K(t) occurs at an integer specialization.