projective objects

Stream: maths

[Johan Commelin]

I've just kicked #7108 (projective objects) on the queue. Just a quick post here to point out that I think it would be a great project to "ground" this abstract stuff in actual examples (modules, vector spaces).

[Kevin Buzzard]

The correct thing to do with vector spaces is to prove they're all free first. Do we have an is_free predicate?

[Johan Commelin]

Not yet. I think it would be a very useful predicate. Because we have a lot of different ways of constructing free modules.

[Damiano Testa]

Would is_free be defined as the existence of a is_basis?

[Kevin Buzzard]

That would be my instinct

[Damiano Testa]

I am mostly testing whether my instinct is developing in a "lean-friendly/reasonable" way: thanks for confirming, Kevin!

[Kevin Buzzard]

And the basic API might be: every module over a field is free, every module over the zero ring is free, zero module is free, product of two free modules is free, arbitrary product of free modules is free, polynomial and multivariable polynomial rings are free over the base semiring

[Damiano Testa]

I see that you are freely using the axiom of choice...

[Kevin Buzzard]

Oh I guess every module over the zero ring is zero you don't need the zero ring result

[Kevin Buzzard]

And then free modules are projective and flat

[Kevin Buzzard]

Projective implies flat I guess

[Damiano Testa]

I remember you telling me an interesting story about the definition of local rings in mathlib. To the list above, I would also probably add (maybe as a longer term goal) that, over a "math local ring", projective is free.

https://stacks.math.columbia.edu/tag/058Z

[Kevin Buzzard]

Right but that's a bigger project. I certainly agree it needs doing! More generally projective iff locally free

[Damiano Testa]

Indeed!

I guess that formalising this, all the required finiteness assumptions would should up, when they are needed.

[Anne Baanen]

I'd like to make a quick warning that I'm refactoring is_basis to be bundled, so I'd like to coordinate a bit before defining is_free.

[Johan Commelin]

Thanks for the reminder!