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

1. the definition works so far and
2. 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.

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):

def annihilator (M : matrix n n K) : ideal (polynomial K) :=
{ carrier := annihilator' n K M,
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


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.

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