Zulip Chat Archive

Am I doing this wrong? I have an ideal $I$ of $R[X]$ ( $R$ a commutative ring) and I want to consider it as an $R$ -module. I can do this with I.restrict_scalars R but for this to work I need an instance of is_scalar_tower R (polynomial R) (polynomial R), which I can make but I suspect I might be making the wrong one. Here's some failing code.

import data.polynomial.degree

open polynomial

example (A B : Type) [comm_ring A] [comm_ring B] [algebra A B] :
  is_scalar_tower A B B := infer_instance -- is_scalar_tower.right

-- Should I be doing this another way?
noncomputable instance (R : Type) [comm_ring R] : algebra R (polynomial R) :=
ring_hom.to_algebra C -- not registered as an instance. Is this a bad move?

--example (R : Type) [comm_ring R] :
--  is_scalar_tower R (polynomial R) (polynomial R) := infer_instance -- still fails

instance foo (R : Type) [comm_ring R] :
  is_scalar_tower R (polynomial R) (polynomial R) :=
begin
  convert  @is_scalar_tower.right R (polynomial R) _ _ _,
  -- ⊢ polynomial.has_scalar = smul_with_zero.to_has_scalar
  repeat {sorry}
end

example (A B M : Type) [comm_ring A] [comm_ring B] [add_comm_group M]
  [module B M] [module A M] [algebra A B] [is_scalar_tower A B M]
  (I : submodule B M) : submodule A M := I.restrict_scalars A

noncomputable example (R : Type) [comm_ring R] (I : submodule (polynomial R) (polynomial R)) :
  submodule R (polynomial R) := I.restrict_scalars R -- needs sorried instance