Rename `Rational-Extension-Ring` to `ℚ-Extension-Ring`

[fredrik-bakke]

This is consistent with how we treat real and complex vector spaces, and as discussed before, does not conflict with the underlying rational extension ring of ℚ, which would be called rational-extension-ring-ℚ.

@malarbol

[malarbol]

Sure, I think it could be good to discuss it even further. IIRC at when we merged Rational-Extension-Ring we discussed how it was related to rational vector spaces but we didn't have any Vector-Space infrastructure to build on. Maybe it's time to refactor this construction using ℚ-vector spaces, ℚ-algebras, etc.?

[fredrik-bakke]

The names ℚ-Vector-Space and ℚ-Algebra seem reasonable, no?

[malarbol]

The names ℚ-Vector-Space and ℚ-Algebra seem reasonable, no?

They surely do. so (rational modules)(https://unimath.github.io/agda-unimath/linear-algebra.rational-modules.html) would be ℚ-Vector-Space and Rational-Extension-Ring, ℚ-Algebra. With the definition that "a ℚ-Vector-Space is an Abelian group whose ring of endomorphisms is a ℚ-Algebra.

I'll have to get familiar with all the new stuff about vector spaces to get through this. I don't think we have anything on algebras over a local ring yet so ℚ-Algebra might be a bit premature.

All in all, I agree this calls for better names.