free module

Stream: condensed mathematics

[Johan Commelin]

docs#module.free is in mathlib, so we can update the definition of polyhedral lattice in LTE.

[Johan Commelin]

I can do that tomorrow, if nobody does it today (-;

[Johan Commelin]

(I've finally battled through most of my todo list of tasks that I had neglected in the last two months.)

[Riccardo Brasca]

I think we need to know that finite R M free R M implies the existence of a finite basis (is this always true? even for noncommutative rings?)

[Johan Commelin]

Why don't you ask Lean? :grinning:

[Riccardo Brasca]

There is docs#finite_dimensional.fin_basis but it is only for fields (and uses finite_dimensional, that means is_noetherian)

[Johan Commelin]

I guess we can do this in steps. First refactor LTE to use module.free, and generalise some stuff to the noncomm. case in a later step.

[Johan Commelin]

I've pushed a start to the poly-fin-free branch

[Johan Commelin]

I've already introduced 3 sorrys :see_no_evil:

[Johan Commelin]

I pushed. There is 1 sorry left:

instance [module.finite R M] [module.free R M] : fintype (module.free.choose_basis_index R M) :=
sorry

[Johan Commelin]

@Scott Morrison Does this easily follow from some of the stuff that you've recently been doing?

[Scott Morrison]

Does

/--
Over any nontrivial ring, the existence of a finite spanning set implies that any basis is finite.
-/
def basis_fintype_of_finite_spans (w : set M) [fintype w] (s : span R w = ⊤)
  {ι : Type w} (b : basis ι R M) : fintype ι := ...

(from branch#ibn4) give what you need?

[Scott Morrison]

(Unfortunately I'm barely here for the next two days, and then entirely offline for two weeks, so this branch is not coming to mathlib in a hurry.)

[Johan Commelin]

Yeah, that looks like exactly what I need

[Johan Commelin]

Thanks for the link. Maybe I'll just copy-pasta some of that, to get LTE working again

[Scott Morrison]

I've already down to the "find correct homes for lemmas" stage, so you may need to hunt around for a few prerequisites about cardinals, I don't quite remember what that proof uses.