Semifields?

Stream: Is there code for X?

[Ryan Lahfa]

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.

[Ryan Lahfa]

Someone just told me 'division semiring' now :D

[Alex J. Best]

@Yury G. Kudryashov was adding these in #5539

[Yakov Pechersky]

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

[Ryan Lahfa]

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

[Ryan Lahfa]

Nat substraction is frightening

[Ryan Lahfa]

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

[Alex J. Best]

Did you already see docs#geom_sum_inv

[Ryan Lahfa]

I was planning to use it

[Mario Carneiro]

Why are semifields needed here?

[Mario Carneiro]

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

[Eric Wieser]

Are the positive non-negative rationals a semifield?

[Mario Carneiro]

no 0

[Eric Wieser]

Pretend I said non-negative

[Eric Wieser]

I suppose you could argue those are not of interest

[Mario Carneiro]

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

[Mario Carneiro]

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

[Ryan Lahfa]

Isn't max-plus algebra semifield?

[Johan Commelin]

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

[Ryan Lahfa]

(R, max, +)

[Mario Carneiro]

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

[Alex J. Best]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Eric Wieser]

We have two examples - field and nnreal

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Mario Carneiro]

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

[Eric Wieser]

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

[Mario Carneiro]

The cost of copy paste is actually not that high

[Eric Wieser]

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

[Mario Carneiro]

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

[Eric Wieser]

Performance tradeoffs should only be made after measuring

[Eric Wieser]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Adam Topaz]

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

[Alex J. Best]

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.

[Mario Carneiro]

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

[Johan Commelin]

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

[Yury G. Kudryashov]

I found nnreal very useful here and there in analysis.

[Yury G. Kudryashov]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Damiano Testa]

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

[Anne Baanen]

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