Zulip Chat Archive

Stream: maths

Topic: algebraic independence in K-Algebras


view this post on Zulip Lennard Henze (Oct 25 2019 at 14:39):

I want to define algebraic independence for elements

x1,...,xnx_1, ..., x_n

of a K-Algebra A via injectivity of

K[X1,...,Xn]A,XixiK[X_1, ..., X_n] \to A, X_i \mapsto x_i

Do we already have homomorphisms of algebras?

view this post on Zulip Reid Barton (Oct 25 2019 at 14:41):

We definitely have that map, it's called mv_polynomial.eval₂

view this post on Zulip Reid Barton (Oct 25 2019 at 14:43):

Also A →ₐ[K] B is a homomorphism of K-algebras

view this post on Zulip Lennard Henze (Oct 25 2019 at 14:55):

okay not quite sure how to use it jet, but i think ill figure it out! thanks!

view this post on Zulip Lennard Henze (Oct 25 2019 at 15:20):

is something like this usefull?

def is_algebraic_independent (Y : set A) : Prop :=
 <injective>  (mv_polynomial.eval\2 (algebra_map A) id)

with a def of injective substituted

view this post on Zulip Kenny Lau (Oct 25 2019 at 15:23):

function.injective

view this post on Zulip Kenny Lau (Oct 25 2019 at 15:24):

also you didn't use Y

view this post on Zulip Chris Hughes (Oct 25 2019 at 15:28):

(deleted)

view this post on Zulip Lennard Henze (Oct 25 2019 at 15:34):

giving the arguments explicit might work

@mv_polynomial.eval₂ _ A Y _ _ (algebra_map A) (@id Y)

but than I need to substitute an embedding for (@id Y)
Is there a better way to find where/how it is defined than "git-grep emb"?

view this post on Zulip Kenny Lau (Oct 25 2019 at 15:35):

(deleted)

view this post on Zulip Kenny Lau (Oct 25 2019 at 15:35):

you can right click it

view this post on Zulip Lennard Henze (Oct 25 2019 at 15:35):

my hope is, that K is implicit in the first underscore

view this post on Zulip Kenny Lau (Oct 25 2019 at 15:36):

yeah I think that works

view this post on Zulip Lennard Henze (Oct 25 2019 at 15:37):

ahh nice i did not knew that right-clicking jumps to definition, but how can i find the def of an embedding if i dont know the name?^^

view this post on Zulip Kenny Lau (Oct 25 2019 at 15:39):

but you must have seen the word "embedding" somewhere

view this post on Zulip Kenny Lau (Oct 25 2019 at 15:40):

namely one of the inputs of mv_polynomial.eval\2

view this post on Zulip Lennard Henze (Oct 25 2019 at 15:42):

mv_polynomial.eval\2 just wants a definition of a function from the index set to A, but it does not say that it is an embedding. i want to give the function by giving the natural embedding from Y to A

view this post on Zulip Kenny Lau (Oct 25 2019 at 15:43):

oh, that's just \lambda x, x : Y \to A

view this post on Zulip Lennard Henze (Oct 25 2019 at 15:43):

oh yeah makes sense!


Last updated: May 11 2021 at 16:22 UTC