Zulip Chat Archive

Stream: new members

Topic: A semiring isomorphic to


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 03 2021 at 10:22):

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

view this post on Zulip Damiano Testa (Mar 03 2021 at 10:22):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 03 2021 at 10:23):

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

view this post on Zulip Damiano Testa (Mar 03 2021 at 10:24):

ah, I see, subsemirings up to injections!

view this post on Zulip Johan Commelin (Mar 03 2021 at 10:24):

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

view this post on Zulip 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!

view this post on Zulip Eric Wieser (Mar 03 2021 at 10:26):

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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 03 2021 at 10:27):

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

view this post on Zulip Eric Wieser (Mar 03 2021 at 10:27):

Properties of bundled homs don't compose well

view this post on Zulip Johan Commelin (Mar 03 2021 at 10:27):

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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 03 2021 at 10:30):

@Johan Commelin, probably yeah

view this post on Zulip 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

view this post on Zulip Damiano Testa (Mar 03 2021 at 10:31):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 03 2021 at 10:37):

I don't know...

view this post on Zulip Johan Commelin (Mar 03 2021 at 10:38):

Both concepts might be useful

view this post on Zulip Damiano Testa (Mar 03 2021 at 10:38):

I will try!

view this post on Zulip Johan Commelin (Mar 03 2021 at 10:39):

For toric your version might be good enough :bulb:

view this post on Zulip Johan Commelin (Mar 03 2021 at 10:39):

And then nat -> real might be another interesting example

view this post on Zulip Damiano Testa (Mar 03 2021 at 10:40):

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

view this post on Zulip 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