feat(ring_theory/ideal/operations): add an instance (#6717)

This instance has been suggested by @eric-wieser in #6640.

On my machine I get a deterministic timeout in `ring_theory/finiteness` at line 325, but in principle it seems a useful instance to have. 

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/ring_theory/finiteness.lean

@@ -252,11 +252,7 @@ end
 
 /-- `R` is finitely presented as `R`-algebra. -/
 lemma self : finite_presentation R R :=
-begin
-  letI hempty := mv_polynomial R pempty,
-  exact @equiv R (_root_.mv_polynomial pempty R) R _ _ _ _ _ hempty
-    (mv_polynomial.pempty_alg_equiv R)
-end
+equiv (mv_polynomial R pempty) (mv_polynomial.pempty_alg_equiv R)
 
 variable {R}
 
@@ -278,7 +274,6 @@ lemma of_surjective {f : A →ₐ[R] B} (hf : function.surjective f) (hker : f.t
   (hfp : finite_presentation R A) : finite_presentation R B :=
 equiv (quotient hker hfp) (ideal.quotient_ker_alg_equiv_of_surjective hf)
 
-
 lemma iff : finite_presentation R A ↔
   ∃ n (I : ideal (_root_.mv_polynomial (fin n) R)) (e : I.quotient ≃ₐ[R] A), I.fg :=
 begin
@@ -323,9 +318,15 @@ begin
   refine equiv _ e.symm,
   obtain ⟨m, I, e, hfg⟩ := iff.1 hfp,
   refine equiv _ (mv_polynomial.map_alg_equiv (fin n) e),
-  letI : is_scalar_tower R (_root_.mv_polynomial (fin m) R)
-    (@ideal.map _ (_root_.mv_polynomial (fin n) (_root_.mv_polynomial (fin m) R))
-    _ _ mv_polynomial.C I).quotient := is_scalar_tower.comap,
+  -- typeclass inference seems to struggle to find this path
+  letI : is_scalar_tower R
+    (_root_.mv_polynomial (fin m) R) (_root_.mv_polynomial (fin m) R) :=
+      is_scalar_tower.right,
+  letI : is_scalar_tower R
+    (_root_.mv_polynomial (fin m) R)
+    (_root_.mv_polynomial (fin n) (_root_.mv_polynomial (fin m) R)) :=
+      mv_polynomial.is_scalar_tower,
+
   refine equiv _ ((@mv_polynomial.quotient_equiv_quotient_mv_polynomial
     _ (fin n) _ I).restrict_scalars R).symm,
   refine quotient (submodule.map_fg_of_fg I hfg _) _,
@@ -340,8 +341,6 @@ lemma trans [algebra A B] [is_scalar_tower R A B] (hfpA : finite_presentation R
   (hfpB : finite_presentation A B) : finite_presentation R B :=
 begin
   obtain ⟨n, I, e, hfg⟩ := iff.1 hfpB,
-  -- note that this unfolds `algebra.comap` from the last argument of `is_scalar_tower`
-  letI : is_scalar_tower R A I.quotient := is_scalar_tower.comap,
   exact equiv (quotient hfg (mv_polynomial_of_finite_presentation hfpA _)) (e.restrict_scalars R)
 end
 

src/ring_theory/ideal/operations.lean

@@ -1232,8 +1232,11 @@ lemma quotient.alg_map_eq (I : ideal A) :
   algebra_map R I.quotient = (algebra_map A I.quotient).comp (algebra_map R A) :=
 by simp only [ring_hom.algebra_map_to_algebra, ring_hom.comp_id]
 
-instance {I : ideal A} : is_scalar_tower R A (ideal.quotient I) :=
-is_scalar_tower.of_algebra_map_eq' (quotient.alg_map_eq R I)
+instance [algebra S A] [algebra S R] [is_scalar_tower S R A]
+  {I : ideal A} : is_scalar_tower S R (ideal.quotient I) :=
+is_scalar_tower.of_algebra_map_eq' $ by
+  rw [quotient.alg_map_eq R, quotient.alg_map_eq S, ring_hom.comp_assoc,
+    is_scalar_tower.algebra_map_eq S R A]
 
 lemma quotient.mkₐ_to_ring_hom (I : ideal A) :
   (quotient.mkₐ R I).to_ring_hom = ideal.quotient.mk I := rfl