Polynomial and rational functions under the block inclusion

The block inclusion TauCeti.glBlockSucc : GL (Fin n) k →* GL (Fin (n + 1)) k replaces a matrix g by diag(g, 1). Substitution of this block matrix into a polynomial in the entries of an (n + 1)-square matrix again gives a polynomial in the entries of g. Moreover the block inclusion preserves determinants. Consequently polynomial and rational functions pull back along the inclusion.

Main results

• TauCeti.Matrix.GeneralLinearGroup.comp_glBlockSucc_mem_polynomialFunctions and TauCeti.Matrix.GeneralLinearGroup.comp_glBlockSucc_mem_rationalFunctions: polynomial and rational functions pull back along the block inclusion.

theorem TauCeti.Matrix.GeneralLinearGroup.comp_glBlockSucc_mem_polynomialFunctions {k : Type u} [CommSemiring k] {n : ℕ} {f : GL (Fin (n + 1)) k → k} (hf : f ∈ polynomialFunctions k (n + 1)) : (fun (g : GL (Fin n) k) => f ((glBlockSucc k n) g)) ∈ polynomialFunctions k n

A polynomial function pulls back to a polynomial function along the block inclusion.

theorem TauCeti.Matrix.GeneralLinearGroup.comp_glBlockSucc_mem_rationalFunctions {k : Type u} [CommRing k] {n : ℕ} {f : GL (Fin (n + 1)) k → k} (hf : f ∈ rationalFunctions k (n + 1)) : (fun (g : GL (Fin n) k) => f ((glBlockSucc k n) g)) ∈ rationalFunctions k n

A rational function pulls back to a rational function along the block inclusion. The denominator remains the same power because diag(g, 1) has determinant det g.