Zulip Chat Archive

Stream: maths

Topic: finite free over PID


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?

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.

Johan Commelin (Mar 11 2021 at 12:46):

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

Anne Baanen (Mar 11 2021 at 12:47):

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

Johan Commelin (Mar 11 2021 at 12:50):

Ooh, probably yes

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

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.

Kevin Buzzard (Mar 12 2021 at 07:03):

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

Johan Commelin (Mar 17 2021 at 09:22):

yes, I think it's somewhat ugly

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: Dec 20 2023 at 11:08 UTC