## Stream: new members

### Topic: An algebra is a subalgebra of itself

#### Aniruddh Agarwal (Jun 25 2020 at 03:03):

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 (Jun 25 2020 at 03:11):

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 (Jun 25 2020 at 03:23):

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 (Jun 25 2020 at 03:26):

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.

Thank you!

#### Johan Commelin (Jun 25 2020 at 04:52):

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?

Last updated: May 10 2021 at 00:31 UTC