LinearOrderedSemiring

Stream: maths

[Riccardo Brasca]

During the Leiden conference, @Flo (Florent Schaffhauser) and myself came up with the question whether docs#sq_nonneg can be generalized to LinearOrderedSemiring. Thanks to @Bhavik Mehta and @Damiano Testa we now know that the answer is "no" (we have a sorry free Lean proof). This means in particular that multiplication by a negative element does not reverse inequalities in a LinearOrderedSemiring.

I don't have a good example of a LinearOrderedSemiring that is not a subset of a LinearOrderedRing, but my intuition suggest that ≤ a ^ 2 should always be true.

[Riccardo Brasca]

/poll Do you think we should change the definition of LinearOrderedSemiring to imply this?
Yes
No
We shouldn't really care

[Pedro Sánchez Terraf]

I went to the definition (in order to make an informed suggestion---I was inclined to say "No" because of my preconception of what LinearOrderedSemiring should be) and I was surprised by the extra structure (for example, the “unit”). Am I not reading it correctly?

[Yaël Dillies]

What "unit"? 0?

[Pedro Sánchez Terraf]

Yaël Dillies said:

What "unit"? 0?

I see a one (1) there.

[Riccardo Brasca]

Currently, a LinearOrderedSemiring is a nontrivial Semiring with a total order such that:

• a ≤ b → c + a ≤ c + b
• a + b ≤ a + c → b ≤ c
• 0 ≤ 1
• a < b → 0 < c → c * a < c * b
• a < b → 0 < c → a * c < b * c

[Riccardo Brasca]

Semiring means associative semiring with 1.

[Yaël Dillies]

Yeah, I don't think anybody cares (yet) about ordered non-unital semirings.

[Pedro Sánchez Terraf]

Yaël Dillies said:

Yeah, I don't think anybody cares (yet) about ordered non-unital semirings.

Haha, fair point. Hope no one does in the future!

[Kevin Buzzard]

@Jireh Loreaux do any examples spring to mind? I know you've been ordering exotic objects -- but if everything for you is a $\mathbb{C}$-algebra then I suspect you don't care about semirings.

[Scott Morrison]

@James Borger, do you care about semirings with linear orders? If so, do you think that 0 \le a^2 is always true?

[Eric Rodriguez]

What is this example that doesn't work? Is it natural?

[Riccardo Brasca]

Here it is (credits to @Bhavik Mehta ).

import Mathlib.Tactic

@[ext] structure MyType : Type := (fst snd : ℕ)

namespace MyType

inductive le : MyType → MyType → Prop
| left {a c y} : a ≤ c → le ⟨a, y⟩ ⟨c, y⟩
| right {a b c d} : d < b → le ⟨a, b⟩ ⟨c, d⟩

instance : Add MyType where add | a, b => ⟨a.1 + b.1, a.2 + b.2⟩
instance : Zero MyType where zero := ⟨0, 0⟩
instance : Mul MyType where mul | a, b => ⟨a.1 * b.1, a.2 * b.1 + a.1 * b.2⟩
instance : One MyType where one := ⟨1, 0⟩
instance : LE MyType where le := le

[Flo (Florent Schaffhauser)]

Kevin Buzzard said:

do any examples spring to mind?

Of ordered non-unital semirings? Well, 2ℕ is an example, but as Riccardo pointed out, it is a subset of an ordered ring.

And of course it is not an example of a linearly ordered semiring in which not all squares are non-negative... (I guess an example of that is what you wanted, Kevin).

[Flo (Florent Schaffhauser)]

To be honest, I am more puzzled by the fact that Semiring means semiring with unit (but I am not advocating for a change here!).

[Riccardo Brasca]

When we introduced non unital stuff we decided to keep the name Ring for rings with unity since it is much more common.

[Bhavik Mehta]

Just a comment on my example - the way to view it is a + b eps, with a nonnegative and b nonpositive, and the ordering is lex in this sense, and eps ^ 2 = 0. The original idea was to have b arbitrary, but this has too many positive elements for mul_lt_mul_of_pos_left to be true (everything except this works); but insisting that b cannot be positive means the only positive elements are the naturals, recovering the axiom. But of course, the hypothetical mul_lt_mul_of_neg_left fails, and this is what creates a negative square. I'll put this example in Counterexamples!

[Damiano Testa]

Without contributing further examples, I am inclined to say that some ring-like structure where multiplication by positive elements is monotone and by negative ones is antitone should exist. Depending on how much effort it is to refactor the current LinearOrderedSemiring, there is also the possibility of defining the newer, more restrictive typeclass and then simply doing a rename.

[Jireh Loreaux]

Pedro Sánchez Terraf said:

Yaël Dillies said:

Yeah, I don't think anybody cares (yet) about ordered non-unital semirings.

Haha, fair point. Hope no one does in the future!

Why wouldn't you care about C₀(X, ℝ≥0) for X a locally compact Hausdorff space?

[Pedro Sánchez Terraf]

Jireh Loreaux said:

Pedro Sánchez Terraf said:

Yaël Dillies said:

Yeah, I don't think anybody cares (yet) about ordered non-unital semirings.

Haha, fair point. Hope no one does in the future!

Why wouldn't you care about C₀(X, ℝ≥0) for X a locally compact Hausdorff space?

I would, I like my things very general. It would seem that the future is right now.

[Jireh Loreaux]

@Kevin Buzzard :up: but, more (or perhaps, equally?) generally, the positive elements in a non-unital commutative C⋆-algebra will be an ordered non-unital semiring. Whether I actually need that as a type class or not is less clear, because it will be a StarOrderedRing, so :shrug:

[Damiano Testa]

@Jireh Loreaux, maybe I missed this, but is it the case for the rings that you work on that the sign of a product is determined by the sign of the factors in the "obvious" way? E.g. can you multiply negative elements and obtain a strictly negative element?

[Jireh Loreaux]

no, that's not possible.

[Damiano Testa]

Ok, so, as far as I can tell, every "actual" instance of a LinearOrderedSemiring in mathlib seems to satisfy the stronger condition that products of negatives is positive (zeros being included on either the negative or the positive side).

[Damiano Testa]

This may be a case for at least introducing this typeclass, whether or not it should replace the current LinearOrderedSemiring is maybe a separate question.

[Jireh Loreaux]

Oh, by the way, I have no nice examples off hand of non-unital linear ordered semirings.

[Damiano Testa]

Ok, the typeclass that I had in mind simply would assume a preorder, maybe, a semiring and then some monotonicities (likely as in the current OrderedSemiring) and the new thing: the product of negative elements is non-negative.

[Yaël Dillies]

I think a better new is that multiplication by a negative (/nonpositive, but I hate this word) element is antitone.

[Damiano Testa]

Yes, that is another possibility and I do not have an example showing that it is actually stronger than just asking it for products of negatives.

[Damiano Testa]

I simply thought that a (on the surface) weaker axiom might be preferable. But I'm not going to make a PR anytime soon anyway!

[Damiano Testa]

Also, I like the automatic symmetry of the weaker assumption, as opposed to having to distinguish between left and right. Anyway, I think that once there is a consensus on wanting a stronger typeclass, we can discuss which strengthening is desired.

[Anatole Dedecker]

Isn’t that the point where we decide to add mixins instead of adding even more nodes to the instance tree? You obviously have all thought more about this than I have, but if there’s one place where I feel like we could use more mixins it’s the intersection of the algebraic and order hierarchies. IMHO things like docs#NormedLinearOrderedField (picked this one since I introduced it a while ago) should just not exist in the first place

[Yaël Dillies]

Actually, I feel like we're starting to get a mixin clutter at the intersection of the algebraic and order hierarchies... NormedLinearOrderedField is the intersection of the algebraic, order and norm hierarchies, btw.

[Yaël Dillies]

Regardless, you're missing the point, Anatole. The current plan is not to add any typeclass but to strengthen an existing one.

[Anatole Dedecker]

True, but it’s starting to feel more and more like a bunch of nice properties put together, at which point you might as well just use the mixins that you need. But again I haven’t thought about it carefully (as shown by the fact that my example doesn’t show what I wanted it to show) so don’t give too much importance to what I say.

[Anatole Dedecker]

Actually I’m getting curious, could you expand on the mixin clutter?

[Flo (Florent Schaffhauser)]

Jireh Loreaux said:

Oh, by the way, I have no nice examples off hand of non-unital linear ordered semirings.

What do you mean by nice here? Is there another property that you would want such an example to satisfy?

[Jireh Loreaux]

By "nice" I mean, "come up in mathematical practice" (e.g., like the C₀(X, ℝ≥0) example I gave without the linear order condition)

[Flo (Florent Schaffhauser)]

I still feel that the even natural numbers should be a go-to example of what you are looking for here :sweat_smile:

[Jireh Loreaux]

Lol, yes, but when do you ever use those in that capacity?

[Flo (Florent Schaffhauser)]

Touché :joy:

[Yuyang Zhao]

Anatole Dedecker said:

True, but it’s starting to feel more and more like a bunch of nice properties put together, at which point you might as well just use the mixins that you need. But again I haven’t thought about it carefully (as shown by the fact that my example doesn’t show what I wanted it to show) so don’t give too much importance to what I say.

I tried to make CanonicallyOrdered... a mixin earlier in #6326, but I haven't found out what was causing a ton of timeouts.

[Flo (Florent Schaffhauser)]

Riccardo Brasca said:

I don't have a good example of a LinearOrderedSemiring that is not a subset of a LinearOrderedRing, but my intuition suggest that ≤ a ^ 2 should always be true.

Is there a chance these could be equivalent properties? Meaning, does a LinearOrderedSemiring embed (in a sense to be made precise) in a LinearOrderedRing if and only if the squares are non-negative?

[Kevin Buzzard]

The proof strategy is clear: you additively invert all elements, this is an injection, you attempt extend <= in the only way you can and then you see what happens when you try and prove everything. Squares are funny in characteristic 2 (in particular knowing things about squares doesn't mean you know things about products) but that can't happen here because of the order.

[Damiano Testa]

I think the "invert => injection" is not entirely clear, but maybe cancellativity of addition is actually sufficient. I never fully convinced myself of that.

[Damiano Testa]

Ok, I was wrong: cancellativity and the fact that addition is commutative are enough: https://math.stackexchange.com/questions/3516249/prove-that-every-abelian-cancellation-semigroup-can-be-imbedded-in-a-group

I was mixing add and mul.

[Flo (Florent Schaffhauser)]

Oh, right, the cancellativity! We thought about that with Riccardo Brasca but I had forgotten :sweat_smile: Maybe that is the abstract condition we should incorporate, then?

[Damiano Testa]

Cancellativity should follow from the iff with monotonicity of addition, so that's ok, I think.

[Flo (Florent Schaffhauser)]

Sorry, what do you mean by 'the iff' here?

[Damiano Testa]

There are fields add_le_add and le_add, that make the inequality of adds and iff (sorry, I'm on mobile!).

[Damiano Testa]

Combining that with a linear order you should get cancellativity of addition. My previous comment was very compressed!

[Flo (Florent Schaffhauser)]

Got it, thanks!

[Damiano Testa]

I wonder how long will it take for the bits of imprecise statements to be automatically converted into a formal proof, without further human assistance...

[Flo (Florent Schaffhauser)]

(your suggestion to look at things like #add_le_add_iff_left clarified it for me)

[Damiano Testa]

There might already be a lemma that says that add is strictly monotone and maybe even a cancel... instance.

[Riccardo Brasca]

Are we sure we can also extend the order?

[Damiano Testa]

Extending preserving addition, I think so. Multiplication... I am really not sure.

[Flo (Florent Schaffhauser)]

Yes, that is not so clear, I agree

[Kevin Buzzard]

Why are people focussed on "squares are nonnegative" rather than "if x,y>=0 then so is x*y"? What's the relationship between those two statements?

[Riccardo Brasca]

This is docs#mul_nonneg and it is already true

[Yaël Dillies]

The problem is when x, y <= 0, Kevin.

[Kevin Buzzard]

But in the ring can't you just prove x>=0 iff -x<=0?

[Kevin Buzzard]

i think I must be missing the point

[Yaël Dillies]

Yeah, in a ring. We're talking about semirings here.

[Riccardo Brasca]

In a ring sure, the discussion is about a semiring.

[Kevin Buzzard]

Then I've lost track of the question. I thought the question was about extending <= from a semiring to a ring.

[Riccardo Brasca]

We are wondering if a semiring such that all squares are nonnegative (or maybe such that the product of nonpositive is nonnegative, we don't know it they're equivalent) can be embedded in an ordered ring.

[Mario Carneiro]

I assume the ordered ring in question is (WLOG) the AddLocalization of the semiring?

[Mario Carneiro]

which extends all the operations except for the order

[Yaël Dillies]

I already proved it extends the order: docs#AddLocalization.orderedAddCancelCommMonoid What I don't believe is that it extends the multiplication in an order-preserving way.

[Kevin Buzzard]

OK so where does the following strategy become problematic:
1) We have a an ordered semiring
2) Extend the ordering to the ringification
3) x>=0 iff -x<=0 so everything is now easy

[Mario Carneiro]

I think part 3b "everything is now easy"

[Kevin Buzzard]

if x,y<=0 then xy=(-x)(-y) and -x>=0 and -y>=0 so done. What am I missing?

[Yaël Dillies]

Probably 2), given that we have an example of an ordered semiring where a square is negative.

[Kevin Buzzard]

but I thought we were linearly ordered here?

[Kevin Buzzard]

Probably mathlib thinks that the complexes are an example of an ordered semiring where a square is negative, but with linear orders this can't happen

[Kevin Buzzard]

or am I wrong?

[Mario Carneiro]

@Yaël Dillies you just said you already did 2

[Mario Carneiro]

although the theorems are only about LinearOrderedCancelCommMonoid and not anything with Group in the name

[Mario Carneiro]

so I'm not sure the negation is proved to be well behaved under the order

[Mario Carneiro]

although it doesn't seem like it should be hard

[Yaël Dillies]

Nonono! I said I showed that the localization was an ordered additive group, and we also know that it's a ring. What's missing is that it's an ordered ring (namely the interaction between the multiplication and the order).

[Kevin Buzzard]

but we know x>=0 and y>=0 implies xy>=0 in the semiring

[Mario Carneiro]

is that in the MonoidLocalization file?

[Yaël Dillies]

Mario Carneiro said:

although it doesn't seem like it should be hard

This part is easy. In fact, @Alex J. Best has a PR proving it. The thing is that it only works when you localize at the top submonoid.

[Kevin Buzzard]

which is what we're localizing at?

[Kevin Buzzard]

I still feel that I don't understand what the actual question is (and I have a meeting now so will stop adding my ill-informed comments to this thread for a while)

[Mario Carneiro]

hm, I'm thinking kevin is right

[Yaël Dillies]

Yes, I'm just explaining why we don't have it in mathlib yet. In mathlib we only have the general theory that works for all localizations, and nothing specific to the Grothendieck group construction.

[Mario Carneiro]

Wait, I can't find any theory about a ring structure on the AddLocalization, even without the order

[Mario Carneiro]

I can't even get

example {α : Type _} [LinearOrderedSemiring α] {a b : AddLocalization (⊤ : AddSubmonoid α)} :
    0 ≤ a → 0 ≤ b → (0 : AddLocalization (⊤ : AddSubmonoid α)) ≤ a * b := sorry

to typecheck because the multiplication doesn't exist

[Yaël Dillies]

Uh oh

[Riccardo Brasca]

Kevin Buzzard said:

OK so where does the following strategy become problematic:
1) We have a an ordered semiring
2) Extend the ordering to the ringification
3) x>=0 iff -x<=0 so everything is now easy

I think the problem is in 2. I see two questions (maybe some already answered..).

• Is the ringification a LinearOrderedRing (assuming we started with a LinearOrderedSemiring)?
• Is the localization map always injective?

The answer cannot be "yes", otherwise the strategy would work in general, but we have an example of a LinearOrderedSemiring with a negative square (something cannot exist in the ringification).

[Kevin Buzzard]

Oh the example is linearly ordered?? Then this is my mistake

[Mario Carneiro]

what is the example?

[Kevin Buzzard]

There is code above, posted by Riccardo and attributed to Bhavik but there's no mathematical explanation.

[Kevin Buzzard]

It seems to be $\N[\epsilon]$ with "epsilon infinitely negative" (so 100000+eps<0)

[Kevin Buzzard]

Oh I've now seen Bhavik's explanation

[Mario Carneiro]

what's the negative square in question? It's not epsilon^2 because that's zero

[Kevin Buzzard]

1+eps

[Kevin Buzzard]

This ring has very few positive elements

[Mario Carneiro]

oh, I thought it had to be a positive number squared

[Kevin Buzzard]

So it's totally breaking my mental model of ordered semirings, which involves having everything >=0

[Flo (Florent Schaffhauser)]

Riccardo Brasca said:

Kevin Buzzard said:

OK so where does the following strategy become problematic:
1) We have a an ordered semiring
2) Extend the ordering to the ringification
3) x>=0 iff -x<=0 so everything is now easy

I think the problem is in 2. I see two questions (maybe some already answered..).

1. Is the ringification a LinearOrderedRing (assuming we started with a LinearOrderedSemiring)?
2. Is the localization map always injective?

The answer cannot be "yes", otherwise the strategy would work in general, but we have an example of a LinearOrderedSemiring with a negative square (something cannot exist in the ringification).

Right. So, for 1, we are asking for a necessary and sufficient condition for the order of a LinearOrderedSemiring to extend to its
ringification (in a way that makes the ringification a LinearOrderedRing).

The fact that the squares should be non-negative is necessary. Is it sufficient?

[Kevin Buzzard]

Product of two nonpositives is nonnegative is a stronger statement and is also necessary

[Kevin Buzzard]

So one can ask two hopefully easier questions: first is product of nonpositives nonnegative sufficient for extension to find, and secondly whether product of <=0 is >=0 is the same as all squares >=0. These questions sound more reasonable. The second can maybe be attacked using (x+y)^2 and hopefully the first is easy

[Kevin Buzzard]

Now I've understood that semirings can be 99% negative elements I'm thinking that the definition of linear ordered semiring is not correct. It looks like what the books say for ordered rings, but with the absence of negation in semirings I feel like a < b -> c < 0 -> c * b < c * a should also be there as an axiom when we don't have negation.

[Kevin Buzzard]

This is not present in the ring case because you can just apply the c > 0 axiom to -c.

[Kevin Buzzard]

Then I bet ringification of a totally ordered semiring is a totally ordered ring

[Riccardo Brasca]

Is addition always cancellative?

[Kevin Buzzard]

Yes because of the order

[Kevin Buzzard]

If a+b=a+c then we can't have b<c because an axiom then says a+b<a+c

[Kevin Buzzard]

Oh wait that isn't an axiom :-/

[Riccardo Brasca]

This

import Mathlib.Algebra.Order.Ring.Defs

example [LinearOrderedSemiring α] : LinearOrderedCancelAddCommMonoid α :=
  { ‹LinearOrderedSemiring α› with }

works. It is the direct generalization of docs#LinearOrderedCommSemiring.toLinearOrderedCancelAddCommMonoid

[Kevin Buzzard]

So how does Bhavik's example fit into that story?

[Yaël Dillies]

Kevin Buzzard said:

If a+b=a+c then we can't have b<c because an axiom then says a+b<a+c

It's not an axiom but it's true

[Riccardo Brasca]

The ringification does not have a LinearOrderedRing instance

[Kevin Buzzard]

Ok then done :-)

[Riccardo Brasca]

By the way we can add my example, inferInstance, does not prove it.

[Kevin Buzzard]

So the issue with Bhavik's ring is not "squares can be negative" , it's "multiplication by negative elements does not reverse the order" which I think is a natural axiom.

[Kevin Buzzard]

Note that "multiplication by positive preserves <" and "multiplication by negative reverses <" implies no zero divisors

[Kevin Buzzard]

(because it implies the usual facts pos x neg is neg, neg x neg is pos)

[Kevin Buzzard]

In particular it implies squares are >= 0, which I feel is maybe a red herring

[Damiano Testa]

I see that most of the discussion from before I boarded my plane was resolved!

I just wanted to add something that has not been made explicit, but that might help: when you "ringify" by adding additive opposites, you may also add more positive elements. This is not in any way strange: the subsemiring of Nat[π] generated by {0, 1, π} does not contain π-1, but when you add opposites it will. Thus, extending the property that multiplication by positive elements is monotone involves checking more inequalities, after adding the opposites.

[Kevin Buzzard]

Right! This is why I'm arguing that only explaining what multiplication by positive elements does, in the context where you can't deduce what multiplying by negative elements does, is kind of a weird idea. In the presence of left and right inverse axioms for a group you only need one of mul_one and one_mul because you can deduce the other one using inverses. However in a monoid this is not the case and you need both. Similarly here I feel like if we're inventing things like linearly ordered semirings and we can't use neg to get the negative story from the positive story we should say what multiplication by a negative element does to the ordering, even though we don't need this for ordered rings.

[Flo (Florent Schaffhauser)]

Riccardo Brasca said:

Currently, a LinearOrderedSemiring is a nontrivial Semiring with a total order such that:

• a ≤ b → c + a ≤ c + b
• a + b ≤ a + c → b ≤ c
• 0 ≤ 1
• a < b → 0 < c → c * a < c * b
• a < b → 0 < c → a * c < b * c

So, just to make sure I understand: based on the previous discussion, the debate is whether to add the following to the list?

• a < b → c < 0 → c * b < c * a
• a < b → c < 0 → b * c < a * c

[Damiano Testa]

I would say that this is one of the main candidates, maybe with more discussion about where you want < and where you want ≤.

[Flo (Florent Schaffhauser)]

I see, thanks. Do we intend to proceed with the poll suggested by Riccardo? If so, perhaps we should lay out the options for change more clearly? Or is it too soon at this stage?

[Flo (Florent Schaffhauser)]

And I have a related question, which mixes math and programming.

In the mathlib definition of a #LinearOrderedField, the property zero_le_one : 0 ≤ 1 is listed as an axiom/constructor. But mathematically this is not necessary, because if 1<0 then 0 = 1 + (-1) < 0 + (-1) = -1 so 0 < (-1) * (-1) = 1.

So, what is the purpose of having it here? Note that I am criticising it, I merely want to understand why this choice has been made and what it permits :pray:

[Damiano Testa]

To answer zero_le_one: the field is defined by extending another typeclass. This means that you copy over the fields of that structure and zero_le_one comes for the ride.

[Flo (Florent Schaffhauser)]

OK, that makes sense! But I guess my question is: we are okay with this mathematically?

[Damiano Testa]

Wrt strengthening the assumptions on LinearOrderedSemiring, this is somewhat unusual since it means replacing a typeclass assumption that is more general with one that is less general. From the little movement that the poll above has, I suspect that people do not really have a strong opinion: the current system works and changing it is not a priority.

I think that trying out the change and checking that noneall of the "concrete" types still satisfies the stronger version would help.

[Damiano Testa]

Flo (Florent Schaffhauser) said:

OK, that makes sense! But I guess my question is: we are okay with this mathematically?

Mathematically I would say: it is provable, so adding it as an axiom is not going to cause any problems!

[Flo (Florent Schaffhauser)]

Flo (Florent Schaffhauser) said:

OK, that makes sense! But I guess my question is: we are okay with this mathematically?

More precisely: we would not define a LinearOrderedField with less axioms, and then show that it satisfies the properties of a LinearOrderedCommRing in order to define instance LinearOrderedField.toLinearOrderedCommRing?

[Flo (Florent Schaffhauser)]

Damiano Testa said:

Flo (Florent Schaffhauser) said:

OK, that makes sense! But I guess my question is: we are okay with this mathematically?

Mathematically I would say: it is provable, so adding it as an axiom is not going to cause any problems!

Yes, can't argue with that!

[Damiano Testa]

With formalization, not always the minimal set of axioms works well. If you look at the implementation of AddMonoid (maybe?), there are nsmul fields that are helpful to suggest better versions of the automatic instance. This is only a computer-generated issue, not a mathematical one. These fields are often left out to their default values, but sometimes it is helpful to control what they are.

[Flo (Florent Schaffhauser)]

Damiano Testa said:

Wrt strengthening the assumptions on LinearOrderedSemiring, this is somewhat unusual since it means replacing a typeclass assumption that is more general with one that is less general. From the little movement that the poll above has, I suspect that people do not really have a strong opinion: the current system works and changing it is not a priority.

Yes, that makes sense. I suppose I am using this as an example to understand the structure of the library and how it is built, going from more general to less general, which occasionally causes things like this to happen.

[Flo (Florent Schaffhauser)]

Damiano Testa said:

With formalization, not always the minimal set of axioms works well.

Thanks, that's what I wanted to have confirmed.

[Kevin Buzzard]

You can make the constructor which doesn't ask for a proof of this axiom and then proves it using the argument above; that way users don't have to prove it. Groups have both mul_one and one_mul and you don't need one of them, it's only there because they extend monoids that this happens. But Chris Hughes recently PRed constructors which don't need all these extra axioms. The actual definitions of things -- what's going on under the hood -- shouldn't be a mathematician's concern.

[Damiano Testa]

Also, this is where someone comes along and says "but there is a definition of groups that only uses one identity, why don't you use that?". The answer is that sometimes laying out your assumptions better and possibly with redundancies may simplify your life later on.

[Flo (Florent Schaffhauser)]

Kevin Buzzard said:

You can make the constructor which doesn't ask for a proof of this axiom and then proves it using the argument above; that way users don't have to prove it. Groups have both mul_one and one_mul and you don't need one of them, it's only there because they extend monoids that this happens. But Chris Hughes recently PRed constructors which don't need all these extra axioms. The actual definitions of things -- what's going on under the hood -- shouldn't be a mathematician's concern.

Ok, great! I will look for examples. But I understand what you're saying: if somebody comes along and want to define an order on a specific field F that they are interested in, they should not have to prove that 0 < 1.

[Kevin Buzzard]

Look at #6472 for example. Chris makes new functions which take smaller axiom sets and produce rings and fields by proving the remaining axioms. The fact that this is not the definition doesn't matter. Mathematicians often say "the following are equivalent... And a ring satisfying any one of these is said to be a DVR" or whatever. Lean has to choose one of them to be the actual definition. But which one it chooses shouldn't be relevant to the user as long as they have access to the theorem.

[Flo (Florent Schaffhauser)]

Yes, I am absolutely on board with this policy but it is helpful to have it spelled out explicitly.

[Yaël Dillies]

Damiano Testa said:

I think that trying out the change and checking that none of the "concrete" types still satisfies the stronger version would help.

All of them, you mean?

[Damiano Testa]

Yaël, I edited my comment above, thanks!

[James Borger]

(deleted)

[James Borger]

Scott Morrison said:

James Borger, do you care about semirings with linear orders? If so, do you think that 0 \le a^2 is always true?

8:55 PM

There are some subrings with linear orders which I care about (e.g. the natural numbers). But I haven't had a need to think about the class of all linearly ordered semirings. For me, they don't form such a well-behaved class. For instance, they're not closed under cartesian products.

(I hope this works. First time here. I was just summoned from the void.)