is_scalar_tower for polynomial rings

Stream: maths

[Kevin Buzzard]

How am I supposed to be doing this?

import tactic
import data.polynomial.degree
import ring_theory.noetherian

noncomputable theory

variables (R : Type) [comm_ring R]

example (I : ideal (polynomial R)) : submodule R (polynomial R) :=
-- what a mathematician would call I
submodule.restrict_scalars R I -- type class error

/-

failed to synthesize type class instance for
R : Type,
_inst_1 : comm_ring R,
I : ideal (polynomial R)
⊢ is_scalar_tower R (polynomial R) (polynomial R)

-/

-- is this what I'm supposed to be doing?
instance : algebra R (polynomial R) := by refine ring_hom.to_algebra (polynomial.C)
-- next line still fails
instance : is_scalar_tower R (polynomial R) (polynomial R) := infer_instance -- still doesn't work

[Riccardo Brasca]

You need to import data.polynomial.algebra_map, and then you have docs#polynomial.algebra_of_algebra, so instance : algebra R (polynomial R) will be there.

[Anne Baanen]

As Riccardo said just before me:

import tactic
import data.polynomial.algebra_map -- missing import
import ring_theory.noetherian

noncomputable theory

variables (R : Type) [comm_ring R]

example (I : ideal (polynomial R)) : submodule R (polynomial R) :=
-- what a mathematician would call I
submodule.restrict_scalars R I

[Kevin Buzzard]

nice -- also works in my use case. Thanks!