## Stream: new members

### Topic: A semiring isomorphic to

#### Damiano Testa (Mar 03 2021 at 10:18):

Dear All,

in the code below, I define the subsemiring of non-negative elements of an ordered_semiring. After that, I would like to prove that, if I apply this construction starting from ℤ, I obtain ℕ. I know that in Type theory, this will not really be an equality, but I would like to be able to convert from one to the other easily. What can I do?

Also, any suggestions/improvements on the given definition are more than welcome!

Thanks!

import ring_theory.subsemiring

variables (R : Type*) [ordered_semiring R]

/--  The subtype of non-negative elements of R. -/
def pR : subsemiring R :=
{ carrier := {r : R | 0 ≤ r},
one_mem' := by simp only [set.mem_set_of_eq, zero_le_one],
mul_mem' := λ x y (x0 : 0 ≤ x) (y0 : 0 ≤ y), mul_nonneg x0 y0,
zero_mem' := rfl.le,
add_mem' := λ x y (x0 : 0 ≤ x) (y0 : 0 ≤ y), add_nonneg x0 y0 }

-- feel free to change this statement to something else that will still
-- assert that pR ℤ *is* ℕ!
lemma pR_Z_eq_N : pR ℤ ≃ ℕ := sorry


#### Johan Commelin (Mar 03 2021 at 10:20):

I think that, in addition to pR you also want a predicate is_nonneg_subsemiring N Z.

#### Johan Commelin (Mar 03 2021 at 10:21):

You should then:

1) Show that pR satisfies this predicate
2) Show that nat and int satisfy this predicate (and eg nnreal and real)
3) Use that predicate whenever you develop API in this setting.

#### Johan Commelin (Mar 03 2021 at 10:22):

In applications, you should then be able to freely switch between pR or nat, etc

#### Damiano Testa (Mar 03 2021 at 10:22):

Ok, thanks Johan! I will process this and report with more questions!

#### Johan Commelin (Mar 03 2021 at 10:23):

The predicate should probably assume that Z is an N-algebra, and then just require that the image of N is positive, algebra_map is injective, and for every positive element, there exists a preimage.

#### Damiano Testa (Mar 03 2021 at 10:23):

The predicate is_nonneg_subsemiring is a predicate on subsemirings of a general ordered_semiring, right? And it simply checks that all the elements are non-negative, I imagine

#### Johan Commelin (Mar 03 2021 at 10:23):

No, not on subsemirings, because then nat will not be an example.

#### Damiano Testa (Mar 03 2021 at 10:24):

ah, I see, subsemirings up to injections!

#### Johan Commelin (Mar 03 2021 at 10:24):

It should be a predicate on two types, [semiring N] [ordered_semiring Z] [algebra N Z]

#### Damiano Testa (Mar 03 2021 at 10:25):

I get it now and it already addresses some of the issues that I was experiencing in my naïve approach!

#### Eric Wieser (Mar 03 2021 at 10:26):

Don't you want the stronger statement pR ℤ ≃+* ℕ?

#### Damiano Testa (Mar 03 2021 at 10:27):

Eric, yes, definitely! I thought that the iso symbol meant what I can see now that your symbol means!

#### Eric Wieser (Mar 03 2021 at 10:27):

You might of course also want pR ℤ ≃o ℕ, once the order PR stuff we worked on gets merged

#### Eric Wieser (Mar 03 2021 at 10:27):

Unfortunately there's no ≃o+* I don't think

#### Eric Wieser (Mar 03 2021 at 10:27):

Properties of bundled homs don't compose well

#### Johan Commelin (Mar 03 2021 at 10:27):

@Eric Wieser this is a consequence of what I sketched, right?

#### Damiano Testa (Mar 03 2021 at 10:29):

Yes, I definitely want all these things, but I am hoping that with the setup that Johan suggested, they will fall through.

Also, Eric, the PR that is causing you so much pain was my attempt at a start of this project...

#### Eric Wieser (Mar 03 2021 at 10:30):

At this point I think everything is resolved, and I just need to wait for the build queue to clear

#### Eric Wieser (Mar 03 2021 at 10:30):

@Johan Commelin, probably yeah

#### Eric Wieser (Mar 03 2021 at 10:31):

You may be interested in docs#nonneg_ring, although I think that's not quite what you're asking for

#### Damiano Testa (Mar 03 2021 at 10:31):

Eric, thank you so much for your help with the earlier, shattered, PR!

#### Damiano Testa (Mar 03 2021 at 10:35):

Johan, is there any reason for wanting N to be all non-negative elements? Would it not be enough to ask that all the elements of N map to non-negative ones?

Will I get in trouble down the road if I allow subrings of non-negative elements that are not all of the non-negative elements?

I don't know...

#### Johan Commelin (Mar 03 2021 at 10:38):

Both concepts might be useful

I will try!

#### Johan Commelin (Mar 03 2021 at 10:39):

For toric your version might be good enough :bulb:

#### Johan Commelin (Mar 03 2021 at 10:39):

And then nat -> real might be another interesting example

#### Damiano Testa (Mar 03 2021 at 10:40):

Exactly, this is what I wanted. Also nat -> rat

#### Damiano Testa (Mar 03 2021 at 10:42):

I am going to try this definition:

def is_nonneg_subsemiring (N Z : Type*) [comm_semiring N] [ordered_semiring Z] [algebra N Z] :
Prop := injective (algebra_map N Z : N → Z) ∧ ∀ n : N, 0 ≤ algebra_map N Z n


Last updated: May 10 2021 at 18:22 UTC