refactor(*): move algebra below polynomial in the import chain (#2294)

* Move `algebra` below `polynomial` in the `import` chain

This PR only moves code and slightly generalizes
`mv_polynomial.aeval`.

* Fix compile

* Update src/data/mv_polynomial.lean

* Apply suggestions from code review

* Apply suggestions from code review

Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: 3 people

src/analysis/calculus/deriv.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Gabriel Ebner. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sébastien Gouëzel
 -/
-import analysis.calculus.fderiv
+import analysis.calculus.fderiv data.polynomial
 
 /-!
 

src/data/mv_polynomial.lean

@@ -931,6 +931,48 @@ eval₂.is_ring_hom _ _
 
 end map
 
+section aeval
+
+/-- The algebra of multivariate polynomials. -/
+instance mv_polynomial (R : Type u) [comm_ring R]
+  (σ : Type v) : algebra R (mv_polynomial σ R) :=
+{ to_fun := mv_polynomial.C,
+  commutes' := λ _ _, mul_comm _ _,
+  smul_def' := λ c p, (mv_polynomial.C_mul' c p).symm,
+  .. mv_polynomial.module }
+
+variables (R : Type u) (A : Type v) (f : σ → A)
+variables [comm_ring R] [comm_ring A] [algebra R A]
+
+/-- A map `σ → A` where `A` is an algebra over `R` generates an `R`-algebra homomorphism
+from multivariate polynomials over `σ` to `A`. -/
+def aeval : mv_polynomial σ R →ₐ[R] A :=
+{ commutes' := λ r, eval₂_C _ _ _
+  ..ring_hom.of (eval₂ (algebra_map A) f) }
+
+theorem aeval_def (p : mv_polynomial σ R) : aeval R A f p = eval₂ (algebra_map A) f p := rfl
+
+@[simp] lemma aeval_X (s : σ) : aeval R A f (X s) = f s := eval₂_X _ _ _
+
+@[simp] lemma aeval_C (r : R) : aeval R A f (C r) = algebra_map A r := eval₂_C _ _ _
+
+instance aeval.is_ring_hom : is_ring_hom (aeval R A f) :=
+by apply_instance
+
+theorem eval_unique (φ : mv_polynomial σ R →ₐ[R] A) :
+  φ = aeval R A (φ ∘ X) :=
+begin
+  ext p,
+  apply mv_polynomial.induction_on p,
+  { intro r, rw aeval_C, exact φ.commutes r },
+  { intros f g ih1 ih2,
+    rw [φ.map_add, ih1, ih2, alg_hom.map_add] },
+  { intros p j ih,
+    rw [φ.map_mul, alg_hom.map_mul, aeval_X, ih] }
+end
+
+end aeval
+
 end comm_ring
 
 section rename

src/data/polynomial.lean

@@ -5,7 +5,7 @@ Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 
 Theory of univariate polynomials, represented as `add_monoid_algebra α ℕ`, where α is a commutative semiring.
 -/
-import data.monoid_algebra
+import data.monoid_algebra ring_theory.algebra
 import algebra.gcd_domain ring_theory.euclidean_domain ring_theory.multiplicity
 import tactic.ring_exp
 
@@ -1347,6 +1347,46 @@ is_ring_hom.map_neg _
 @[simp] lemma eval_sub (p q : polynomial α) (x : α) : (p - q).eval x = p.eval x - q.eval x :=
 is_ring_hom.map_sub _
 
+section aeval
+/-- `R[X]` is the generator of the category `R-Alg`. -/
+instance polynomial (R : Type u) [comm_ring R] : algebra R (polynomial R) :=
+{ to_fun := polynomial.C,
+  commutes' := λ _ _, mul_comm _ _,
+  smul_def' := λ c p, (polynomial.C_mul' c p).symm,
+  .. polynomial.module }
+
+variables (R : Type u) (A : Type v)
+variables [comm_ring R] [comm_ring A] [algebra R A]
+variables (x : A)
+
+/-- Given a valuation `x` of the variable in an `R`-algebra `A`, `aeval R A x` is
+the unique `R`-algebra homomorphism from `R[X]` to `A` sending `X` to `x`. -/
+def aeval : polynomial R →ₐ[R] A :=
+{ commutes' := λ r, eval₂_C _ _,
+  ..ring_hom.of (eval₂ (algebra_map A) x) }
+
+theorem aeval_def (p : polynomial R) : aeval R A x p = eval₂ (algebra_map A) x p := rfl
+
+@[simp] lemma aeval_X : aeval R A x X = x := eval₂_X _ x
+
+@[simp] lemma aeval_C (r : R) : aeval R A x (C r) = algebra_map A r := eval₂_C _ x
+
+instance aeval.is_ring_hom : is_ring_hom (aeval R A x) :=
+by apply_instance
+
+theorem eval_unique (φ : polynomial R →ₐ[R] A) (p) :
+  φ p = eval₂ (algebra_map A) (φ X) p :=
+begin
+  apply polynomial.induction_on p,
+  { intro r, rw eval₂_C, exact φ.commutes r },
+  { intros f g ih1 ih2,
+    rw [is_ring_hom.map_add φ, ih1, ih2, eval₂_add] },
+  { intros n r ih,
+    rw [pow_succ', ← mul_assoc, is_ring_hom.map_mul φ, eval₂_mul (algebra_map A : R → A), eval₂_X, ih] }
+end
+
+end aeval
+
 lemma degree_sub_lt (hd : degree p = degree q)
   (hp0 : p ≠ 0) (hlc : leading_coeff p = leading_coeff q) :
   degree (p - q) < degree p :=

src/ring_theory/adjoin.lean

@@ -70,7 +70,7 @@ begin
 end
 
 theorem adjoin_eq_range [decidable_eq R] [decidable_eq A] :
-  adjoin R s = (mv_polynomial.aeval R A s).range :=
+  adjoin R s = (mv_polynomial.aeval R A (coe : s → A)).range :=
 le_antisymm
   (adjoin_le $ λ x hx, ⟨mv_polynomial.X ⟨x, hx⟩, mv_polynomial.eval₂_X _ _ _⟩)
   (λ x ⟨p, hp⟩, hp ▸ mv_polynomial.induction_on p

src/ring_theory/algebra.lean

@@ -6,7 +6,6 @@ Authors: Kenny Lau
 Algebra over Commutative Ring (under category)
 -/
 
-import data.polynomial data.mv_polynomial
 import data.complex.basic
 import data.matrix.basic
 import linear_algebra.tensor_product
@@ -103,21 +102,6 @@ by rw [smul_def, smul_def, left_comm]
   (r • x) * y = r • (x * y) :=
 by rw [smul_def, smul_def, mul_assoc]
 
-/-- R[X] is the generator of the category R-Alg. -/
-instance polynomial (R : Type u) [comm_ring R] : algebra R (polynomial R) :=
-{ to_fun := polynomial.C,
-  commutes' := λ _ _, mul_comm _ _,
-  smul_def' := λ c p, (polynomial.C_mul' c p).symm,
-  .. polynomial.module }
-
-/-- The algebra of multivariate polynomials. -/
-instance mv_polynomial (R : Type u) [comm_ring R]
-  (ι : Type v) : algebra R (mv_polynomial ι R) :=
-{ to_fun := mv_polynomial.C,
-  commutes' := λ _ _, mul_comm _ _,
-  smul_def' := λ c p, (mv_polynomial.C_mul' c p).symm,
-  .. mv_polynomial.module }
-
 /-- Creating an algebra from a subring. This is the dual of ring extension. -/
 instance of_subring (S : set R) [is_subring S] : algebra S R :=
 of_ring_hom subtype.val ⟨rfl, λ _ _, rfl, λ _ _, rfl⟩
@@ -319,74 +303,6 @@ def comap : algebra.comap R S A →ₐ[R] algebra.comap R S B :=
 
 end alg_hom
 
-namespace polynomial
-
-variables (R : Type u) (A : Type v)
-variables [comm_ring R] [comm_ring A] [algebra R A]
-variables (x : A)
-
-/-- A → Hom[R-Alg](R[X],A) -/
-def aeval : polynomial R →ₐ[R] A :=
-{ commutes' := λ r, eval₂_C _ _,
-  ..ring_hom.of (eval₂ (algebra_map A) x) }
-
-theorem aeval_def (p : polynomial R) : aeval R A x p = eval₂ (algebra_map A) x p := rfl
-
-@[simp] lemma aeval_X : aeval R A x X = x := eval₂_X _ x
-
-@[simp] lemma aeval_C (r : R) : aeval R A x (C r) = algebra_map A r := eval₂_C _ x
-
-instance aeval.is_ring_hom : is_ring_hom (aeval R A x) :=
-by apply_instance
-
-theorem eval_unique (φ : polynomial R →ₐ[R] A) (p) :
-  φ p = eval₂ (algebra_map A) (φ X) p :=
-begin
-  apply polynomial.induction_on p,
-  { intro r, rw eval₂_C, exact φ.commutes r },
-  { intros f g ih1 ih2,
-    rw [is_ring_hom.map_add φ, ih1, ih2, eval₂_add] },
-  { intros n r ih,
-    rw [pow_succ', ← mul_assoc, is_ring_hom.map_mul φ, eval₂_mul (algebra_map A : R → A), eval₂_X, ih] }
-end
-
-end polynomial
-
-namespace mv_polynomial
-
-variables (R : Type u) (A : Type v)
-variables [comm_ring R] [comm_ring A] [algebra R A]
-variables (σ : set A)
-
-/-- (ι → A) → Hom[R-Alg](R[ι],A) -/
-def aeval : mv_polynomial σ R →ₐ[R] A :=
-{ commutes' := λ r, eval₂_C _ _ _
-  ..ring_hom.of (eval₂ (algebra_map A) subtype.val) }
-
-theorem aeval_def (p : mv_polynomial σ R) : aeval R A σ p = eval₂ (algebra_map A) subtype.val p := rfl
-
-@[simp] lemma aeval_X (s : σ) : aeval R A σ (X s) = s := eval₂_X _ _ _
-
-@[simp] lemma aeval_C (r : R) : aeval R A σ (C r) = algebra_map A r := eval₂_C _ _ _
-
-instance aeval.is_ring_hom : is_ring_hom (aeval R A σ) :=
-by apply_instance
-
-variables (ι : Type w)
-
-theorem eval_unique (φ : mv_polynomial ι R →ₐ[R] A) (p) :
-  φ p = eval₂ (algebra_map A) (φ ∘ X) p :=
-begin
-  apply mv_polynomial.induction_on p,
-  { intro r, rw eval₂_C, exact φ.commutes r },
-  { intros f g ih1 ih2,
-    rw [is_ring_hom.map_add φ, ih1, ih2, eval₂_add] },
-  { intros p j ih,
-    rw [is_ring_hom.map_mul φ, eval₂_mul, eval₂_X, ih] }
-end
-
-end mv_polynomial
-
 namespace rat
 
 instance algebra_rat {α} [division_ring α] [char_zero α] : algebra ℚ α :=

src/ring_theory/algebra_operations.lean

@@ -6,7 +6,7 @@ Authors: Kenny Lau
 Multiplication and division of submodules of an algebra.
 -/
 
-import ring_theory.algebra algebra.pointwise
+import ring_theory.algebra ring_theory.ideals algebra.pointwise
 import tactic.chain
 import tactic.monotonicity.basic
 

src/ring_theory/free_comm_ring.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Johan Commelin
 -/
 
-import group_theory.free_abelian_group data.equiv.functor data.polynomial
+import group_theory.free_abelian_group data.equiv.functor data.mv_polynomial
 import ring_theory.ideal_operations ring_theory.free_ring
 
 noncomputable theory