feat(data/polynomial): ext lemmas for homomorphisms from `polynomial …

…R` (#4823)

src/data/polynomial/algebra_map.lean

@@ -106,6 +106,9 @@ def aeval : polynomial R →ₐ[R] A :=
 
 variables {R A}
 
+@[ext] lemma alg_hom_ext {f g : polynomial R →ₐ[R] A} (h : f X = g X) : f = g :=
+by { ext, exact h }
+
 theorem aeval_def (p : polynomial R) : aeval x p = eval₂ (algebra_map R A) x p := rfl
 
 @[simp] lemma aeval_zero : aeval x (0 : polynomial R) = 0 :=

src/data/polynomial/basic.lean

@@ -107,6 +107,21 @@ finsupp.ext_iff
 @[ext] lemma ext {p q : polynomial R} : (∀ n, coeff p n = coeff q n) → p = q :=
 finsupp.ext
 
+@[ext] lemma add_hom_ext' {M : Type*} [add_monoid M] {f g : polynomial R →+ M}
+  (h : ∀ n, f.comp (monomial n).to_add_monoid_hom = g.comp (monomial n).to_add_monoid_hom) :
+  f = g :=
+finsupp.add_hom_ext' h
+
+lemma add_hom_ext {M : Type*} [add_monoid M] {f g : polynomial R →+ M}
+  (h : ∀ n a, f (monomial n a) = g (monomial n a)) :
+  f = g :=
+finsupp.add_hom_ext h
+
+@[ext] lemma lhom_ext' {M : Type*} [add_comm_monoid M] [semimodule R M] {f g : polynomial R →ₗ[R] M}
+  (h : ∀ n, f.comp (monomial n) = g.comp (monomial n)) :
+  f = g :=
+finsupp.lhom_ext' h
+
 -- this has the same content as the subsingleton
 lemma eq_zero_of_eq_zero (h : (0 : R) = (1 : R)) (p : polynomial R) : p = 0 :=
 by rw [←one_smul R p, ←h, zero_smul]

src/data/polynomial/monomial.lean

@@ -88,4 +88,12 @@ calc monomial n a = monomial n (a * 1) : by simp
   ... = a • monomial n 1 : (smul_single' _ _ _).symm
   ... = a • X^n  : by rw X_pow_eq_monomial
 
+lemma ring_hom_ext {S} [semiring S] {f g : polynomial R →+* S}
+  (h₁ : ∀ a, f (C a) = g (C a)) (h₂ : f X = g X) : f = g :=
+by { ext, exacts [h₁ _, h₂] }
+
+@[ext] lemma ring_hom_ext' {S} [semiring S] {f g : polynomial R →+* S}
+  (h₁ : f.comp C = g.comp C) (h₂ : f X = g X) : f = g :=
+ring_hom_ext (ring_hom.congr_fun h₁) h₂
+
 end polynomial