structure vs class

Stream: new members

[Jonas Wildberger]

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

[Kenny Lau]

eval map algebra_map is basically aeval right

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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]

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]

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

[Kenny Lau]

we call this a type ascription, i.e. announcing that [expr] has type [expr2] by writing ([expr] : [expr2])

[Kenny Lau]

the kernel is ring_hom.kernel

[Jonas Wildberger]

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]

exactly

[Kevin Buzzard]

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

[Jonas Wildberger]

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]

In ring_theory/algebra.lean there is docs#matrix_algebra

[Jonas Wildberger]

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]

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]

But this fails as the matrix ring is not commutative and aeval is only set up for commutative semirings.

[Kenny Lau]

oh, that's my bad then

[Mario Carneiro]

Just sorry a proof that matrix_ring is commutative ;P

[Adam Topaz]

Non commutative rings don't exist anyway.

[Adam Topaz]

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?

[Vasily Ilin]

How do I decide if my definition should be a class or a structure? What influences this decision? Here is the concrete example:

import ring_theory.tensor_product

open_locale tensor_product
open algebra.tensor_product

variables (K : Type*) [comm_ring K]
variables (A : Type*) [comm_ring A] [algebra K A]

structure hopf_algebra := -- should this be a class?
(comul : A →ₐ[K] A ⊗[K] A)
(counit : A →ₐ[K] K)
(coassoc : (tensor_product.assoc K A A A) ∘ (map comul (alg_hom.id K A)) ∘ comul = map (alg_hom.id K A) comul ∘ comul)
(counit_left : (tensor_product.lid K A) ∘ (map counit (alg_hom.id K A)) ∘ comul = (alg_hom.id K A))
(counit_right : (tensor_product.rid K A) ∘ (map (alg_hom.id K A) counit) ∘ comul = (alg_hom.id K A))
(coinv : A →ₐ[K] A)
(coinv_right : (lmul' K) ∘ (map (alg_hom.id K A) coinv) ∘ comul = (algebra.of_id K A) ∘ counit)
(coinv_left : (lmul' K) ∘ (map coinv (alg_hom.id K A)) ∘ comul = (algebra.of_id K A) ∘ counit)
.

[Eric Wieser]

A good question to ask is "do I care primarily about talking about two different hopf algebra structures on the same type, or about talking about the canonical hopf algebra on a type"

[Eric Wieser]

The answers are respectively structure and class

[Eric Wieser]

I would say that yours should be a class

[Vasily Ilin]

Thank you so much!