The monic polynomial with prescribed lower coefficients

A monic polynomial of degree n is exactly its n lower coefficients: the leading term is forced to be X ^ n. This file names the resulting polynomial TauCeti.Polynomial.monicOfCoeff c for a tuple c : Fin n → R, and records that reading the coefficients back off is inverse to it.

The point of naming it is that it is the object against which analytic dependence on the coefficients is stated: TauCeti/Analysis/Polynomial/SimpleRoots/Basic.lean differentiates (c, z) ↦ (monicOfCoeff c).eval z in c and z jointly, so the lower coefficients must appear as a free tuple rather than as the data of a polynomial subtype.

Main declarations

• TauCeti.Polynomial.monicOfCoeff: the monic polynomial X ^ n + ∑ i, c i * X ^ i of degree n whose n lower coefficients are c.
• TauCeti.Polynomial.monic_monicOfCoeff, TauCeti.Polynomial.natDegree_monicOfCoeff, TauCeti.Polynomial.eval_monicOfCoeff: its monicity, its degree and its values.
• TauCeti.Polynomial.coeff_monicOfCoeff and TauCeti.Polynomial.monicOfCoeff_coeff: the coefficients are read back off, and every monic polynomial of degree n arises this way, so the two constructions are mutually inverse.

Mathlib writes the same polynomial in the same shape one universe up: Polynomial.freeMonic R n, in Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean, is X ^ n + ∑ i, monomial i (MvPolynomial.X i) over MvPolynomial (Fin n) R, of which monicOfCoeff c is the specialization at c. Mathlib also has the same correspondence in bundled form, as the composite of Polynomial.monicEquivDegreeLT with Polynomial.degreeLTEquiv; monicOfCoeff c is by definition the image of c under the inverse of that composite, with the degree-< n and monic subtypes unbundled away and without the Nontrivial R that monicEquivDegreeLT carries. TauCeti.Sym.coeffEquiv is built from the bundled form, and TauCeti.Sym.toMonic_coeffEquiv_symm identifies its inverse with monicOfCoeff.

noncomputable def TauCeti.Polynomial.monicOfCoeff {R : Type u_1} [CommSemiring R] {n : ℕ} (c : Fin n → R) : Polynomial R

The monic polynomial of degree n whose n lower coefficients are c, that is, the specialization of Mathlib's Polynomial.freeMonic at the coefficient tuple c. It is the inverse of the coefficient-reading half of TauCeti.Sym.coeffEquiv, and is the natural object to state analytic dependence on the coefficients against: TauCeti.Sym.coeffEquiv_symm_apply describes the inverse chart as its root multiset.

Equations

• TauCeti.Polynomial.monicOfCoeff c = Polynomial.X ^ n + ∑ i : Fin n, (Polynomial.monomial ↑i) (c i)

@[simp]

theorem TauCeti.Polynomial.monic_monicOfCoeff {R : Type u_1} [CommSemiring R] {n : ℕ} (c : Fin n → R) : (monicOfCoeff c).Monic

The polynomial attached to a coefficient tuple is monic: its lower part has degree < n, so the term X ^ n leads.

@[simp]

theorem TauCeti.Polynomial.coeff_monicOfCoeff {R : Type u_1} [CommSemiring R] {n : ℕ} (c : Fin n → R) (i : Fin n) : (monicOfCoeff c).coeff ↑i = c i

The prescribed coefficients are read back off: this is the defining property of TauCeti.Polynomial.monicOfCoeff.

theorem TauCeti.Polynomial.eval_monicOfCoeff {R : Type u_1} [CommSemiring R] {n : ℕ} (c : Fin n → R) (z : R) : Polynomial.eval z (monicOfCoeff c) = z ^ n + ∑ i : Fin n, c i * z ^ ↑i

Evaluating the monic polynomial attached to a coefficient tuple: the leading power plus the prescribed lower part.

@[simp]

theorem TauCeti.Polynomial.map_monicOfCoeff {R : Type u_1} [CommSemiring R] {n : ℕ} {S : Type u_2} [CommSemiring S] (φ : R →+* S) (c : Fin n → R) : Polynomial.map φ (monicOfCoeff c) = monicOfCoeff fun (i : Fin n) => φ (c i)

Mapping coefficients commutes with forming the monic polynomial with prescribed lower coefficients.

@[simp]

theorem TauCeti.Polynomial.natDegree_monicOfCoeff {R : Type u_1} [CommSemiring R] {n : ℕ} [Nontrivial R] (c : Fin n → R) : (monicOfCoeff c).natDegree = n

The polynomial attached to a tuple of n coefficients has degree exactly n, the degree of its leading term X ^ n.

theorem TauCeti.Polynomial.monicOfCoeff_coeff {R : Type u_1} [CommSemiring R] {n : ℕ} [Nontrivial R] {p : Polynomial R} (hp : p.Monic) (hdeg : p.natDegree = n) : (monicOfCoeff fun (i : Fin n) => p.coeff ↑i) = p

Every monic polynomial of degree n is the monic polynomial attached to its own lower coefficients: together with TauCeti.Polynomial.coeff_monicOfCoeff this identifies the monic polynomials of degree n with the coefficient tuples.