Zulip Chat Archive

Stream: Is there code for X?

Topic: Is there a `ring` instance on a semiring that is a ℤ-alge...


view this post on Zulip Damiano Testa (Mar 03 2021 at 04:17):

Dear All,

after the major breakdown that my last attempt with instances caused, I am a little worried about this one. Is there a ring instance on a semiring that is a ℤ-algebra?

In the code below, replacing the instances with by apply_instance does not work. Also, I imagine that there are easier proofs of the unique fact that this instance requires.

Thanks!

import algebra.algebra.basic

variables (S : Type*) [semiring S] [algebra  S]

instance negZ : has_neg S := λ r, (- 1 : )  r

instance Zalg.to_ring : ring S :=
{ neg := has_neg.neg,
  add_left_neg := λ a, begin
    simp [(has_neg.neg)],
    nth_rewrite 1  one_smul  a,
    rw  add_smul,
    have : (int.neg 1 + 1) = 0,
    { change ((- 1 : ) + 1 = 0),
      exact neg_add_self _ },
    rw [this, zero_smul],
  end,
  ..(infer_instance : semiring S) }

view this post on Zulip Damiano Testa (Mar 03 2021 at 04:28):

In fact, instead of ℤ, you could get the proof to work for a general comm_ring, instead:

variables (R S : Type*) [comm_ring R] [semiring S] [algebra R S]

instance negZ : has_neg S := λ r, (- 1 : R)  r

instance Zalg.to_ring : ring S :=
{ neg := λ r, (- 1 : R)  r,
  add_left_neg := λ a, begin
    simp [(has_neg.neg)],
    nth_rewrite 1  one_smul R a,
    rw  add_smul,
    have : (sub_neg_monoid.neg (1 : )  (1 : R) + 1) = 0,
    { change ((- 1 : R) + 1 = 0),
      convert neg_add_self (1 : R),
      simpa [negZ], },
    rw [this, zero_smul],
  end,
  ..(infer_instance : semiring S) }

view this post on Zulip Adam Topaz (Mar 03 2021 at 04:31):

Yeah this was an issue that came up a while ago. @Eric Wieser do you remember how this ended up?

view this post on Zulip Damiano Testa (Mar 03 2021 at 04:36):

I am worried that this might cause more trouble than the whole "subsets of semirings closed under addition and multiplication are semirings" mess. (PR #6489 et al)

view this post on Zulip Eric Wieser (Mar 03 2021 at 06:50):

Was it docs#algebra.semiring_to_ring?

view this post on Zulip Eric Wieser (Mar 03 2021 at 06:51):

Which isn't safe to use unless you know A and know you will be the only one to give it a ring instance

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

Thanks, this looks exactly what I was looking for! I will try to use it with care!

view this post on Zulip Eric Wieser (Mar 03 2021 at 08:42):

docs#semimodule.add_comm_monoid_to_add_comm_group is similar

view this post on Zulip Damiano Testa (Mar 03 2021 at 08:47):

Great, thanks! I may indeed want to convert between (semi)modules, when acquiring/losing subtractions!


Last updated: May 17 2021 at 14:12 UTC