transcendence basis

Stream: maths

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Patrick Massot]

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?

[Kevin Buzzard]

I have no idea what a matroid is :-(

[Kevin Buzzard]

You do seem to be right.

[Enrico Borba]

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

[Patrick Massot]

I never heard about them before using Lean.

[Bryan Gin-ge Chen]

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.