Polynomials and adjoining roots

Main results

• Algebra.instCommSemiringAdjoinSingleton, Algebra.instCommRingAdjoinSingleton: adjoining an element to a commutative (semi)ring gives a commutative (semi)ring
• Algebra.adjoin_singleton_induction: proving a fact about a : R[x] is the same as proving it for aeval x p where p is an arbitrary polynomial

@[simp]

theorem Polynomial.adjoin_X {R : Type u} [CommSemiring R] : R[X] = ⊤

theorem Algebra.adjoin_singleton_eq_range_aeval (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) : R[x] = (Polynomial.aeval x).range

@[simp]

theorem Polynomial.aeval_mem_adjoin_singleton (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] {p : Polynomial R} (x : A) : (aeval x) p ∈ R[x]

@[instance_reducible]

noncomputable instance Algebra.instCoeDepCoeAlgHomPolynomialAevalSubtypeMemSubalgebraAdjoinSingletonSet {A : Type u_2} {B : Type u_3} [CommSemiring A] [Semiring B] [Algebra A B] (x : B) (p : Polynomial A) : CoeDep B ((Polynomial.aeval x) p) ↥A[x]

Equations

• Algebra.instCoeDepCoeAlgHomPolynomialAevalSubtypeMemSubalgebraAdjoinSingletonSet x p = { coe := ⟨(Polynomial.aeval x) p, ⋯⟩ }

@[simp]

theorem Algebra.adjoin_aeval_self (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] {p : Polynomial R} (x : A) : ⟨(Polynomial.aeval x) p, ⋯⟩ = (Polynomial.aeval ⟨x, ⋯⟩) p

theorem Algebra.adjoin_mem_exists_aeval (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) {a : A} (h : a ∈ R[x]) : ∃ (p : Polynomial R), (Polynomial.aeval x) p = a

theorem Algebra.adjoin_eq_exists_aeval (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) (a : ↥R[x]) : ∃ (p : Polynomial R), (Polynomial.aeval x) p = ↑a

theorem Algebra.exists_mvPolynomial_aeval_eq_of_mem_adjoin {R : Type u_2} {A : Type u_3} {σ : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] {S : Set A} {a : A} {f : σ → A} (hS : S ⊆ Set.range f) (ha : a ∈ adjoin R S) : ∃ (p : MvPolynomial σ R), (MvPolynomial.aeval f) p = a

theorem Algebra.exists_mvPolynomial_eq_of_adjoin {R : Type u_2} {A : Type u_3} {σ : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] {S : Set A} {f : σ → A} (hS : S ⊆ Set.range f) (a : ↥(adjoin R S)) : ∃ (p : MvPolynomial σ R), (MvPolynomial.aeval f) p = ↑a

theorem Algebra.adjoin_singleton_induction (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) {M : ↥R[x] → Prop} (a : ↥R[x]) (f : ∀ (p : Polynomial R), M ⟨(Polynomial.aeval x) p, ⋯⟩) : M a

Proving a fact about a : R[x] is the same as proving it for aeval x p where pis an arbitrary polynomial.

@[instance_reducible]

instance Algebra.instCommSemiringAdjoinSingleton (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) : CommSemiring ↥R[x]

Equations

• Algebra.instCommSemiringAdjoinSingleton R x = { toSemiring := R[x].toSemiring, mul_comm := ⋯ }

@[instance_reducible]

instance Algebra.instCommRingAdjoinSingleton {R : Type u_2} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] (x : A) : CommRing ↥R[x]

Equations

• Algebra.instCommRingAdjoinSingleton x = { toRing := R[x].toRing, mul_comm := ⋯ }