LocalizedModule vs DivisibleCompletion

Stream: mathlib4

[Weiyi Wang]

When developing Hahn embedding theorem, I created DivisibleCompletion in #25338, which embeds an ordered group M into a ordered ℚ-module. I later realized this is equivalent to the existing LocalizedModule (nonZeroDivisors ℤ) M). The "only" thing missing is a linear order on LocalizedModule.

However when I tried adding that linear order, it became pretty cumbersome as the "denominator" of LocalizedModule is in nonZeroDivisors ℤ, and the sign doesn't play well with the ordering in multiplication. Should I continue working in this direction? Or is DivisibleCompletion good enough even though it is somewhat duplicating the theory?

(I also looked at another equivalent object ℚ ⊗[ℤ] M, which similarly lacks theory for linear order, and I haven't figured out the right definition for ordering on tensor product yet)

[Weiyi Wang]

(maybe I just got stuck for no reason and it isn't that hard to add the linear order)

[Weiyi Wang]

I suppose I could add a IsLocalization (Submonoid.pos ℤ) ℚ instance and now LocalizedModule (Submonoid.pos ℤ) M will truly be equivalent to my DivisibleCompletion

[Weiyi Wang]

Alright, so I was able to add linear order and prove properties I wanted to LocalizedModule (Submonoid.pos ℤ) M. The next question would be if I could generalize this to other rings besides ℤ... this sounds really painful. I hope I can just PR the ℤ version?

[Scott Carnahan]

I think divisible completion (or injective hull) is sufficiently important that you don’t need to generalize to other rings at this time.