finite free over PID

Stream: maths

[Johan Commelin]

@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$) 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]

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]

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

[Anne Baanen]

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

[Johan Commelin]

Ooh, probably yes

[Anne Baanen]

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]

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

[Kevin Buzzard]

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

[Johan Commelin]

yes, I think it's somewhat ugly

[Johan Commelin]

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