An algebra is a subalgebra of itself

Stream: new members

[Aniruddh Agarwal]

How do I make the following compile:

import data.polynomial
import ring_theory.algebra

variables (k : Type*) [field k]

def rhs : subalgebra k (polynomial k) := polynomial k

The error is:

 play.lean    16  42 error           type mismatch, term
   polynomial k
 has type
   Type u_1 : Type (max 1 (u_1+1))
 but is expected to have type
   subalgebra k (polynomial k) : Type u_1 (lean-checker)

[Aniruddh Agarwal]

In case there is a better way of doing what I'm trying to do, I'm trying to prove that a certain subset $S$ of $k[X]$ generates $k[X]$. So i wanted to set up a theorem like

theorem th : adjoin k { polynomial.X } = polynomial k := sorry

[Alex J. Best]

import data.polynomial
import ring_theory.algebra

variables (k : Type*) [field k]

open_locale classical
noncomputable theory
open algebra
instance come_on_lean : algebra k (polynomial k) := by apply_instance

theorem th : adjoin k ({ polynomial.X } : set (polynomial k)) = ⊤ :=
begin
  sorry
end

[Alex J. Best]

Its a little unfortunate that we have to remind lean that polynomial k is a k-algebra. \top means the whole algebra polynomial k as a subalgebra of itself.

[Aniruddh Agarwal]

Thank you!

[Johan Commelin]

Alex J. Best said:

Its a little unfortunate that we have to remind lean that polynomial k is a k-algebra.

Does anyone understand why this happens?