Zulip Chat Archive

Stream: new members

Topic: An algebra is a subalgebra of itself


view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Aniruddh Agarwal (Jun 25 2020 at 03:32):

Thank you!

view this post on Zulip 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