## Stream: Is there code for X?

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

#### 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,
simp [(has_neg.neg)],
nth_rewrite 1 ← one_smul ℤ a,
have : (int.neg 1 + 1) = 0,
{ change ((- 1 : ℤ) + 1 = 0),
rw [this, zero_smul],
end,
..(infer_instance : semiring S) }


#### 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,
simp [(has_neg.neg)],
nth_rewrite 1 ← one_smul R a,
have : (sub_neg_monoid.neg (1 : ℤ) • (1 : R) + 1) = 0,
{ change ((- 1 : R) + 1 = 0),
simpa [negZ], },
rw [this, zero_smul],
end,
..(infer_instance : semiring S) }


#### 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?

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

#### 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

#### 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!

#### 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