Zulip Chat Archive

Stream: maths

Topic: transcendence basis


view this post on Zulip Kevin Buzzard (Jan 20 2020 at 08:22):

Do we have transcendence bases in Lean? I need the transcendence basis analogue of the linear algebra assertion that every spanning set contains a basis.

view this post on Zulip Mario Carneiro (Jan 20 2020 at 08:42):

I don't think so. I guess the nicest way to assert this is that the evaluation map from R[X1, ..., Xn] using the basis is injective

view this post on Zulip Mario Carneiro (Jan 20 2020 at 08:45):

That is, injective (eval₂ coe b) says that b : I -> R is an algebraically independent family (where coe : Q -> R is the inclusion)

view this post on Zulip Kevin Buzzard (Jan 20 2020 at 08:45):

I was trying to work through how to set this up. If I have a small field k and a big field K, then it seems to me to be crucial that I use subsets of K, so I can use mv_polynomial s k with s the subset, coerced to a subtype. I'm only interested in the finite situation right now, but here I don't think I can use a finset -- or do finsets also coerce to types?

view this post on Zulip Mario Carneiro (Jan 20 2020 at 08:46):

You don't actually need anything here to be finite, that was just illustration

view this post on Zulip Mario Carneiro (Jan 20 2020 at 08:48):

I'm not sure that it is crucial to use subsets, but I would have to know more about your application

view this post on Zulip Mario Carneiro (Jan 20 2020 at 08:48):

Indeed, my experience with basis itself suggests otherwise, that you should use families instead (indexed in some arbitrary type) or you will regret it later and have to refactor

view this post on Zulip Kevin Buzzard (Jan 20 2020 at 09:34):

My application is the Nullstellensatz because in the situation where I need this I realise that I can take RR to be a field, so the theory of transcendence bases gives me what I want immediately.

view this post on Zulip Patrick Massot (Jan 20 2020 at 11:31):

I think both Bryan and Antoine started on matroids at some point. They are meant to be a common abstraction of bases in linear algebra and your situation, right?

view this post on Zulip Kevin Buzzard (Jan 20 2020 at 18:46):

I have no idea what a matroid is :-(

view this post on Zulip Kevin Buzzard (Jan 20 2020 at 19:18):

You do seem to be right.

view this post on Zulip Enrico Borba (Jan 20 2020 at 19:19):

I have always been curious as to how common matroids are. I first encountered them in an algorithms class but never again since.

view this post on Zulip Patrick Massot (Jan 20 2020 at 19:28):

I never heard about them before using Lean.

view this post on Zulip Bryan Gin-ge Chen (Jan 20 2020 at 19:44):

The latest version of my matroids code is in the "fintype2" branch here. It's evolved a fair bit since my original thread, but still needs a lot more work. I'll post a brief comment in that thread about the current status.


Last updated: May 18 2021 at 07:19 UTC