## Stream: maths

### Topic: algebraic independence in K-Algebras

#### Lennard Henze (Oct 25 2019 at 14:39):

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 (Oct 25 2019 at 14:41):

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

#### Reid Barton (Oct 25 2019 at 14:43):

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

#### 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!

#### 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

#### Kenny Lau (Oct 25 2019 at 15:23):

function.injective

#### Kenny Lau (Oct 25 2019 at 15:24):

also you didn't use Y

(deleted)

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

(deleted)

#### Kenny Lau (Oct 25 2019 at 15:35):

you can right click it

#### Lennard Henze (Oct 25 2019 at 15:35):

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

#### Kenny Lau (Oct 25 2019 at 15:36):

yeah I think that works

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

#### Kenny Lau (Oct 25 2019 at 15:39):

but you must have seen the word "embedding" somewhere

#### Kenny Lau (Oct 25 2019 at 15:40):

namely one of the inputs of mv_polynomial.eval\2

#### 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

#### Kenny Lau (Oct 25 2019 at 15:43):

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

#### Lennard Henze (Oct 25 2019 at 15:43):

oh yeah makes sense!

Last updated: May 11 2021 at 16:22 UTC