Polynomials with degree strictly less than n

This file contains the properties of the submodule of polynomials of degree less than n in a (semi)ring R, denoted R[X]_n.

Main definitions/lemmas

• degreeLT.basis R n: a basis for R[X]_n the submodule of polynomials with degree < n, given by the monomials X^i for i < n.

• degreeLT.basisProd R m n: a basis for R[X]_m × R[X]_n, which is the sum of two instances of the basis given above.

• degreeLT.addLinearEquiv R m n: an isomorphism between R[X]_(m + n) and R[X]_m × R[X]_n, given by the fact that the bases are both indexed by Fin (m + n). This is used for the Sylvester matrix, which is the matrix representing the Sylvester map between these two spaces, in a future file.

• taylorLinear r n: The linear automorphism induced by taylor r on R[X]_n which sends X to X + r and preserves degrees.

def Polynomial.«term_[X]__» : Lean.TrailingParserDescr

The R-submodule of R[X] consisting of polynomials of degree < n.

noncomputable def Polynomial.degreeLT.basis (R : Type u_1) [Semiring R] (n : ℕ) : Module.Basis (Fin n) R ↥(degreeLT R n)

Basis for R[X]_n given by X^i with i < n.

instance Polynomial.degreeLT.instFiniteSubtypeMemSubmodule {R : Type u_1} [Semiring R] {n : ℕ} : Module.Finite R ↥(degreeLT R n)

instance Polynomial.degreeLT.instFreeSubtypeMemSubmodule {R : Type u_1} [Semiring R] {n : ℕ} : Module.Free R ↥(degreeLT R n)

@[simp]

theorem Polynomial.degreeLT.basis_repr {R : Type u_1} [Semiring R] {n : ℕ} (i : Fin n) (P : ↥(degreeLT R n)) : ((basis R n).repr P) i = (↑P).coeff ↑i

@[simp]

theorem Polynomial.degreeLT.basis_val {R : Type u_1} [Semiring R] {n : ℕ} (i : Fin n) : ↑((basis R n) i) = X ^ ↑i

noncomputable def Polynomial.degreeLT.basisProd (R : Type u_1) [Semiring R] (m n : ℕ) : Module.Basis (Fin (m + n)) R (↥(degreeLT R m) × ↥(degreeLT R n))

Basis for R[X]_m × R[X]_n.

@[simp]

theorem Polynomial.degreeLT.basisProd_castAdd {R : Type u_1} [Semiring R] (m n : ℕ) (i : Fin m) : (basisProd R m n) (Fin.castAdd n i) = ((basis R m) i, 0)

@[simp]

theorem Polynomial.degreeLT.basisProd_natAdd {R : Type u_1} [Semiring R] (m n : ℕ) (i : Fin n) : (basisProd R m n) (Fin.natAdd m i) = (0, (basis R n) i)

noncomputable def Polynomial.degreeLT.addLinearEquiv (R : Type u_1) [Semiring R] (m n : ℕ) : ↥(degreeLT R (m + n)) ≃ₗ[R] ↥(degreeLT R m) × ↥(degreeLT R n)

An isomorphism between R[X]_(m + n) and R[X]_m × R[X]_n given by the fact that the bases are both indexed by Fin (m + n).

theorem Polynomial.degreeLT.addLinearEquiv_castAdd {R : Type u_1} [Semiring R] {m n : ℕ} (i : Fin m) : (addLinearEquiv R m n) ((basis R (m + n)) (Fin.castAdd n i)) = ((basis R m) i, 0)

theorem Polynomial.degreeLT.addLinearEquiv_natAdd {R : Type u_1} [Semiring R] {m n : ℕ} (i : Fin n) : (addLinearEquiv R m n) ((basis R (m + n)) (Fin.natAdd m i)) = (0, (basis R n) i)

theorem Polynomial.degreeLT.addLinearEquiv_symm_apply_inl_basis {R : Type u_1} [Semiring R] {m n : ℕ} (i : Fin m) : (addLinearEquiv R m n).symm ((LinearMap.inl R ↥(degreeLT R m) ↥(degreeLT R n)) ((basis R m) i)) = (basis R (m + n)) (Fin.castAdd n i)

theorem Polynomial.degreeLT.addLinearEquiv_symm_apply_inr_basis {R : Type u_1} [Semiring R] {m n : ℕ} (j : Fin n) : (addLinearEquiv R m n).symm ((LinearMap.inr R ↥(degreeLT R m) ↥(degreeLT R n)) ((basis R n) j)) = (basis R (m + n)) (Fin.natAdd m j)

theorem Polynomial.degreeLT.addLinearEquiv_symm_apply_inl {R : Type u_1} [Semiring R] {m n : ℕ} (P : ↥(degreeLT R m)) : ↑((addLinearEquiv R m n).symm ((LinearMap.inl R ↥(degreeLT R m) ↥(degreeLT R n)) P)) = ↑P

theorem Polynomial.degreeLT.addLinearEquiv_symm_apply_inr {R : Type u_1} [Semiring R] {m n : ℕ} (Q : ↥(degreeLT R n)) : ↑((addLinearEquiv R m n).symm ((LinearMap.inr R ↥(degreeLT R m) ↥(degreeLT R n)) Q)) = ↑Q * X ^ m

theorem Polynomial.degreeLT.addLinearEquiv_symm_apply {R : Type u_1} [Semiring R] {m n : ℕ} (PQ : ↥(degreeLT R m) × ↥(degreeLT R n)) : ↑((addLinearEquiv R m n).symm PQ) = ↑PQ.1 + ↑PQ.2 * X ^ m

theorem Polynomial.degreeLT.addLinearEquiv_symm_apply' {R : Type u_1} [Semiring R] {m n : ℕ} (PQ : ↥(degreeLT R m) × ↥(degreeLT R n)) : ↑((addLinearEquiv R m n).symm PQ) = ↑PQ.1 + X ^ m * ↑PQ.2

theorem Polynomial.degreeLT.addLinearEquiv_apply' {m n : ℕ} {R : Type u_2} [Ring R] (f : ↥(degreeLT R (m + n))) : ↑((addLinearEquiv R m n) f).1 = ↑f %ₘ X ^ m ∧ ↑((addLinearEquiv R m n) f).2 = ↑f /ₘ X ^ m

theorem Polynomial.degreeLT.addLinearEquiv_apply_fst {m n : ℕ} {R : Type u_2} [Ring R] (f : ↥(degreeLT R (m + n))) : ↑((addLinearEquiv R m n) f).1 = ↑f %ₘ X ^ m

theorem Polynomial.degreeLT.addLinearEquiv_apply_snd {m n : ℕ} {R : Type u_2} [Ring R] (f : ↥(degreeLT R (m + n))) : ↑((addLinearEquiv R m n) f).2 = ↑f /ₘ X ^ m

theorem Polynomial.degreeLT.addLinearEquiv_apply {m n : ℕ} {R : Type u_2} [Ring R] (f : ↥(degreeLT R (m + n))) : (addLinearEquiv R m n) f = (⟨↑f %ₘ X ^ m, ⋯⟩, ⟨↑f /ₘ X ^ m, ⋯⟩)

@[simp]

theorem Polynomial.taylor_mem_degreeLT {R : Type u_1} [CommRing R] {r : R} {n : ℕ} {f : Polynomial R} : (taylor r) f ∈ degreeLT R n ↔ f ∈ degreeLT R n

theorem Polynomial.comap_taylorEquiv_degreeLT {R : Type u_1} [CommRing R] {r : R} {n : ℕ} : Submodule.comap (taylorEquiv r) (degreeLT R n) = degreeLT R n

theorem Polynomial.map_taylorEquiv_degreeLT {R : Type u_1} [CommRing R] {r : R} {n : ℕ} : Submodule.map (taylorEquiv r) (degreeLT R n) = degreeLT R n

noncomputable def Polynomial.taylorLinearEquiv {R : Type u_1} [CommRing R] (r : R) (n : ℕ) : ↥(degreeLT R n) ≃ₗ[R] ↥(degreeLT R n)

The map taylor r induces an automorphism of the module R[X]_n of polynomials of degree < n.

@[simp]

theorem Polynomial.taylorLinearEquiv_apply_coe {R : Type u_1} [CommRing R] (r : R) (n : ℕ) (a✝ : ↥(degreeLT R n)) : ↑((taylorLinearEquiv r n) a✝) = ↑(((↑(taylorEquiv r)).submoduleMap (degreeLT R n)) a✝)

@[simp]

theorem Polynomial.taylorLinearEquiv_symm {R : Type u_1} [CommRing R] {n : ℕ} (r : R) : (taylorLinearEquiv r n).symm = taylorLinearEquiv (-r) n

@[simp]

theorem Polynomial.det_taylorLinearEquiv_toLinearMap {R : Type u_1} [CommRing R] {r : R} {n : ℕ} : LinearMap.det ↑(taylorLinearEquiv r n) = 1

@[simp]

theorem Polynomial.det_taylorLinearEquiv {R : Type u_1} [CommRing R] {r : R} {n : ℕ} : LinearEquiv.det (taylorLinearEquiv r n) = 1