Zulip Chat Archive

Stream: maths

Topic: projective objects


view this post on Zulip Johan Commelin (Apr 20 2021 at 06:24):

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

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 06:27):

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

view this post on Zulip Johan Commelin (Apr 20 2021 at 06:29):

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

view this post on Zulip Damiano Testa (Apr 20 2021 at 06:31):

Would is_free be defined as the existence of a is_basis?

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 06:34):

That would be my instinct

view this post on Zulip Damiano Testa (Apr 20 2021 at 06:36):

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

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 06:36):

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

view this post on Zulip Damiano Testa (Apr 20 2021 at 06:36):

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

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 06:37):

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

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 06:37):

And then free modules are projective and flat

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 06:38):

Projective implies flat I guess

view this post on Zulip Damiano Testa (Apr 20 2021 at 06:39):

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

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 06:49):

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

view this post on Zulip Damiano Testa (Apr 20 2021 at 06:50):

Indeed!

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

view this post on Zulip Anne Baanen (Apr 20 2021 at 07:49):

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.

view this post on Zulip Johan Commelin (Apr 20 2021 at 07:49):

Thanks for the reminder!


Last updated: Jun 17 2021 at 16:20 UTC