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

Stream: Is there code for X?

[Damiano Testa]

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

[Damiano Testa]

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

[Adam Topaz]

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

[Damiano Testa]

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)

[Eric Wieser]

Was it docs#algebra.semiring_to_ring?

[Eric Wieser]

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

[Damiano Testa]

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

[Eric Wieser]

docs#semimodule.add_comm_monoid_to_add_comm_group is similar

[Damiano Testa]

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