Should linear ordered comm monoids with zero be torsion-free

Stream: mathlib4

[Yaël Dillies]

We have two lemmas proving that, if n : ℕ is non-zero, then a : M is one iff a ^ n is one:

• docs#IsMulTorsionFree.pow_eq_one_iff_left, assuming that M is torsion-free
• docs#pow_eq_one_iff, assuming that M is a linearly ordered monoid

[Yaël Dillies]

The latter looks like a code smell to me, since n ≠ 0 → (a ^ n = 1 ↔ a = 1) is a purely algebraic statement, yet it is proved using some order assumptions. This got me thinking: Is there any non-torsion-free linearly ordered monoid we care about? If not, we could fully replace pow_eq_one_iff with IsMulTorsionFree.pow_eq_one_iff_left.

[Yaël Dillies]

The answer is "It's hard, currently", because pow_eq_one_iff is used in the context of valuations on the target Γ of a valuation, which is a linearly ordered comm monoid with zero. This is a problem, because docs#LinearOrderedCommMonoidWithZero currently only implies monotonicity of multiplication, not strict monotonicity.

[Yaël Dillies]

My question therefore is: Should it be that LinearOrderedCommMonoidWithZero M₀ imply PosMulStrictMono M₀ (which would in turn imply IsMulTorsionFree M₀)?

[Yaël Dillies]

cc @Johan Commelin

[Yaël Dillies]

Here's my current progress unifying the two lemmas at the top of the thread: #30799

[Johan Commelin]

Thanks for the ping. I can't immediately think of a counter example. But let me ping some experts:
@Filippo A. E. Nuccio @María Inés de Frutos Fernández @Antoine Chambert-Loir @Yakov Pechersky @Adam Topaz

[Damiano Testa]

There is a counterexample to something that may be related in file#Counterexamples.CanonicallyOrderedCommSemiringTwoMul, but I am not sure if it is the (counter)example that you are looking for.

[Filippo A. E. Nuccio]

I'm on mobile now, but aren't you mixing up multiplicative and additive notation, @Yaël Dillies ? So, don't you want the conclusion that when n is non-zero, we have a*n=0 iff a=0?

[Yaël Dillies]

I mean torsion-free in the sense of docs#IsMulTorsionFree, ie n ≠ 0 → Injective (· ^ n)

[Filippo A. E. Nuccio]

Ok, but then in your code snippet you want to replace a^n = 0 by a^n=1, right? I'm asking to understand if you care about monoids with zero or simply honest monoids.

[Yaël Dillies]

Yes, sorry, that was a running typo

[Damiano Testa]

In the context of groups, a linear ordered forces the group to be torsion free.

[Damiano Testa]

I'm on mobile, but what happens with WithTop Unit?

[Yaël Dillies]

Indeed, LinearOrderedCommGroupWithZero G₀ already implies PosMulStrictMono G₀ (mathlib knows this). My question really is about non-group monoids. ZMod 2 (= WithTop Unit) respects PosMulStrictMono, so that's not interesting.

[Filippo A. E. Nuccio]

And ZMod 2 x ZMod 2 (as product of WithTop Units?) I'm not sure to immediately come up with an interesting valuation valued there, but it seems plausible.

[Yaël Dillies]

This is not linearly ordered

[Yaël Dillies]

You would need to come up with a non-cancellative monoid with zero, ie there would need to be some a ≠ b and c ≠ 0 such that a * c = b * c.

[Damiano Testa]

Like Z + ZMod 2, where (n, 0) < (n, 1): does it work?

[Damiano Testa]

Oh, this is a group!

[Filippo A. E. Nuccio]

Well, it depends on the structure on ZMod 2

[Filippo A. E. Nuccio]

I mean, if you see it as WithZero Unit, then 0 absorbs.

[Kenny Lau]

@Yaël Dillies consider the truncated monoid Fin 67 where a + b := min(a+b, 66) and a * b := min(ab,66), then 3^37 = 4^37

[Yaël Dillies]

Yes, I know this exists. My question is "Do you care about them?"

[Kenny Lau]

i guess other people in this discussion didn't know it exists

[Yaël Dillies]

Sorry, I should have given it as an example, but I didn't want to influence what people would come up with

[Antoine Chambert-Loir]

Well, everybody who worked with a 8-digit calculator knows that truncated integers exist.

[Antoine Chambert-Loir]

For me, there are two distinct questions:

• What kind of objects do LinearOrderedblahblahwe wish to model?
• Given the name of the structure, what is expected that they would satisfy.

[Damiano Testa]

This is only tangentially related, but when proving that monoid algebra (don't) have zero divisors, there were a lot of arguments involving an ordering on the grading monoid that were replaced by UniqueSums and it worked very well. Maybe something analogous should happen here, though I don't know what the replacement is!

[Antoine Chambert-Loir]

Thinking from ordered groups, there's a basic theorem that they are torsion free, which drives the whole mathematical field. (For example, it follows from the fact that the braid group is orderable that it is torsion free.) So I guess our ordered blobs should satisfy this as well.

[Antoine Chambert-Loir]

From what I understand, only the relation with $\leq$ has been imposed but not $\lt$, and that may be a mistake. On the other hand, changing the definition now might break a lot of things and we may also wish to have a weaker structure at our disposal.

[Kenny Lau]

I feel like this is heading towards the direction of "we should only allow monoids whose map to its groupification is injective" and I don't think that's a good direction

[Antoine Chambert-Loir]

Not at all, there are very important monoids/semirings which are not like that.

[Antoine Chambert-Loir]

The question here is only about the notion of an ordering relation on a monoid, that is, the nature of the expected interaction between the ordering relation and the multiplication. Is it that multiplication respects $<$ or that it respects $\leq$? As your simple example shows, these are two different notions.

[Yaël Dillies]

Do you have (naturally occurring) examples of valuations that are valued in non-cancellative monoids with zero? This, to me, seems like the central question

[Kenny Lau]

I suppose by that you mean organic examples

[Aaron Liu]

what's a valuation

[Johan Commelin]

docs#Valuation

[Aaron Liu]

I can value any local domain which is not a field in a three element linear ordered comm monoid with zero that's not cancellative

[Aaron Liu]

is that "natural"

[Yaël Dillies]

I am looking for important mathematical applications, not theoretical considerations

[Antoine Chambert-Loir]

The fact that the whole edifice of mathematics holds up is a combination of important examples and such theoretical considerations. (Analogous argument: you can likely delete the empty set from the theory of sets by pretending but this will make the theory much more difficult to work out.)

[Kenny Lau]

Yaël Dillies said:

Do you have (naturally occurring) examples of valuations that are valued in non-cancellative monoids with zero?

At least for ValuativeRel the answer is negative, because it is set up so that the support is always a prime ideal, so you get a valuation on R/supp(R) which is an integral domain

[Kenny Lau]

(but it seems like Valuation does not have this restriction)

[Antoine Chambert-Loir]

For docs#Valuation, keep in mind that mathematicians always consider the case where the monoid with zero comes from a linearly ordered group with zero added. Here, mathlib has to judge between the tension of adding an extra level of generality (by authorizing all ordered comm monoids with zero, whatever that means) with the need of providing additional hypotheses to get actual theorems, or sticking within the classical story.

[Yaël Dillies]

Thanks Antoine! I believe what you just said is strong evidence we could restrict the Valuation API (and therefore LinearOrderedCommMonoidWithZero, whose sole purpose is to be used in the Valuation API) to talk about cancellative monoids with zero.

[Yaël Dillies]

docs#LinearOrderedAddMonoidWithTop would then need changing too, as it is the generality of the codomain of a general additive valuation

[Yakov Pechersky]

If I understand correctly the setting, by our LinearOrderedCommGroupWithZero (and general "math" structure), the Hahn embedding theorem says any such group can be decomposed into a lexicographic product of subgroups of the Reals (considered additively). So one gets the LE to LT relationship naturally that way, due to inheriting it from the Reals (or Int when discrete).

[Antoine Chambert-Loir]

… or, simpler, by cancellation if the monoid with zero is actually a group with zero.

[Andrew Yang]

Maybe sidetracking but I am a bit sad that all linear ordered cancellative monoid stuff are only developed assuming it is a partial order. This forced me to duplicate API for the valuation preorder on valued fields.

[Yaël Dillies]

I think your point is worth another discussion, yes