Projective module over a local ring is free

Stream: Is there code for X?

[Kevin Buzzard]

We have things which seem to me to be at least as strong as this in Algebra.Module.FreeLocus (see for example docs#Module.freeLocus_eq_univ_iff ) but do we have the simple statement that a projective module over a local ring is free?

import Mathlib

example (R : Type*) [CommRing R] [IsLocalRing R] (M : Type*) [AddCommGroup M] [Module R M]
  (h : Module.Projective R M) : Module.Free R M := by sorry

Edit: aah that theorem in the library already only works for finitely presented modules :-/ But this theorem is true in general, right? Edit: yes, it's https://stacks.math.columbia.edu/tag/0593

[Christian Merten]

We have docs#Module.free_of_flat_of_isLocalRing, but only with the finiteness assumption.

[Kevin Buzzard]

Rather annoyingly, the module in question is finitely-generaed but assuming finite presentation is basically putting some Noetherian hypotheses on the situation which shouldn't be there because we're representing a functor (the Grassmannian) so really should be running over all rings

[Joël Riou]

If a projective module is finitely generated, it is automatically finite presentation (e.g. as a direct factor of a finitely presented module). There should be a reasonable way to do this without Noetherian assumptions.

[Junyan Xu]

Yes, there is Module.finitePresentation_of_projective. (The proof identifies the kernel with a range: LinearMap.ker_eq_range_of_comp_eq_id.)
Or you can directly use #20460 :)
The result for non-f.g. modules is due to Kaplansky and depends on the whole section stacks#058T. Not aware of people working on this ...

[Kevin Buzzard]

Oh nice! In which case we don't need the general result. Thanks a lot!

[Off-topic: Matsumura's proof of the result uses ordinal induction, and until recently this was the only place I'd ever seen ordinals used outside of set theory/infinitary combinatorics. But then Conrad told me he knew a proof which avoided it. However Mathlib's proof of N\"obeling's theorem (used by Scholze in his work on condensed mathematics) also uses ordinal induction and I don't know a proof which avoids ordinals]

[Kevin Buzzard]

@Ivan Farabella you can get away with what is already in mathlib.

[Jz Pan]

Kevin Buzzard said:

Matsumura's proof of the result uses ordinal induction, and until recently this was the only place I'd ever seen ordinals used outside of set theory/infinitary combinatorics.

I think this is also using transfinite induction? https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/CardinalEmb.html

[Kevin Buzzard]

But this is just a counting result rather than anything "useful" (I can't imagine this result being used for anything else)

[Antoine Chambert-Loir]

As a matter of fact, you can always replace ordinal induction by Zorn's lemma. Sometimes, it's just awkward to do so (especially if you already have a proof of the other type under the eyes).

[Antoine Chambert-Loir]

Also : it is often sufficient to use Hartogs's lemma that given any set, there is a well ordered set that doesn't inject in it, but one doesn't need the specific model of ordinals. (This is how I prove Kaplansky's theorem in my book, Mostly commutative algebra).

[Violeta Hernández]

Kevin Buzzard said:

Mathlib's proof of N\"obeling's theorem (used by Scholze in his work on condensed mathematics) also uses ordinal induction and I don't know a proof which avoids ordinals]

The proof doesn't really need ordinals; it needs well-founded recursion, which isn't quite the same thing. In fact I've previously attempted to replace one by the other, I think the proof would be a bit cleaner that way since it avoids moving back and forth between the original order and the associated ordinals.

[Violeta Hernández]

Unfortunately got stuck at the very end of the refactor. I think I needed to use well-founded recursion over WithTop I rather than just I.
#20030

[Violeta Hernández]

As for results that need ordinals, I guess there's Goodstein's theorem, though that's admittedly very artificial and very obviously trying to exploit a specific ordinal notation.

[Antoine Chambert-Loir]

Violeta Hernández said:

I think I needed to use well-founded recursion over WithTop I rather than just I.
#20030

My experience is that often one needs to pick up a well ordering which has a top element.