Absolute minimum vs. interesting minimum mixins.

Stream: new members

[Peter Hansen]

I was looking at the TODO: assume weaker typeclasses for docs#IsOrderedMonoid.

Here is the current definition:

class IsOrderedMonoid (α : Type*) [CommMonoid α] [PartialOrder α] where
  protected mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c, c * a ≤ c * b
  protected mul_le_mul_right : ∀ a b : α, a ≤ b → ∀ c, a * c ≤ b * c := fun a b h c ↦ by
    rw [mul_comm _ c, mul_comm _ c]; exact mul_le_mul_left a b h c

A barebone version of the class could be

class IsOrderedCommMagma (α : Type*) [CommMagma α] [LE α] where
  protected mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c, c * a ≤ c * b
  protected mul_le_mul_right : ∀ a b : α, a ≤ b → ∀ c, a * c ≤ b * c := fun a b h c ↦ by
    rw [mul_comm _ c, mul_comm _ c]; exact mul_le_mul_left a b h c

Is this the right approach?

We can state the monotonicity properties with just [LE α], but we do not have much to say about it unless we atleast have a [Preorder α]. What's the general philosophy here? Do we choose the absolute minimum typeclass required to state the props (LE), or the "interesting minimum" required to build a useful theory (Preorder)?

[Aaron Liu]

I was thinking weaken CommMonoid to Monoid or Semigroup or Mul

[Aaron Liu]

That way it can be applied to ordinals which do not have commutative multiplication

[Peter Hansen]

Aaron Liu said:

I was thinking weaken CommMonoid to Monoid or Semigroup or Mul

I suppose there is no intrinsic reason for the operation to be commutative ... or associative really ... so maybe just a Mul?

[Aaron Liu]

Also changing PartialOrder to Preorder does have a use (I have a use in mind)

[Aaron Liu]

but not sure about Preorder to LE

[Peter Hansen]

Aaron Liu said:

but not sure about Preorder to LE

No, I doubt it would have much use without at least a preorder. Hence my question in the post. There seem to be little gained from using LE, but is there any expense?

[Kevin Buzzard]

It's not clear to me that you shoud change the name of the class. For example we have things like docs#RingHom which is more general than homomorphisms between rings but is called RingHom to maximise readability.

[Peter Hansen]

Kevin Buzzard said:

It's not clear to me that you shoud change the name of the class. For example we have things like docs#RingHom which is more general than homomorphisms between rings but is called RingHom to maximise readability.

Fair enough - let's keep it an ordered monoid then. If you have any thoughts regarding the type-classes it should assume, I would very much like to hear it :)

[Kevin Buzzard]

I don't really know how the basic stuff like this should be wired up. Just git blame who wrote the TODO and ping them here :-)

[Yaël Dillies]

cc @Artie Khovanov, I'm sure you would enjoy the discussion :wink:

[Peter Hansen]

cc @Yuyang Zhao

[Artie Khovanov]

Cheers Yaël :sob:
Yes, I have my own proposals in this space
Around IsOrderedRing

[Eric Paul]

Just wanted to say that I'd be excited to see a version that includes noncommutative ordered semigroups as I need them in a project of mine!

Here's an example of the definitions I care about in case that's helpful Defs.lean

[Artie Khovanov]

@Eric Paul are you aware of the unbundled order mixins in Algebra.Order.Monoid.Unbundled.Defs?

[Eric Paul]

I'm roughly aware of them but wasn't certain the best way to interact with them. I went ahead and tried to copy the way mathlib currently sets up docs#IsOrderedMonoid, that is defining an IsOrdered___ and then giving it the instances of those unbundled things.

[Yuyang Zhao]

I noticed that some people might want weaker assumptions. But to avoid affecting the benchmark results, I didn't weaken it in that PR. I'm not sure whether [LE α] or [Preorder α] is better. Regarding the name issue, it has already been asked once at https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Ways.20to.20speed.20up.20Mathlib/near/494192310.