# Zulip Chat Archive

## Stream: new members

### Topic: structure vs class

#### Jonas Wildberger (Aug 21 2020 at 09:20):

Hello everyone,

I am relatively new to lean and therefore tried to find a hopefully rather simple topic. Therefore I am now trying to define the annihilator of a linear operator and show that it is an ideal.

My definition is the following:

```
universes u v
section
variables (n: Type u) [decidable_eq n] [fintype n] (K: Type v) [field K]
def annihilator' (M: matrix n n K):= {p : polynomial K // (p.map (algebra_map K (matrix n n K))).eval M = 0}
end
```

I am aware that there are generalizations to this definition, but I thought I could work on generalizations once the basic functionality works.

So I was wondering if

- the definition works so far and
- what is the syntax for showing that this set is an ideal? The instance command seems not suitable because an ideal in a ring $R$ is implemented as an $R$-submodule in $R$ which is defined as a structure rather than a class.

Thanks in advance

#### Kenny Lau (Aug 21 2020 at 09:23):

`eval map algebra_map`

is basically `aeval`

right

#### Kenny Lau (Aug 21 2020 at 09:23):

also this is not a set: a set uses `|`

instead of `//`

#### Kenny Lau (Aug 21 2020 at 09:23):

also we can't say "this set is an ideal", but rather "here's an ideal whose underlying set is this set"

#### Kenny Lau (Aug 21 2020 at 09:24):

so it would start with:

```
def annihilator (M : matrix n n K) : ideal (polynomial K) :=
{ carrier := annihilator' n K M,
add_mem' := _,
zero_mem' := _,
smul_mem' := _ }
```

#### Kenny Lau (Aug 21 2020 at 09:25):

oh and as `aeval`

is an algebra hom, you can coerce it to a ring hom, and then just take the kernel, and you will have your ideal

#### Kenny Lau (Aug 21 2020 at 09:26):

if `[expr]`

is an algebra hom, you can coerce it to a ring hom by typing `([expr] : [source] \to+* [target])`

#### Kenny Lau (Aug 21 2020 at 09:26):

we call this a type ascription, i.e. announcing that `[expr]`

has type `[expr2]`

by writing `([expr] : [expr2])`

#### Kenny Lau (Aug 21 2020 at 09:26):

the kernel is `ring_hom.kernel`

#### Jonas Wildberger (Aug 21 2020 at 09:54):

Alright, I thought `//`

and `|`

were used interchangably, so thanks for resolving that confusion.

I thought about the kernel definition, but didn't know if that was hom was already in lean. So the definition should look something like this?:

```
universes u v
section
variables (n: Type u) [decidable_eq n] [fintype n] (K: Type v) [field K]
def annihilator' (M: matrix n n K) : ideal (polynomial K) := (polynomial.aeval K (matrix n n K) M : polynomial K →+* matrix n n K).kernel
end
```

#### Kenny Lau (Aug 21 2020 at 10:03):

exactly

#### Kevin Buzzard (Aug 21 2020 at 13:28):

I'm afraid general theory has removed your chance to prove that it's an ideal :-)

#### Jonas Wildberger (Aug 21 2020 at 14:09):

Haha alright. So following Kenny's advice, lean still wants proof that `matrix n n K`

ist a K-Algebra. Is there already code for this? apply_instance doesn't work :(

#### Alex J. Best (Aug 21 2020 at 14:10):

In `ring_theory/algebra.lean`

there is docs#matrix_algebra

#### Jonas Wildberger (Aug 21 2020 at 16:21):

Sorry, but I still don't quite know how to incorporate docs#matrix_algebra to make it work. I think I misunderstand what `matrix_algebra n K`

outputs, as I get the error

type expected at

matrix_algebra n K

term has type

algebra K (matrix n n K)

though I thought `algebra K (matrix n n K)`

is what I wanted.

The rest of the code looks like this

```
universes u v
variables (n: Type u) [decidable_eq n] [fintype n] (K: Type v) [field K]
open polynomial
def annihilator' (M: matrix_algebra n K) : ideal (polynomial K) := (aeval (matrix_algebra n n K) matrix_algebra M : polynomial K →+* matrix_algebra n n K).ker
```

I also don't quite know how to make sure lean gets the correct structure of the matrix ring, as for the type ascryption I assume that I should not use `matrix_algebra`

because I only want the ring structure...

#### Alex J. Best (Aug 21 2020 at 16:55):

I'm also a bit confused how to do what you want I would like to write the line as:

```
def annihilator' (M : matrix n n K) : ideal (polynomial K) := (aeval M : (polynomial K →ₐ[K] (matrix n n K))).to_ring_hom.ker
```

#### Alex J. Best (Aug 21 2020 at 16:55):

But this fails as the matrix ring is not commutative and `aeval`

is only set up for commutative semirings.

#### Kenny Lau (Aug 21 2020 at 17:26):

oh, that's my bad then

#### Mario Carneiro (Aug 21 2020 at 18:38):

Just sorry a proof that `matrix_ring`

is commutative ;P

#### Adam Topaz (Aug 21 2020 at 18:39):

Non commutative rings don't exist anyway.

#### Adam Topaz (Aug 21 2020 at 18:53):

More seriously though, is there no proof that, given `algebra R A`

, (so `R`

is commutative), and a singleton `S = {x}`

, that `adjoin S`

is commutative?

Last updated: May 15 2021 at 23:13 UTC