Zulip Chat Archive

Stream: Is there code for X?

Topic: Semifields?


view this post on Zulip Ryan Lahfa (Feb 01 2021 at 17:28):

I'm trying to prove something like this:

import algebra.geom_sum

lemma geom_sum_eq_factor_inv_geom_sum
  {α} [field α]
  (x: α) (n: ):
  geom_series x n = (x ^ (n - 1)) * geom_series (x⁻¹) n :=
  sorry

And I wonder if there is something to say: I want a semiring with multiplicative inverses, which I think, are called semifields.

view this post on Zulip Ryan Lahfa (Feb 01 2021 at 17:31):

Someone just told me 'division semiring' now :D

view this post on Zulip Alex J. Best (Feb 01 2021 at 17:35):

@Yury G. Kudryashov was adding these in #5539

view this post on Zulip Yakov Pechersky (Feb 01 2021 at 17:37):

You might have more fun proving this if you express it as geom_series x (n + 1) = (x ^ n) * geom_series (x \-) (n + 1)

view this post on Zulip Ryan Lahfa (Feb 01 2021 at 17:37):

Yakov Pechersky said:

You might have more fun proving this if you express it as geom_series x (n + 1) = (x ^ n) * geom_series (x \-) n

Indeed

view this post on Zulip Ryan Lahfa (Feb 01 2021 at 17:38):

Nat substraction is frightening

view this post on Zulip Ryan Lahfa (Feb 01 2021 at 17:38):

Alex J. Best said:

Yury G. Kudryashov was adding these in #5539

Thanks for the reference! Will wait for them, meanwhile, it will be just field

view this post on Zulip Alex J. Best (Feb 01 2021 at 17:38):

Did you already see docs#geom_sum_inv

view this post on Zulip Ryan Lahfa (Feb 01 2021 at 17:39):

I was planning to use it

view this post on Zulip Mario Carneiro (Feb 01 2021 at 17:42):

Why are semifields needed here?

view this post on Zulip Mario Carneiro (Feb 01 2021 at 17:43):

Are there any concrete semifields of interest that aren't fields already?

view this post on Zulip Eric Wieser (Feb 01 2021 at 17:44):

Are the positive non-negative rationals a semifield?

view this post on Zulip Mario Carneiro (Feb 01 2021 at 17:44):

no 0

view this post on Zulip Eric Wieser (Feb 01 2021 at 17:45):

Pretend I said non-negative

view this post on Zulip Eric Wieser (Feb 01 2021 at 17:45):

I suppose you could argue those are not of interest

view this post on Zulip Mario Carneiro (Feb 01 2021 at 17:46):

I think you see where I'm going with this...

view this post on Zulip Mario Carneiro (Feb 01 2021 at 17:46):

Yes you can always take an algebraic object and chop it in half

view this post on Zulip Ryan Lahfa (Feb 01 2021 at 17:47):

Isn't max-plus algebra semifield?

view this post on Zulip Johan Commelin (Feb 01 2021 at 17:47):

There is a lot of stuff about nnreal in mathlib. That is a "serious" type.

view this post on Zulip Ryan Lahfa (Feb 01 2021 at 17:47):

(R, max, +)

view this post on Zulip Mario Carneiro (Feb 01 2021 at 17:50):

Okay, I grant that nnreal is a useful example, but you need at least two examples to make generalization worthwhile, and max-plus is not in mathlib AFAIK

view this post on Zulip Alex J. Best (Feb 01 2021 at 17:54):

Right, but won't it be easier to add max-plus if there is already an api for semifield, nobody wants to add a definition with no supporting lemmata but writing a bunch of things for max-plus which will then be generalised and unified with nnreal later by making them both semifields seems a bit inefficient.

view this post on Zulip Mario Carneiro (Feb 01 2021 at 17:57):

Adding a new algebraic class means a lot of API to fill out, and longer typeclass instances for everything else. It's something to avoid if at all possible

view this post on Zulip Mario Carneiro (Feb 01 2021 at 17:58):

For sure it's more than you would have if you just proved theorems on both types independently

view this post on Zulip Eric Wieser (Feb 01 2021 at 17:59):

We have two examples - field and nnreal

view this post on Zulip Eric Wieser (Feb 01 2021 at 18:00):

I don't think you need two examples to insert a new entry between two existing typeclasses - inserting one still means that you can reuse existing lemmas for your new weaker object

view this post on Zulip Eric Wieser (Feb 01 2021 at 18:01):

Most of the API to "fill out" would just be moving relevant bits of API from field to semifield

view this post on Zulip Eric Wieser (Feb 01 2021 at 18:01):

It's the algebraic _structures_ like subfield that cause the huge amount of pain to fill out

view this post on Zulip Mario Carneiro (Feb 01 2021 at 18:02):

Yes, but that doesn't change the fact that now typeclass instances will have to stop at one more intermediate node while trying to show that a field has a plus

view this post on Zulip Eric Wieser (Feb 01 2021 at 18:02):

IMO the cost of humans duplicating lemmas is way higher than a small slowdown to typeclass search

view this post on Zulip Mario Carneiro (Feb 01 2021 at 18:03):

The cost of copy paste is actually not that high

view this post on Zulip Eric Wieser (Feb 01 2021 at 18:03):

Every duplicate lemma we have makes auto-complete and doc-gen search less effective

view this post on Zulip Mario Carneiro (Feb 01 2021 at 18:03):

it's a little inelegant, but that's what the tradeoff is about

view this post on Zulip Eric Wieser (Feb 01 2021 at 18:05):

Performance tradeoffs should only be made after measuring

view this post on Zulip Eric Wieser (Feb 01 2021 at 18:05):

Ie, add semifield, and see if the slowdown is actually relevant

view this post on Zulip Adam Topaz (Feb 01 2021 at 18:05):

One more example: The Krasner semifield: {0,1}\{0,1\} with 1+1=11 + 1 = 1.

view this post on Zulip Adam Topaz (Feb 01 2021 at 18:05):

Or is this called the boolean semifield? I don't remember.

view this post on Zulip Mario Carneiro (Feb 01 2021 at 18:06):

I don't doubt that examples can be made to fit the definition

view this post on Zulip Mario Carneiro (Feb 01 2021 at 18:06):

I can come up with lots of examples of moufang loops but that doesn't mean mathlib needs to have the definition

view this post on Zulip Adam Topaz (Feb 01 2021 at 18:06):

A morphism from a commutative ring AA to {0,1}\{0,1\} is "the same" as a prime ideal. Sorry that was wrong (you need to consider {0,1}\{0,1\} as a hyperfield, not a semifield, where 1+1={0,1}1 + 1 = \{0,1\}, then it becomes true.)

view this post on Zulip Alex J. Best (Feb 01 2021 at 18:14):

Mario Carneiro said:

The cost of copy paste is actually not that high

Personally I find copy pasting quite annoying, there are variables and sections and namespaces etc to consider, it can often be a bigger job than ctrl-c ctrl-v.
And thats if people remember to copy paste, I think there's a maintenance burden on people to either always double check whether a lemma they prove for field or division ring also may apply to nnreal and copy paste it, in practice nobody does this so it seems to me we would miss potentially useful results this way.

view this post on Zulip Mario Carneiro (Feb 01 2021 at 18:30):

Well this is in part the cost of keeping nnreal around as an algebraic object instead of just a subtype of real. I'm still not sure that was a good idea

view this post on Zulip Johan Commelin (Feb 01 2021 at 18:44):

If used real at the start of LTE, then switched to nnreal. I'm very happy with the change.

view this post on Zulip Yury G. Kudryashov (Feb 01 2021 at 18:46):

I found nnreal very useful here and there in analysis.

view this post on Zulip Yury G. Kudryashov (Feb 01 2021 at 18:46):

(e.g., as an algebraic type with norm_cast lemmas both to real and ennreal)

view this post on Zulip Mario Carneiro (Feb 01 2021 at 18:48):

But nnreal.lean isn't really that long of a file, and there aren't any subfiles, so I think the status quo is fine

view this post on Zulip Mario Carneiro (Feb 01 2021 at 18:50):

certainly anything about the coe to real isn't going to generalize to semifields

view this post on Zulip Mario Carneiro (Feb 01 2021 at 18:50):

and that's where most of the theorems are coming from

view this post on Zulip Mario Carneiro (Feb 01 2021 at 18:52):

in fact the only thing that looks like it would generalize is the last section section inv, which is more about canonically ordered semifields

view this post on Zulip Mario Carneiro (Feb 01 2021 at 18:54):

there is a definition of subtraction on nnreal, I don't know if we want a class for that (which it could share with nat) but general semifields don't have it

view this post on Zulip Johan Commelin (Feb 01 2021 at 19:49):

Note that a whole bunch of lemmas about nnreal were generalized to lin.ord.comm.grp with zero's

view this post on Zulip Damiano Testa (Feb 01 2021 at 20:13):

Sorry for spamming the conversation, but I cannot resist saying the Moufang loops actually paly a role in studying rational points on cubic hypersurfaces.

view this post on Zulip Anne Baanen (Feb 01 2021 at 21:27):

Another class of examples of semifields would be fractional ideals in a Dedekind domain (PR coming soon, hopefully!)


Last updated: May 16 2021 at 05:21 UTC