feat(data/polynomial/algebra_map): aeval_tower (#9250)

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

src/algebra/algebra/tower.lean

@@ -125,15 +125,15 @@ rfl
 
 variables {R S A B}
 
-@[simp, priority 900] lemma _root_.alg_hom.commutes_of_tower (f : A →ₐ[S] B) (r : R) :
+@[simp, priority 900] lemma _root_.alg_hom.map_algebra_map (f : A →ₐ[S] B) (r : R) :
   f (algebra_map R A r) = algebra_map R B r :=
 by rw [algebra_map_apply R S A r, f.commutes, ← algebra_map_apply R S B]
 
 variables (R)
 
 @[simp, priority 900] lemma _root_.alg_hom.comp_algebra_map_of_tower (f : A →ₐ[S] B) :
   (f : A →+* B).comp (algebra_map R A) = algebra_map R B :=
-ring_hom.ext f.commutes_of_tower
+ring_hom.ext f.map_algebra_map
 
 variables (R) {S A B}
 

src/data/polynomial/algebra_map.lean

@@ -19,7 +19,8 @@ open_locale big_operators
 
 namespace polynomial
 universes u v w z
-variables {R : Type u} {S : Type v} {T : Type w} {A : Type z} {a b : R} {n : ℕ}
+variables {R : Type u} {S : Type v} {T : Type w} {A : Type z} {A' B' : Type*} {a b : R} {n : ℕ}
+variables [comm_semiring A'] [comm_semiring B']
 
 section comm_semiring
 variables [comm_semiring R] {p q r : polynomial R}
@@ -52,10 +53,23 @@ When we have `[comm_ring R]`, the function `C` is the same as `algebra_map R (po
 (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_semiring R] (r : R) :
+lemma C_eq_algebra_map (r : R) :
   C r = algebra_map R (polynomial R) r :=
 rfl
 
+variables {R}
+
+/--
+  Extensionality lemma for algebra maps out of `polynomial A'` over a smaller base ring than `A'`
+-/
+@[ext] lemma alg_hom_ext' [algebra R A'] [algebra R B']
+  {f g : polynomial A' →ₐ[R] B'}
+  (h₁ : f.comp (is_scalar_tower.to_alg_hom R A' (polynomial A')) =
+        g.comp (is_scalar_tower.to_alg_hom R A' (polynomial A')))
+  (h₂ : f X = g X) : f = g :=
+alg_hom.coe_ring_hom_injective (polynomial.ring_hom_ext'
+  (congr_arg alg_hom.to_ring_hom h₁) h₂)
+
 variable (R)
 
 /-- Algebra isomorphism between `polynomial R` and `add_monoid_algebra R ℕ`. This is just an
@@ -259,6 +273,48 @@ lemma is_root_of_aeval_algebra_map_eq_zero [algebra R S] {p : polynomial R}
   {r : R} (hr : aeval (algebra_map R S r) p = 0) : p.is_root r :=
 is_root_of_eval₂_map_eq_zero inj hr
 
+section aeval_tower
+
+variables [algebra S R] [algebra S A'] [algebra S B']
+
+/-- Version of `aeval` for defining algebra homs out of `polynomial R` over a smaller base ring
+  than `R`. -/
+def aeval_tower (f : R →ₐ[S] A') (x : A') : polynomial R →ₐ[S] A' :=
+{ commutes' := λ r, by simp [algebra_map_apply],
+  ..eval₂_ring_hom ↑f x }
+
+variables (g : R →ₐ[S] A') (y : A')
+
+@[simp] lemma aeval_tower_X : aeval_tower g y X = y := eval₂_X _ _
+
+@[simp] lemma aeval_tower_C (x : R) : aeval_tower g y (C x) = g x := eval₂_C _ _
+
+@[simp] lemma aeval_tower_comp_C : ((aeval_tower g y : polynomial R →+* A').comp C) = g :=
+ring_hom.ext $ aeval_tower_C _ _
+
+@[simp] lemma aeval_tower_algebra_map (x : R) :
+  aeval_tower g y (algebra_map R (polynomial R) x) = g x := eval₂_C _ _
+
+@[simp] lemma aeval_tower_comp_algebra_map :
+  (aeval_tower g y : polynomial R →+* A').comp (algebra_map R (polynomial R)) = g :=
+aeval_tower_comp_C _ _
+
+lemma aeval_tower_to_alg_hom (x : R) :
+  aeval_tower g y (is_scalar_tower.to_alg_hom S R (polynomial R) x) = g x :=
+aeval_tower_algebra_map _ _ _
+
+@[simp] lemma aeval_tower_comp_to_alg_hom :
+  (aeval_tower g y).comp (is_scalar_tower.to_alg_hom S R (polynomial R)) = g :=
+alg_hom.coe_ring_hom_injective $ aeval_tower_comp_algebra_map _ _
+
+@[simp] lemma aeval_tower_id : aeval_tower (alg_hom.id S S) = aeval :=
+by { ext, simp only [eval_X, aeval_tower_X, coe_aeval_eq_eval], }
+
+@[simp] lemma aeval_tower_of_id : aeval_tower (algebra.of_id S A') = aeval :=
+by { ext, simp only [aeval_X, aeval_tower_X], }
+
+end aeval_tower
+
 end comm_semiring
 
 section comm_ring