algebraic independence in K-Algebras

Stream: maths

[Lennard Henze]

I want to define algebraic independence for elements

$x_1, ..., x_n$

of a K-Algebra A via injectivity of

$K[X_1, ..., X_n] \to A, X_i \mapsto x_i$

Do we already have homomorphisms of algebras?

[Reid Barton]

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

[Reid Barton]

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

[Lennard Henze]

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

[Lennard Henze]

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

[Kenny Lau]

function.injective

[Kenny Lau]

also you didn't use Y

[Chris Hughes]

(deleted)

[Lennard Henze]

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"?

[Kenny Lau]

(deleted)

[Kenny Lau]

you can right click it

[Lennard Henze]

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

[Kenny Lau]

yeah I think that works

[Lennard Henze]

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?^^

[Kenny Lau]

but you must have seen the word "embedding" somewhere

[Kenny Lau]

namely one of the inputs of mv_polynomial.eval\2

[Lennard Henze]

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

[Kenny Lau]

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

[Lennard Henze]

oh yeah makes sense!