Mathlib.RingTheory.Adjoin.Polynomial

Module docstring

{"# Polynomials and adjoining roots

Main results

Polynomial.instCommSemiringAdjoinSingleton, instCommRingAdjoinSingleton: adjoining an element to a commutative (semi)ring gives a commutative (semi)ring "}

Polynomial.adjoin_X theorem

: Algebra.adjoin R ({ X } : Set R[X]) = ⊤

Full source

@[simp]
theorem adjoin_X : Algebra.adjoin R ({X} : Set R[X]) = ⊤ := by
  refine top_unique fun p _hp => ?_
  set S := Algebra.adjoin R ({X} : Set R[X])
  rw [← sum_monomial_eq p]; simp only [← smul_X_eq_monomial, Sum]
  exact S.sum_mem fun n _hn => S.smul_mem (S.pow_mem (Algebra.subset_adjoin rfl) _) _

Adjoining Polynomial Variable Generates Full Polynomial Ring: $\text{adjoin}_R(\{X\}) = R[X]$

Informal description

The algebra generated by adjoining the polynomial variable $X$ to a commutative (semi)ring $R$ is equal to the entire polynomial ring $R[X]$, i.e., $\text{Algebra.adjoin}_R(\{X\}) = \top$.

Algebra.adjoin_singleton_eq_range_aeval theorem

(x : A) : Algebra.adjoin R { x } = (Polynomial.aeval x).range

Full source

theorem _root_.Algebra.adjoin_singleton_eq_range_aeval (x : A) :
    Algebra.adjoin R {x} = (Polynomial.aeval x).range := by
  rw [← Algebra.map_top, ← adjoin_X, AlgHom.map_adjoin, Set.image_singleton, aeval_X]

Adjoined Singleton Equals Range of Polynomial Evaluation: $\text{adjoin}_R(\{x\}) = \text{range}(\text{aeval}_x)$

Informal description

For any commutative (semi)ring $R$ and any element $x$ in an $R$-algebra $A$, the algebra generated by $R$ and the singleton set $\{x\}$ is equal to the range of the polynomial evaluation map $\text{aeval}_x : R[X] \to A$, i.e., \[ \text{Algebra.adjoin}_R(\{x\}) = \text{range}(\text{aeval}_x). \]

Polynomial.aeval_mem_adjoin_singleton theorem

: aeval x p ∈ Algebra.adjoin R { x }

Full source

@[simp]
theorem aeval_mem_adjoin_singleton :
    aevalaeval x p ∈ Algebra.adjoin R {x} := by
  simpa only [Algebra.adjoin_singleton_eq_range_aeval] using Set.mem_range_self p

Polynomial Evaluation Belongs to Adjoined Singleton Algebra

Informal description

For any commutative (semi)ring $R$, any $R$-algebra $A$, any element $x \in A$, and any polynomial $p \in R[X]$, the evaluation of $p$ at $x$ via the algebra homomorphism $\text{aeval}_x$ belongs to the algebra generated by $R$ and $\{x\}$, i.e., \[ \text{aeval}_x(p) \in \text{Algebra.adjoin}_R(\{x\}). \]

Polynomial.instCommSemiringAdjoinSingleton instance

: CommSemiring <| Algebra.adjoin R { x }

Full source

instance instCommSemiringAdjoinSingleton :
    CommSemiring <| Algebra.adjoin R {x} :=
  { mul_comm := fun ⟨p, hp⟩ ⟨q, hq⟩ ↦ by
      obtain ⟨p', rfl⟩ := Algebra.adjoin_singleton_eq_range_aeval R x ▸ hp
      obtain ⟨q', rfl⟩ := Algebra.adjoin_singleton_eq_range_aeval R x ▸ hq
      simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MulMemClass.mk_mul_mk, ← map_mul,
        mul_comm p' q'] }

Commutative Semiring Structure on Adjoined Singleton

Informal description

For any commutative semiring $R$ and $R$-algebra $A$, the algebra generated by $R$ and a single element $x \in A$ forms a commutative semiring.

Polynomial.instCommRingAdjoinSingleton instance

{R A : Type*} [CommRing R] [Ring A] [Algebra R A] (x : A) : CommRing <| Algebra.adjoin R { x }

Full source

instance instCommRingAdjoinSingleton {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (x : A) :
    CommRing <| Algebra.adjoin R {x} :=
  { mul_comm := mul_comm }

Commutative Ring Structure on Algebra Adjoining a Singleton

Informal description

For any commutative ring $R$, ring $A$ with an $R$-algebra structure, and element $x \in A$, the algebra generated by $R$ and $\{x\}$ forms a commutative ring.