Mathlib.Algebra.Polynomial.Monomial

Polynomial.monomial_one_eq_iff theorem

[Nontrivial R] {i j : ℕ} : (monomial i 1 : R[X]) = monomial j 1 ↔ i = j

Full source

theorem monomial_one_eq_iff [Nontrivial R] {i j : ℕ} :
    (monomial i 1 : R[X]) = monomial j 1 ↔ i = j := by
  simp_rw [← ofFinsupp_single, ofFinsupp.injEq]
  exact AddMonoidAlgebra.of_injective.eq_iff

Monomial Equality Criterion: $X^i = X^j \leftrightarrow i = j$

Informal description

Let $R$ be a nontrivial semiring. For any natural numbers $i$ and $j$, the monomials $X^i$ and $X^j$ in the polynomial ring $R[X]$ are equal if and only if $i = j$.

Polynomial.infinite instance

[Nontrivial R] : Infinite R[X]

Full source

instance infinite [Nontrivial R] : Infinite R[X] :=
  Infinite.of_injective (fun i => monomial i 1) fun m n h => by simpa [monomial_one_eq_iff] using h

Polynomial Rings over Nontrivial Semirings are Infinite

Informal description

For any nontrivial semiring $R$, the polynomial ring $R[X]$ is infinite.

Polynomial.card_support_le_one_iff_monomial theorem

{f : R[X]} : Finset.card f.support ≤ 1 ↔ ∃ n a, f = monomial n a

Full source

theorem card_support_le_one_iff_monomial {f : R[X]} :
    Finset.cardFinset.card f.support ≤ 1 ↔ ∃ n a, f = monomial n a := by
  constructor
  · intro H
    rw [Finset.card_le_one_iff_subset_singleton] at H
    rcases H with ⟨n, hn⟩
    refine ⟨n, f.coeff n, ?_⟩
    ext i
    by_cases hi : i = n
    · simp [hi, coeff_monomial]
    · have : f.coeff i = 0 := by
        rw [← not_mem_support_iff]
        exact fun hi' => hi (Finset.mem_singleton.1 (hn hi'))
      simp [this, Ne.symm hi, coeff_monomial]
  · rintro ⟨n, a, rfl⟩
    rw [← Finset.card_singleton n]
    apply Finset.card_le_card
    exact support_monomial' _ _

Characterization of Monomials via Support Cardinality: $\#\text{supp}(f) \leq 1 \leftrightarrow f$ is a monomial

Informal description

For any polynomial $f$ over a semiring $R$, the cardinality of its support (the set of exponents with nonzero coefficients) is at most 1 if and only if $f$ is a monomial, i.e., there exists a natural number $n$ and an element $a \in R$ such that $f = aX^n$.

Polynomial.ringHom_ext theorem

{S} [Semiring S] {f g : R[X] →+* S} (h₁ : ∀ a, f (C a) = g (C a)) (h₂ : f X = g X) : f = g

Full source

theorem ringHom_ext {S} [Semiring S] {f g : R[X]R[X] →+* S} (h₁ : ∀ a, f (C a) = g (C a))
    (h₂ : f X = g X) : f = g := by
  set f' := f.comp (toFinsuppIso R).symm.toRingHom with hf'
  set g' := g.comp (toFinsuppIso R).symm.toRingHom with hg'
  have A : f' = g' := by
    ext
    simp [f', g', h₁, RingEquiv.toRingHom_eq_coe]
    simpa using h₂
  have B : f = f'.comp (toFinsuppIso R) := by
    rw [hf', RingHom.comp_assoc]
    ext x
    simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.symm_apply_apply, Function.comp_apply,
      RingHom.coe_comp, RingEquiv.coe_toRingHom]
  have C' : g = g'.comp (toFinsuppIso R) := by
    rw [hg', RingHom.comp_assoc]
    ext x
    simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.symm_apply_apply, Function.comp_apply,
      RingHom.coe_comp, RingEquiv.coe_toRingHom]
  rw [B, C', A]

Extensionality of Ring Homomorphisms on Polynomial Rings via Constant and Variable Evaluation

Informal description

Let $R$ and $S$ be semirings, and let $f, g \colon R[X] \to S$ be ring homomorphisms from the polynomial ring over $R$ to $S$. If: 1. $f$ and $g$ agree on all constant polynomials (i.e., $f(C(a)) = g(C(a))$ for all $a \in R$), and 2. $f(X) = g(X)$ where $X$ is the polynomial variable, then $f = g$.

Polynomial.ringHom_ext' theorem

{S} [Semiring S] {f g : R[X] →+* S} (h₁ : f.comp C = g.comp C) (h₂ : f X = g X) : f = g

Full source

@[ext high]
theorem ringHom_ext' {S} [Semiring S] {f g : R[X]R[X] →+* S} (h₁ : f.comp C = g.comp C)
    (h₂ : f X = g X) : f = g :=
  ringHom_ext (RingHom.congr_fun h₁) h₂

Extensionality of Ring Homomorphisms on Polynomial Rings via Composition and Variable Evaluation

Informal description

Let $R$ and $S$ be semirings, and let $f, g \colon R[X] \to S$ be ring homomorphisms from the polynomial ring over $R$ to $S$. If: 1. The compositions of $f$ and $g$ with the constant polynomial embedding $C \colon R \to R[X]$ are equal (i.e., $f \circ C = g \circ C$), and 2. $f(X) = g(X)$, where $X$ is the polynomial variable, then $f = g$.