feat(data/polynomial): some lemmas about eval2 and algebra_map (#3382)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/data/polynomial.lean

@@ -572,8 +572,6 @@ end ring
 section comm_semiring
 variables [comm_semiring R] {p q r : polynomial R}
 
-local attribute [instance] coeff_coe_to_fun
-
 instance : comm_semiring (polynomial R) := add_monoid_algebra.comm_semiring
 
 section
@@ -586,8 +584,51 @@ lemma algebra_map_apply (r : R) :
   algebra_map R (polynomial A) r = C (algebra_map R A r) :=
 rfl
 
+/--
+When we have `[comm_ring R]`, the function `C` is the same as `algebra_map R (polynomial R)`.
+
+(But note that `C` is defined when `R` is not necessarily commutative, in which case
+`algebra_map` is not available.)
+-/
+lemma C_eq_algebra_map {R : Type*} [comm_ring R] (r : R) :
+  C r = algebra_map R (polynomial R) r :=
+rfl
+
 end
 
+@[simp]
+lemma alg_hom_eval₂_algebra_map
+  {R A B : Type*} [comm_ring R] [ring A] [ring B] [algebra R A] [algebra R B]
+  (p : polynomial R) (f : A →ₐ[R] B) (a : A) :
+  f (eval₂ (algebra_map R A) a p) = eval₂ (algebra_map R B) (f a) p :=
+begin
+  dsimp [eval₂, finsupp.sum],
+  simp only [f.map_sum, f.map_mul, f.map_pow, ring_hom.eq_int_cast, ring_hom.map_int_cast, alg_hom.commutes],
+end
+
+@[simp]
+lemma eval₂_algebra_map_X {R A : Type*} [comm_ring R] [ring A] [algebra R A]
+  (p : polynomial R) (f : polynomial R →ₐ[R] A) :
+  eval₂ (algebra_map R A) (f X) p = f p :=
+begin
+  conv_rhs { rw [←polynomial.sum_C_mul_X_eq p], },
+  dsimp [eval₂, finsupp.sum],
+  simp only [f.map_sum, f.map_mul, f.map_pow, ring_hom.eq_int_cast, ring_hom.map_int_cast],
+  simp [polynomial.C_eq_algebra_map],
+end
+
+@[simp]
+lemma ring_hom_eval₂_algebra_map_int {R S : Type*} [ring R] [ring S]
+  (p : polynomial ℤ) (f : R →+* S) (r : R) :
+  f (eval₂ (algebra_map ℤ R) r p) = eval₂ (algebra_map ℤ S) (f r) p :=
+alg_hom_eval₂_algebra_map p f.to_int_alg_hom r
+
+@[simp]
+lemma eval₂_algebra_map_int_X {R : Type*} [ring R] (p : polynomial ℤ) (f : polynomial ℤ →+* R) :
+  eval₂ (algebra_map ℤ R) (f X) p = f p :=
+-- Unfortunately `f.to_int_alg_hom` doesn't work here, as typeclasses don't match up correctly.
+eval₂_algebra_map_X p { commutes' := λ n, by simp, .. f }
+
 section eval
 variable {x : R}
 

src/ring_theory/algebra.lean

@@ -95,6 +95,28 @@ variables [comm_semiring R] [comm_semiring S] [semiring A] [algebra R A]
 lemma smul_def'' (r : R) (x : A) : r • x = algebra_map R A r * x :=
 algebra.smul_def' r x
 
+/--
+To prove two algebra structures on a fixed `[comm_semiring R] [semiring A]` agree,
+it suffices to check the `algebra_map`s agree.
+-/
+-- We'll later use this to show `algebra ℤ M` is a subsingleton.
+@[ext]
+lemma algebra_ext {R : Type*} [comm_semiring R] {A : Type*} [semiring A] (P Q : algebra R A)
+  (w : ∀ (r : R), by { haveI := P, exact algebra_map R A r } = by { haveI := Q, exact algebra_map R A r }) :
+  P = Q :=
+begin
+  unfreezingI { rcases P with ⟨⟨P⟩⟩, rcases Q with ⟨⟨Q⟩⟩ },
+  congr,
+  { funext r a,
+    replace w := congr_arg (λ s, s * a) (w r),
+    simp only [←algebra.smul_def''] at w,
+    apply w, },
+  { ext r,
+    exact w r, },
+  { apply proof_irrel_heq, },
+  { apply proof_irrel_heq, },
+end
+
 @[priority 200] -- see Note [lower instance priority]
 instance to_semimodule : semimodule R A :=
 { one_smul := by simp [smul_def''],
@@ -939,6 +961,13 @@ instance algebra_int : algebra ℤ R :=
   smul_def' := λ _ _, gsmul_eq_mul _ _,
   .. int.cast_ring_hom R }
 
+/--
+Promote a ring homomorphisms to a `ℤ`-algebra homomorphism.
+-/
+def ring_hom.to_int_alg_hom {R S : Type*} [ring R] [ring S] (f : R →+* S) : R →ₐ[ℤ] S :=
+{ commutes' := λ n, by simp,
+  .. f }
+
 variables {R}
 /-- A subring is a `ℤ`-subalgebra. -/
 def subalgebra_of_subring (S : set R) [is_subring S] : subalgebra ℤ R :=
@@ -953,6 +982,21 @@ def subalgebra_of_subring (S : set R) [is_subring S] : subalgebra ℤ R :=
     (λ i ih, show ((-i - 1 : ℤ) : R) ∈ S, by { rw [int.cast_sub, int.cast_one],
       exact is_add_subgroup.sub_mem S _ _ ih is_submonoid.one_mem }) }
 
+
+section
+variables {S : Type*} [ring S]
+
+instance int_algebra_subsingleton : subsingleton (algebra ℤ S) :=
+⟨λ P Q, by { ext, simp, }⟩
+end
+
+section
+variables {S : Type*} [semiring S]
+
+instance nat_algebra_subsingleton : subsingleton (algebra ℕ S) :=
+⟨λ P Q, by { ext, simp, }⟩
+end
+
 @[simp] lemma mem_subalgebra_of_subring {x : R} {S : set R} [is_subring S] :
   x ∈ subalgebra_of_subring S ↔ x ∈ S :=
 iff.rfl