Special-casing definitions in mathlib: IsSharpMonoid

Stream: mathlib4

[Bhavik Mehta]

In #26110, @Yaël Dillies proposes to add IsSharpMonoid to mathlib, which says

/-- A monoid is sharp iff its only unit is `1`. -/
class IsSharpMonoid (M : Type*) [Monoid M] : Prop where
  eq_one_of_isUnit {a : M} : IsUnit a → a = 1

It is not hard to see that this is equivalent to Subsingleton Mˣ, but the PR description says

This concept already existed in the guise of Subsingleton Mˣ, but giving it a name makes it easier to refer to, uncovers the missing instance and turning it into its own class gives the opportunity for it to have a useful default constructor.

Do we want to have this definition in mathlib, for the reasons given above? Or should we continue to refer to this notion by the existing spelling Subsingleton Mˣ? My preference is for the latter, but I'd like to hear others' opinions.

[Edward van de Meent]

isn't this just something that can be an abbrev?

[Edward van de Meent]

i don't think that having this in mathlib is particularly harmful.

[Bhavik Mehta]

I agree it's probably not particularly harmful, but it is new precedent: we famously don't have VectorSpace, which not dissimilar from what's happening here.

[Yaël Dillies]

I think it is more similar to Representation actually :thinking: ... in the sense that it's a typeclass that can be written as the specialisation of some other typeclass to a type constructor

[Sophie Morel]

Representation is an abbrev, so your comparison would be in favor of making IsSharpMonoid an abbrev too.

[Yaël Dillies]

I am happy to make this an abbrev. Turns out the nice constructor isn't so nice... I do still believe we should give this proposition a name, because it's a name that exists in the literature, because it structures thought, and because it would become more searchable

[Bhavik Mehta]

However, all of these were arguments used in favour of VectorSpace. What I'm not yet seeing is how this case is different from that!

[Artie Khovanov]

What was the winning argument against abbrev Vector Space?

[Kevin Buzzard]

In Lean 3: it didn't work very well. In Lean 4: we haven't tried it yet.

[Jovan Gerbscheid]

@[inherit_doc] scoped[Affine] notation "AffineSpace" => AddTorsor

This thing exists with the same flavour. I think it is nice, but equally confusing, because now you can write the same thing in two ways.

[Edward van de Meent]

imo the main difference with VectorSpace is that VectorSpace is essentially restricting arguments compared to Module, while in this case there is no such thing.

[Edward van de Meent]

i.e. since Units and IsSharpMonoid both take a Monoid instance, there is no "loss of generality" by phrasing it differently

[Artie Khovanov]

Ideal is a special case of Submonoid right?

[Aaron Liu]

An ideal of R is an R-submodule of R
src#Ideal

/-- A (left) ideal in a semiring `R` is an additive submonoid `s` such that
`a * b ∈ s` whenever `b ∈ s`. If `R` is a ring, then `s` is an additive subgroup. -/
abbrev Ideal (R : Type u) [Semiring R] :=
  Submodule R R

[Julian Berman]

Artie Khovanov said:

What was the winning argument against abbrev Vector Space?

I think abbrev aside, the last time I recall VectorSpace being brought up the agreement was -- at least to my recollection for all who participated in the thread -- that it was not any longer a "no", and was just waiting on someone sending a PR using variable_alias for it -- so I sent https://github.com/leanprover-community/mathlib4/pull/19212 -- but got stalled because... I forget why, I think I couldn't figure out how to test variable? and then forgot about the PR.

[Yaël Dillies]

Yes, my suggestion is probably closest to Ideal

[Junyan Xu]

docs#FiniteDimensional is an abbrev of docs#Module.Finite. Since this works VectorSpace would probably also work?
Looks like we have exactly one decl docs#VectorSpace.card_fintype under the VectorSpace namespace, plus some other decls containing VectorSpace in the name.

[Jovan Gerbscheid]

The problem is that VectorSpace is not an abbrev for one class, but an abbrev for two classes simultaneously. That is why we would need class abbrev for it.

[Junyan Xu]

Are you suggesting something other than

import Mathlib.Algebra.Field.Defs
import Mathlib.Algebra.Module.Defs
abbrev VectorSpace (K V : Type*) [DivisionRing K] [AddCommGroup V] := Module K V

?

[Kenny Lau]

Junyan Xu said:

docs#FiniteDimensional is an abbrev of docs#Module.Finite. Since this works VectorSpace would probably also work?

but Module.Finite is a Prop

[Jovan Gerbscheid]

@Junyan Xu Yes that should work. My suggestion with the proposed class abbrev would allow you to write VectorSpace in place of the combination of AddCommGroup and Module.

[Junyan Xu]

I see! Oh now I remember there's also docs#Subspace.

[Andrew Yang]

Junyan Xu said:

I see! Oh now I remember there's also docs#Subspace.

Wait. Do we really want this?

[Bhavik Mehta]

It's still not clear to me that IsSharpMonoid actually helps us in mathlib: I think most people here would find it more understandable to see an assumption Subsingleton Mˣ rather than IsSharpMonoid M; in contrast with Module vs VectorSpace.

[Yaël Dillies]

For me, the main reason to have IsSharpMonoid is to standardise the spelling. There are many different ways to state it (although Subsingleton Mˣ seems to be the only one that's a Prop-valued class), and it feels appropriate to say "This is the spelling that people should use"

[Yaël Dillies]

More concretely, it also lets us have niceties like anonymous dot notation for

lemma IsSharpMonoid.of_isUnit (h : ∀ a : M, IsUnit a → a = 1) : IsSharpMonoid M

instead of

lemma Subsingleton.units_of_isUnit (h : ∀ a : M, IsUnit a → a = 1) : Subsingleton Mˣ

[Jireh Loreaux]

Yaël Dillies said:

There are many different ways to state it

What are all these ways? If there are multiple competing ways in Mathlib, all of which are commonly used, then I could see that as an argument. If not, then I think this is in the same class as VectorSpace.

[Kenny Lau]

@Jireh Loreaux

• Subsingleton Mˣ shows up in assumptions 59 times and in statements 2 times
• Unique Mˣ shows up in statements 8 times and in assumptions 0 times (as it should)

[Jireh Loreaux]

okay, but these are actually slightly different, since Unique carries data, hence the discrepancy between statements and assumptions. Adding IsSharpMonoid would only replace the first bullet point, not the second.

[Kenny Lau]

@Jireh Loreaux no, the Unique stuff should all just be replaced with Subsingleton imo, we know 1 is in there anyway

[Jireh Loreaux]

Sure, fine, but then your post doesn't answer my question?

[Yaël Dillies]

Jireh Loreaux said:

What are all these ways?

Subsingleton M\^x, \for x : M, IsUnit x \r x = 1.

[Ruben Van de Velde]

Do you have examples of the latter on hand?

[Yaël Dillies]

I do not, no

[Yaël Dillies]

I personally think the IsSharpMonoid abbrev fulfills three roles:

1. It shows that the combination of Subsingleton and Units is mathematically relevant, and links to the literature name
2. It enables dot notation on it, eg my lemma IsSharpMonoid.of_isUnit (h : ∀ a : M, IsUnit a → a = 1) : IsSharpMonoid M spelled without IsSharpMonoid would be lemma Subsingleton.units_of_isUnit (h : ∀ a : M, IsUnit a → a = 1) : Subsingleton Mˣ
3. It makes it clear what instances we should be writing, eg right now we are missing instances like [∀ i, IsSharpMonoid (M i)] → IsSharpMonoid (∀ i, M i), I assume because [∀ i, Subsingleton (M i)ˣ] → Subsingleton (∀ i, M i)ˣ is a bit weird to look at

[Jovan Gerbscheid]

I don't understand point 3. What is wrong with [∀ i, Subsingleton (M i)ˣ] → Subsingleton (∀ i, M i)ˣ?

[Bhavik Mehta]

I also don't understand point 1, the literature name is already quite niche, and most people who know what "sharp monoid" means will understand "subsingleton units", but many people will know "subsingleton units" without having heard of "sharp monoid". We already have a canonical spelling for this in mathlib!

[Bhavik Mehta]

Ruben Van de Velde said:

Do you have examples of the latter on hand?

Loogle tells me there's only one result of this shape: https://loogle.lean-lang.org/?q=%E2%88%80+x%2C+IsUnit+x+%E2%86%92%C2%A0x+%3D+1 and it can't be written as Subsingleton M\^x anyway

[Yaël Dillies]

I'm clearly outnumbered here, so #26110 is updated to not include IsSharpMonoid anymore

[Matthew Ballard]

I assume Units is in the keys for Subsingleton M\^x?

[Yaël Dillies]

I have no idea. How do I check?

[Jovan Gerbscheid]

import Mathlib

-- Subsingleton (Units ℤ _)
#discr_tree_key Subsingleton Intˣ

[Junyan Xu]

Where does the terminology "sharp monoid" come from? This paper calls it "reduced" in §2.2.

[Yaël Dillies]

It comes from the corresponding property for convex cones, I believe. In mathlib it's called docs#ConvexCone.Salient