chore(*): use is_algebra_tower instead of algebra.comap and generalize some constructions to semirings (#3299)

`algebra.comap` is now reserved to the **creation** of new algebra instances. For assumptions of theorems / constructions, `is_algebra_tower` is the new way to do it. For example:
```lean
variables [algebra K L] [algebra L A]
lemma is_algebraic_trans (L_alg : is_algebraic K L) (A_alg : is_algebraic L A) :
  is_algebraic K (comap K L A) :=
```
is now written as:
```lean
variables [algebra K L] [algebra L A] [algebra K A] [is_algebra_tower K L A]
lemma is_algebraic_trans (L_alg : is_algebraic K L) (A_alg : is_algebraic L A) :
  is_algebraic K A :=
```

Author: kckennylau

src/algebra/lie_algebra.lean

@@ -466,8 +466,8 @@ def lie_subalgebra_of_subalgebra (A : Type v) [ring A] [algebra R A]
 { lie_mem := λ x y hx hy, by {
     change ⁅x, y⁆ ∈ A', change x ∈ A' at hx, change y ∈ A' at hy,
     rw lie_ring.of_associative_ring_bracket,
-    have hxy := subalgebra.mul_mem A' x y hx hy,
-    have hyx := subalgebra.mul_mem A' y x hy hx,
+    have hxy := A'.mul_mem hx hy,
+    have hyx := A'.mul_mem hy hx,
     exact submodule.sub_mem A'.to_submodule hxy hyx, },
   ..A'.to_submodule }
 

src/data/mv_polynomial.lean

@@ -927,6 +927,39 @@ end
 
 end total_degree
 
+section aeval
+
+/-! ### The algebra of multivariate polynomials -/
+
+variables (R : Type u) (A : Type v) (f : σ → A)
+variables [comm_semiring R] [comm_semiring 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 _ _ _
+  .. eval₂_hom (algebra_map R A) f }
+
+theorem aeval_def (p : mv_polynomial σ R) : aeval R A f p = eval₂ (algebra_map R 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 R A r := eval₂_C _ _ _
+
+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_semiring
 
 section comm_ring
@@ -1069,39 +1102,6 @@ calc (a - b).total_degree = (a + -b).total_degree                : by rw sub_eq_
 
 end total_degree
 
-section aeval
-
-/-- The algebra of multivariate polynomials. -/
-
-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 _ _ _
-  .. eval₂_hom (algebra_map R A) f }
-
-theorem aeval_def (p : mv_polynomial σ R) : aeval R A f p = eval₂ (algebra_map R 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 R A r := eval₂_C _ _ _
-
-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

@@ -1821,17 +1821,21 @@ section comm_semiring
 variables [comm_semiring R] {p q : polynomial R}
 
 section aeval
-/-- `R[X]` is the generator of the category `R-Alg`. -/
-instance polynomial (R : Type u) [comm_semiring R] : algebra R (polynomial R) :=
-{ commutes' := λ _ _, mul_comm _ _,
-  smul_def' := λ c p, (polynomial.C_mul' c p).symm,
-  .. polynomial.semimodule, .. ring_hom.of polynomial.C }
+instance algebra' (R : Type u) [comm_semiring R] (A : Type v) [semiring A] [algebra R A] :
+  algebra R (polynomial A) :=
+{ smul := λ r p, algebra_map R A r • p,
+  commutes' := λ c p, ext $ λ n,
+    show (C (algebra_map R A c) * p).coeff n = (p * C (algebra_map R A c)).coeff n,
+    by rw [coeff_C_mul, coeff_mul_C, algebra.commutes],
+  smul_def' := λ c p, (C_mul' _ _).symm,
+  .. C.comp (algebra_map R A) }
 
 variables (R) (A)
 
 -- TODO this could be generalized: there's no need for `A` to be commutative,
 -- we just need that `x` is central.
-variables [comm_ring A] [algebra R A]
+variables [comm_semiring A] [algebra R A]
+variables {B : Type*} [comm_semiring B] [algebra R B]
 variables (x : A)
 
 /-- Given a valuation `x` of the variable in an `R`-algebra `A`, `aeval R A x` is
@@ -1859,6 +1863,12 @@ begin
     rw [pow_succ', ← mul_assoc, φ.map_mul, eval₂_mul (algebra_map R A), eval₂_X, ih] }
 end
 
+theorem aeval_alg_hom (f : A →ₐ[R] B) (x : A) : aeval R B (f x) = f.comp (aeval R A x) :=
+alg_hom.ext $ λ p, by rw [eval_unique (f.comp (aeval R A x)), alg_hom.comp_apply, aeval_X, aeval_def]
+
+theorem aeval_alg_hom_apply (f : A →ₐ[R] B) (x : A) (p) : aeval R B (f x) p = f (aeval R A x p) :=
+alg_hom.ext_iff.1 (aeval_alg_hom f x) p
+
 variables [comm_ring S] {f : R →+* S}
 
 lemma is_root_of_eval₂_map_eq_zero
@@ -1874,7 +1884,7 @@ lemma is_root_of_aeval_algebra_map_eq_zero [algebra R S] {p : polynomial R}
   {r : R} (hr : aeval R S (algebra_map R S r) p = 0) : p.is_root r :=
 is_root_of_eval₂_map_eq_zero inj hr
 
-lemma dvd_term_of_dvd_eval_of_dvd_terms {z p : A} {f : polynomial A} (i : ℕ)
+lemma dvd_term_of_dvd_eval_of_dvd_terms {z p : S} {f : polynomial S} (i : ℕ)
   (dvd_eval : p ∣ f.eval z) (dvd_terms : ∀ (j ≠ i), p ∣ f.coeff j * z ^ j) :
   p ∣ f.coeff i * z ^ i :=
 begin
@@ -1891,7 +1901,7 @@ begin
     exact finsupp.not_mem_support_iff.mp hi }
 end
 
-lemma dvd_term_of_is_root_of_dvd_terms {r p : A} {f : polynomial A} (i : ℕ)
+lemma dvd_term_of_is_root_of_dvd_terms {r p : S} {f : polynomial S} (i : ℕ)
   (hr : f.is_root r) (h : ∀ (j ≠ i), p ∣ f.coeff j * r ^ j) : p ∣ f.coeff i * r ^ i :=
 dvd_term_of_dvd_eval_of_dvd_terms i (eq.symm hr ▸ dvd_zero p) h
 

src/field_theory/splitting_field.lean

@@ -289,12 +289,12 @@ splitting_field_aux.algebra n _
 
 instance algebra_tower {n : ℕ} {f : polynomial α} (hfn : f.nat_degree = n + 1) :
   is_algebra_tower α (adjoin_root f.factor) (splitting_field_aux _ _ hfn) :=
-is_algebra_tower.of_algebra_map_eq _ _ _ $ λ x, rfl
+is_algebra_tower.of_algebra_map_eq $ λ x, rfl
 
 instance algebra_tower' {n : ℕ} {f : polynomial α} (hfn : f.nat_degree = n + 1) :
   is_algebra_tower α (adjoin_root f.factor)
     (splitting_field_aux n f.remove_factor (nat_degree_remove_factor' hfn)) :=
-is_algebra_tower.of_algebra_map_eq _ _ _ $ λ x, rfl
+is_algebra_tower.of_algebra_map_eq $ λ x, rfl
 
 theorem algebra_map_succ (n : ℕ) (f : polynomial α) (hfn : f.nat_degree = n + 1) :
   by exact algebra_map α (splitting_field_aux _ _ hfn) =

src/linear_algebra/tensor_product.lean

@@ -9,15 +9,14 @@ Tensor product of modules over commutative rings.
 import group_theory.free_abelian_group
 import linear_algebra.direct_sum_module
 
-variables {R : Type*} [comm_ring R]
-variables {M : Type*} {N : Type*} {P : Type*} {Q : Type*} {S : Type*}
-variables [add_comm_group M] [add_comm_group N] [add_comm_group P] [add_comm_group Q] [add_comm_group S]
-variables [module R M] [module R N] [module R P] [module R Q] [module R S]
-include R
-
+namespace linear_map
 
+variables {R : Type*} [comm_semiring R]
+variables {M : Type*} {N : Type*} {P : Type*} {Q : Type*} {S : Type*}
 
-namespace linear_map
+variables [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [add_comm_monoid S]
+variables [semimodule R M] [semimodule R N] [semimodule R P] [semimodule R Q] [semimodule R S]
+include R
 
 variables (R)
 def mk₂ (f : M → N → P)
@@ -64,7 +63,11 @@ variables {R M N P}
 
 theorem map_zero₂ (y) : f 0 y = 0 := (flip f y).map_zero
 
-theorem map_neg₂ (x y) : f (-x) y = -f x y := (flip f y).map_neg _
+theorem map_neg₂ {R : Type*} [comm_ring R] {M N P : Type*}
+  [add_comm_group M] [add_comm_group N] [add_comm_group P]
+  [module R M] [module R N] [module R P] (f : M →ₗ[R] N →ₗ[R] P) (x y) :
+  f (-x) y = -f x y :=
+(flip f y).map_neg _
 
 theorem map_add₂ (x₁ x₂ y) : f (x₁ + x₂) y = f x₁ y + f x₂ y := (flip f y).map_add _ _
 
@@ -112,6 +115,13 @@ variables {R M}
 
 end linear_map
 
+variables {R : Type*} [comm_ring R]
+variables {M : Type*} {N : Type*} {P : Type*} {Q : Type*} {S : Type*}
+
+variables [add_comm_group M] [add_comm_group N] [add_comm_group P] [add_comm_group Q] [add_comm_group S]
+variables [module R M] [module R N] [module R P] [module R Q] [module R S]
+include R
+
 variables (M N)
 
 namespace tensor_product
@@ -236,7 +246,7 @@ instance : semimodule R (M ⊗ N) := semimodule.of_core
 (smul_tmul _ _ _).symm
 
 variables (R M N)
-def mk : M →ₗ N →ₗ M ⊗ N :=
+def mk : M →ₗ N →ₗ M ⊗[R] N :=
 linear_map.mk₂ R (⊗ₜ) add_tmul (λ c m n, by rw [smul_tmul, tmul_smul]) tmul_add tmul_smul
 variables {R M N}
 
@@ -354,7 +364,7 @@ theorem lift_compr₂ (g : P →ₗ Q) : lift (f.compr₂ g) = g.comp (lift f) :
 eq.symm $ lift.unique $ λ x y, by simp
 
 theorem lift_mk_compr₂ (f : M ⊗ N →ₗ P) : lift ((mk R M N).compr₂ f) = f :=
-by rw [lift_compr₂, lift_mk, linear_map.comp_id]
+by rw [lift_compr₂ f, lift_mk, linear_map.comp_id]
 
 @[ext]
 theorem ext {g h : (M ⊗[R] N) →ₗ[R] P}
@@ -500,7 +510,7 @@ end
 rfl
 
 /-- The tensor product of a pair of linear maps between modules. -/
-def map (f : M →ₗ[R] P) (g : N →ₗ Q) : M ⊗ N →ₗ P ⊗ Q :=
+def map (f : M →ₗ[R] P) (g : N →ₗ Q) : M ⊗ N →ₗ[R] P ⊗ Q :=
 lift $ comp (compl₂ (mk _ _ _) g) f
 
 @[simp] theorem map_tmul (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (m : M) (n : N) :