Zulip Chat Archive

Stream: maths

Topic: Constructive tensor product


view this post on Zulip Kenny Lau (Jul 25 2018 at 01:26):

https://github.com/kckennylau/Lean/blob/master/constructive_tensor_product.lean

view this post on Zulip Kenny Lau (Jul 25 2018 at 01:27):

I built a constructive tensor product and proved that it is a module. I have not proved its properties.

view this post on Zulip Kenny Lau (Jul 25 2018 at 01:27):

But inside there is also a constructive version of free abelian group

view this post on Zulip Kevin Buzzard (Jul 25 2018 at 08:55):

I needed free abelian group on a type and the finsupp approach demanded I had decidable equality on the type. Is this to be expected?

view this post on Zulip Kenny Lau (Jul 25 2018 at 08:55):

my version does not need decidable equality

view this post on Zulip Kenny Lau (Jul 25 2018 at 08:55):

but finsupp does need decidable equality

view this post on Zulip Kevin Buzzard (Jul 25 2018 at 08:56):

Oh great! I was a bit confused as to why I suddenly needed it.

view this post on Zulip Kenny Lau (Jul 25 2018 at 12:07):

https://github.com/kckennylau/Lean/blob/master/constructive_tensor_product.lean

view this post on Zulip Kenny Lau (Jul 25 2018 at 12:07):

I proved the property

view this post on Zulip Kenny Lau (Jul 25 2018 at 12:07):

@Kevin Buzzard

view this post on Zulip Kevin Buzzard (Jul 25 2018 at 13:28):

So now back to alg closure? ;-)

view this post on Zulip Kenny Lau (Jul 25 2018 at 18:25):

hmm

view this post on Zulip Kenny Lau (Jul 25 2018 at 18:26):

let's prove the separability lemma first


Last updated: May 10 2021 at 06:13 UTC