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 ) 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: May 09 2021 at 11:09 UTC