Zulip Chat Archive

Stream: maths

Topic: finite free over PID


view this post on Zulip Johan Commelin (Mar 11 2021 at 05:00):

@Anne Baanen your PR about submodules of finite free modules over a PID came just at the right time. We need that kind of stuff (over Z\Z) for the liquid project. How hard do you think it is to lean the fact that over a PID exists_finite_basis is equivalent to fg + torsion_free?

view this post on Zulip Anne Baanen (Mar 11 2021 at 12:18):

Hmm, it wouldn't surprise me if it isn't too hard actually, depending on how much we already have about f.g. for modules (rather than vector spaces). The direction ∃ b, is_basis b → fg ∧ torsion_free should be no problem, the other way might be a bit trickier but you can probably go a long way with induction on the generating set? I'll have to see the state of the library to be sure.

view this post on Zulip Johan Commelin (Mar 11 2021 at 12:46):

@Anne Baanen Note that there isn't a definition of torsion_free yet, afaik

view this post on Zulip Anne Baanen (Mar 11 2021 at 12:47):

Isn't docs#no_zero_smul_divisors equivalent to torsion-free over a domain?

view this post on Zulip Johan Commelin (Mar 11 2021 at 12:50):

Ooh, probably yes

view this post on Zulip Anne Baanen (Mar 11 2021 at 12:52):

Still, it would be worth it to have the "real" torsion-free definition as well, and prove the equivalence (presumably as a set of typeclass instances?)

view this post on Zulip Johan Commelin (Mar 11 2021 at 12:53):

we probably can't have instances in every direction, but yes we should certainly have the definition.

view this post on Zulip Kevin Buzzard (Mar 12 2021 at 07:03):

Isn't the proof of this quite messy involving explicit matrix calculations and grotty normal forms?

view this post on Zulip Johan Commelin (Mar 17 2021 at 09:22):

yes, I think it's somewhat ugly

view this post on Zulip Johan Commelin (Mar 17 2021 at 09:23):

For our application in LTE we might just want to construct a basis of a quotient directly, although that will require doing the grotty normal forms manually in that specific case


Last updated: May 09 2021 at 11:09 UTC