## Stream: maths

### Topic: projective objects

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

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

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

#### Damiano Testa (Apr 20 2021 at 06:31):

Would is_free be defined as the existence of a is_basis?

#### Kevin Buzzard (Apr 20 2021 at 06:34):

That would be my instinct

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

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

#### Damiano Testa (Apr 20 2021 at 06:36):

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

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

#### Kevin Buzzard (Apr 20 2021 at 06:37):

And then free modules are projective and flat

#### Kevin Buzzard (Apr 20 2021 at 06:38):

Projective implies flat I guess

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

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

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

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

#### Johan Commelin (Apr 20 2021 at 07:49):

Thanks for the reminder!

Last updated: Jun 17 2021 at 16:20 UTC