## 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$) 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