The subring generated by the coefficients of a monic factor

For a polynomial F over a commutative ring R, NotaPuente.A F is the subring generated by its coefficients. If F and G are monic and F * G has integer coefficients, then A F = A G: division by a monic polynomial stays inside any subring containing the coefficients.

Main results

• NotaPuente.coeff_divByMonic_mem: p /ₘ q has its coefficients in every subring containing those of p and of the monic q (by lifting to T[X] with Polynomial.toSubring).
• NotaPuente.A_eq_of_mul_int: the division lemma, A F = A G.
• NotaPuente.A_mul_int_monic: multiplying by a monic integer polynomial does not change A.

References

• C. Marín, Non-real orders of character values of GL(n), preprint (2026).
• C. Marín, The ring of character values depends only on the segment: SU(n), Sp(2m) and GL(n) at a torsion element, Zenodo (2026), doi:10.5281/zenodo.22847476.

noncomputable def NotaPuente.A {R : Type u_1} [CommRing R] (F : Polynomial R) : Subring R

The subring of R generated by the coefficients of F.

Equations

• NotaPuente.A F = Subring.closure ↑F.coeffs

theorem NotaPuente.A_le_iff {R : Type u_1} [CommRing R] (F : Polynomial R) (T : Subring R) : A F ≤ T ↔ ∀ (n : ℕ), F.coeff n ∈ T

A F ≤ T iff every coefficient of F lies in T.

theorem NotaPuente.coeff_mem_A {R : Type u_1} [CommRing R] (F : Polynomial R) (n : ℕ) : F.coeff n ∈ A F

theorem NotaPuente.coeff_divByMonic_mem {R : Type u_1} [CommRing R] (T : Subring R) {p q : Polynomial R} (hq : q.Monic) (hp : ∀ (n : ℕ), p.coeff n ∈ T) (hqT : ∀ (n : ℕ), q.coeff n ∈ T) (n : ℕ) : (p /ₘ q).coeff n ∈ T

Division by a monic polynomial stays inside any subring containing the coefficients.

theorem NotaPuente.coeff_map_int_mem {R : Type u_1} [CommRing R] (T : Subring R) (H : Polynomial ℤ) (n : ℕ) : (Polynomial.map (Int.castRingHom R) H).coeff n ∈ T

Coefficients of a polynomial coming from ℤ[X] lie in every subring.

theorem NotaPuente.A_le_of_mul_int {R : Type u_1} [CommRing R] {F G : Polynomial R} (hF : F.Monic) {H : Polynomial ℤ} (hFG : F * G = Polynomial.map (Int.castRingHom R) H) : A G ≤ A F

One inclusion: F monic and F * G ∈ ℤ[X] give A G ≤ A F.

theorem NotaPuente.A_eq_of_mul_int {R : Type u_1} [CommRing R] {F G : Polynomial R} (hF : F.Monic) (hG : G.Monic) {H : Polynomial ℤ} (hFG : F * G = Polynomial.map (Int.castRingHom R) H) : A F = A G

Division lemma (Lemma 2.1 of the note).

theorem NotaPuente.A_mul_int_monic {R : Type u_1} [CommRing R] (F : Polynomial R) {H : Polynomial ℤ} (hH : H.Monic) : A (F * Polynomial.map (Int.castRingHom R) H) = A F

Corollary. Multiplying by a monic integer polynomial does not change A (F need not be monic).