## Stream: maths

### Topic: transcendence basis

#### 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.

#### 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

#### 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)

#### 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?

#### Mario Carneiro (Jan 20 2020 at 08:46):

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

#### 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

#### 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

#### 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 $R$ to be a field, so the theory of transcendence bases gives me what I want immediately.

#### 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?

#### Kevin Buzzard (Jan 20 2020 at 18:46):

I have no idea what a matroid is :-(

#### Kevin Buzzard (Jan 20 2020 at 19:18):

You do seem to be right.

#### 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.

#### Patrick Massot (Jan 20 2020 at 19:28):

I never heard about them before using Lean.

#### 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