## Stream: Is there code for X?

### Topic: Semifields?

#### 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.

#### Ryan Lahfa (Feb 01 2021 at 17:31):

Someone just told me 'division semiring' now :D

#### Alex J. Best (Feb 01 2021 at 17:35):

@Yury G. Kudryashov was adding these in #5539

#### 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)

#### 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

#### Ryan Lahfa (Feb 01 2021 at 17:38):

Nat substraction is frightening

#### 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

#### Ryan Lahfa (Feb 01 2021 at 17:39):

I was planning to use it

#### Mario Carneiro (Feb 01 2021 at 17:42):

Why are semifields needed here?

#### Mario Carneiro (Feb 01 2021 at 17:43):

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

#### Eric Wieser (Feb 01 2021 at 17:44):

Are the positive non-negative rationals a semifield?

no 0

#### Eric Wieser (Feb 01 2021 at 17:45):

Pretend I said non-negative

#### Eric Wieser (Feb 01 2021 at 17:45):

I suppose you could argue those are not of interest

#### Mario Carneiro (Feb 01 2021 at 17:46):

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

#### Mario Carneiro (Feb 01 2021 at 17:46):

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

#### Ryan Lahfa (Feb 01 2021 at 17:47):

Isn't max-plus algebra semifield?

#### Johan Commelin (Feb 01 2021 at 17:47):

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

(R, max, +)

#### 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

#### 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.

#### 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

#### 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

#### Eric Wieser (Feb 01 2021 at 17:59):

We have two examples - field and nnreal

#### 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

#### 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

#### 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

#### 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

#### 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

#### Mario Carneiro (Feb 01 2021 at 18:03):

The cost of copy paste is actually not that high

#### Eric Wieser (Feb 01 2021 at 18:03):

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

#### Eric Wieser (Feb 01 2021 at 18:05):

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

#### Adam Topaz (Feb 01 2021 at 18:05):

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

#### Adam Topaz (Feb 01 2021 at 18:05):

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

#### Mario Carneiro (Feb 01 2021 at 18:06):

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

#### 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

#### Adam Topaz (Feb 01 2021 at 18:06):

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 (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.

#### 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

#### 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.

#### Yury G. Kudryashov (Feb 01 2021 at 18:46):

I found nnreal very useful here and there in analysis.

#### Yury G. Kudryashov (Feb 01 2021 at 18:46):

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

#### 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

#### Mario Carneiro (Feb 01 2021 at 18:50):

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

#### Mario Carneiro (Feb 01 2021 at 18:50):

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

#### 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

#### 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

#### 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

#### 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.

#### 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