Trivial group / monoid / monoid with zero

Stream: Is there code for X?

[Jiang Jiedong]

Is there a definition or notation for the trivial group / monoid / monoid with zero, i.e. a monoid/group of a single element 1, and a monoid with zero of two element {0,1}?

[Yaël Dillies]

For the first question, one answer is docs#Unit

[Yaël Dillies]

For the second one, you can use WithZero Unit

[Jiang Jiedong]

I find that first two works and the third fails. I think I should write a LinearOrderedCommMonoid instance on my own.

import Mathlib.RingTheory.Valuation.Basic

#synth LinearOrder Unit
#synth CommMonoid Unit
#synth LinearOrderedCommMonoid Unit

[Kevin Buzzard]

Do import Mathlib just to check, but if it's not there then feel free to add it!

[Riccardo Brasca]

Note that you may prefer Subsingleton G if you want to speak about a trivial group. Otherwise your result will apply only to that literal group. What is you goal?

[Kevin Buzzard]

Yes, Unit is one very specific group, there are infinitely many other isomorphic but not equal groups with one element, and any theorem proved about Unit will not apply to them.

[Jiang Jiedong]

My goal is to first define a trivial valuation using this Unit, then define a predicate ‘IsTrivial’ of a valuation if it is equivalent to this special valuation. Do you think this is a good way to do it?

[Riccardo Brasca]

Maybe I am missing something, but isn't a valuation trivial iff v x = 0 for all x?

[Riccardo Brasca]

I mean, you can define isTrivial directly

[Kevin Buzzard]

Oh this sounds like an OK usage because the equivalence will take care of the issue that Riccardo has raised.

Another way of doing it would be to define a valuation to be trivial if the associated preorder (defined by x<=y iff v(x)<=v(y) is the preorder associated to the trivial valuation.

[Kevin Buzzard]

Riccardo I think the trivial valuation has v(0)=0 and v(x)=1 for all nonzero x

[Jiang Jiedong]

(deleted)

[Riccardo Brasca]

Oh, yes, 1, not 0.

[Riccardo Brasca]

Anyway as Kevin said you approach would work in this case

[Kevin Buzzard]

In my opinion, if you are only interested in valuations up to equivalence (e.g. if you are thinking about adic spaces) then a much better model for this type would be preorders on the ring satisfying the relevant list of axioms. This way you don't have to work with equivalence classes at all.

[Jiang Jiedong]

Kevin Buzzard said:

In my opinion, if you are only interested in valuations up to equivalence (e.g. if you are thinking about adic spaces) then a much better model for this type would be preorders on the ring satisfying the relevant list of axioms. This way you don't have to work with equivalence classes at all.

Oh that's what I didn't think of before. Thank you! Should I create a new post discussing this designing problem? Which stream should this post belong to?

[Kevin Buzzard]

Yes please do -- in #maths maybe. My impression is that people working on things like DVRs really do want a concrete valuation but that people working in the adic theory don't need it.

[Kevin Buzzard]

The preorder I'm talking about is mentioned at the bottom of p25 of these notes https://arxiv.org/pdf/1910.05934.pdf . This is the trick we used in the perfectoid project to prove (the type-theoretic analogue of) that equivalence classes of valuations were actually a set (because of course the collection of all totally ordered groups with 0 is not a set, so there are set-theoretic issues in the definition of adic space which you find in the books, which are often ignored i.e. literally not even mentioned -- see for example the claim in Def 4.1 of that paper that something is a set without any mention of this issue.)