Zulip Chat Archive

Stream: new members

Topic: structure vs class


view this post on Zulip 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.

Thanks in advance

view this post on Zulip Kenny Lau (Aug 21 2020 at 09:23):

eval map algebra_map is basically aeval right

view this post on Zulip Kenny Lau (Aug 21 2020 at 09:23):

also this is not a set: a set uses | instead of //

view this post on Zulip 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"

view this post on Zulip 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' := _ }

view this post on Zulip 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

view this post on Zulip 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])

view this post on Zulip 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])

view this post on Zulip Kenny Lau (Aug 21 2020 at 09:26):

the kernel is ring_hom.kernel

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 21 2020 at 10:03):

exactly

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 13:28):

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

view this post on Zulip 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 :(

view this post on Zulip Alex J. Best (Aug 21 2020 at 14:10):

In ring_theory/algebra.lean there is docs#matrix_algebra

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Aug 21 2020 at 17:26):

oh, that's my bad then

view this post on Zulip Mario Carneiro (Aug 21 2020 at 18:38):

Just sorry a proof that matrix_ring is commutative ;P

view this post on Zulip Adam Topaz (Aug 21 2020 at 18:39):

Non commutative rings don't exist anyway.

view this post on Zulip 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