Modules over PID

Stream: new members

[Chengyan Hu]

I’m curious about whether the theorem ‘for module over PID, flat and torsion-free are the same thing’ is already in mathlib? If so, what’s the proof stratergy? I’m currently taking a course in homological algebra and it’s sounds like a well-known proof is wrong.

[Riccardo Brasca]

I don't know why you think the usual proof is wrong, but we more generally have it for Dedekind domains IsDedekindDomain.flat_iff_torsion_eq_bot

[Riccardo Brasca]

The strategy seems to be the one in the stack project.

[Chengyan Hu]

Thanks a lot! I do agree with this proof.

[Chengyan Hu]

IMG_1677.png
IMG_1678.png
The proof I thought to be wrong is this one:

[Chengyan Hu]

Seems to be wrong from the first step

[Andrew Yang]

The proof seems correct to me?