fix(ring_theory/algebraic): prove a diamond exists and remove the ins…

…tances (#11935)

It seems nothing used these instances anyway.

src/ring_theory/algebraic.lean

@@ -279,17 +279,25 @@ section pi
 
 variables (R' : Type u) (S' : Type v) (T' : Type w)
 
-instance polynomial.has_scalar_pi [semiring R'] [has_scalar R' S'] :
+/-- This is not an instance as it forms a diamond with `pi.has_scalar`.
+
+See the `instance_diamonds` test for details. -/
+def polynomial.has_scalar_pi [semiring R'] [has_scalar R' S'] :
   has_scalar (R'[X]) (R' → S') :=
 ⟨λ p f x, eval x p • f x⟩
 
-noncomputable instance polynomial.has_scalar_pi' [comm_semiring R'] [semiring S'] [algebra R' S']
+/-- This is not an instance as it forms a diamond with `pi.has_scalar`.
+
+See the `instance_diamonds` test for details. -/
+noncomputable def polynomial.has_scalar_pi' [comm_semiring R'] [semiring S'] [algebra R' S']
   [has_scalar S' T'] :
   has_scalar (R'[X]) (S' → T') :=
 ⟨λ p f x, aeval x p • f x⟩
 
 variables {R} {S}
 
+local attribute [instance] polynomial.has_scalar_pi polynomial.has_scalar_pi'
+
 @[simp] lemma polynomial_smul_apply [semiring R'] [has_scalar R' S']
   (p : R'[X]) (f : R' → S') (x : R') :
   (p • f) x = eval x p • f x := rfl
@@ -300,7 +308,8 @@ variables {R} {S}
 
 variables [comm_semiring R'] [comm_semiring S'] [comm_semiring T'] [algebra R' S'] [algebra S' T']
 
-noncomputable instance polynomial.algebra_pi :
+/-- This is not an instance for the same reasons as `polynomial.has_scalar_pi'`. -/
+noncomputable def polynomial.algebra_pi :
   algebra (R'[X]) (S' → T') :=
 { to_fun := λ p z, algebra_map S' T' (aeval z p),
   map_one' := funext $ λ z, by simp,
@@ -311,6 +320,8 @@ noncomputable instance polynomial.algebra_pi :
   smul_def' := λ p f, funext $ λ z, by simp [algebra.algebra_map_eq_smul_one],
   ..polynomial.has_scalar_pi' R' S' T' }
 
+local attribute [instance] polynomial.algebra_pi
+
 @[simp] lemma polynomial.algebra_map_pi_eq_aeval :
   (algebra_map (R'[X]) (S' → T') : R'[X] → (S' → T')) =
     λ p z, algebra_map _ _ (aeval z p) := rfl

test/instance_diamonds.lean

@@ -9,6 +9,7 @@ import data.polynomial.basic
 import group_theory.group_action.prod
 import group_theory.group_action.units
 import data.complex.module
+import ring_theory.algebraic
 
 /-! # Tests that instances do not form diamonds -/
 
@@ -97,3 +98,35 @@ begin
 end
 
 end multiplicative
+
+/-! ## `polynomial` instances -/
+section polynomial
+
+variables (R A : Type*)
+open_locale polynomial
+open polynomial
+
+/-- `polynomial.has_scalar_pi` forms a diamond with `pi.has_scalar`. -/
+example [semiring R] [nontrivial R] :
+  polynomial.has_scalar_pi _ _ ≠ (pi.has_scalar : has_scalar R[X] (R → R[X])) :=
+begin
+  intro h,
+  simp_rw [has_scalar.ext_iff, function.funext_iff, polynomial.ext_iff] at h,
+  simpa using h X 1 1 0,
+end
+
+/-- `polynomial.has_scalar_pi'` forms a diamond with `pi.has_scalar`. -/
+example [comm_semiring R] [nontrivial R] :
+  polynomial.has_scalar_pi' _ _ _ ≠ (pi.has_scalar : has_scalar R[X] (R → R[X])) :=
+begin
+  intro h,
+  simp_rw [has_scalar.ext_iff, function.funext_iff, polynomial.ext_iff] at h,
+  simpa using h X 1 1 0,
+end
+
+/-- `polynomial.has_scalar_pi'` is consistent with `polynomial.has_scalar_pi`. -/
+example [comm_semiring R] [nontrivial R] :
+  polynomial.has_scalar_pi' _ _ _ = (polynomial.has_scalar_pi _ _ : has_scalar R[X] (R → R[X])) :=
+rfl
+
+end polynomial