Zulip Chat Archive

Stream: condensed mathematics

Topic: free module


Johan Commelin (Jun 21 2021 at 13:27):

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

Johan Commelin (Jun 21 2021 at 13:28):

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

Johan Commelin (Jun 21 2021 at 13:28):

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

Riccardo Brasca (Jun 21 2021 at 13:45):

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 (Jun 21 2021 at 13:47):

Why don't you ask Lean? :grinning:

Riccardo Brasca (Jun 21 2021 at 14:03):

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

Johan Commelin (Jun 21 2021 at 14:06):

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 (Jun 22 2021 at 10:17):

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

Johan Commelin (Jun 22 2021 at 10:17):

I've already introduced 3 sorrys :see_no_evil:

Johan Commelin (Jun 22 2021 at 12:16):

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 (Jun 22 2021 at 12:17):

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

Scott Morrison (Jun 22 2021 at 12:24):

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 (Jun 22 2021 at 12:25):

(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 (Jun 22 2021 at 12:25):

Yeah, that looks like exactly what I need

Johan Commelin (Jun 22 2021 at 12:26):

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

Scott Morrison (Jun 22 2021 at 12:26):

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.


Last updated: Dec 20 2023 at 11:08 UTC