A semiring isomorphic to

Stream: new members

[Damiano Testa]

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]

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

[Johan Commelin]

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]

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

[Damiano Testa]

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

[Johan Commelin]

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]

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]

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

[Damiano Testa]

ah, I see, subsemirings up to injections!

[Johan Commelin]

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

[Damiano Testa]

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

[Eric Wieser]

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

[Damiano Testa]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

Properties of bundled homs don't compose well

[Johan Commelin]

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

[Damiano Testa]

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]

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

[Eric Wieser]

@Johan Commelin, probably yeah

[Eric Wieser]

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

[Damiano Testa]

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

[Damiano Testa]

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?

[Johan Commelin]

I don't know...

[Johan Commelin]

Both concepts might be useful

[Damiano Testa]

I will try!

[Johan Commelin]

For toric your version might be good enough :bulb:

[Johan Commelin]

And then nat -> real might be another interesting example

[Damiano Testa]

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

[Damiano Testa]

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