Ring/Semiring

Stream: Is there code for X?

[Antoine Chambert-Loir]

Does Mathlib know to get (Comm)Ring S from CommRing R, (Comm)Semiring S and Algebra R S?
This is mathematically quite obvious. Would adding an instance cause any trouble?

[Jireh Loreaux]

Yes, I think this is actually a big problem. It's because the new data (e.g., neg) will depend on the algebra structure. So if S is an algebra over two different rings R and R', then it will have two non-defeq neg functions. Even if you avoid that with Classical.choice or some such, you still have the problem that when S is already a ring, you have two negs (the one from the algebra structure and the fact that it is a semiring, and the one it is already endowed with).

[Jireh Loreaux]

You could add it as a def to use locally in proofs though.

[Antoine Chambert-Loir]

OK. For me it won't be a problem though, I'll do as in the classic litterature and stick to rings all along, the slight added generality has never been of any use.

[Antoine Chambert-Loir]

If I wanted to allow this generality, I would need to extend docs#RingQuot to semirings, which should not be a problem either, unless a semiring-quotient of a ring by an equivalence relation differs from its ring-quotient (does it?).

[Eric Wieser]

This exists and it's how we build the ring instance on TensorAlgebra

[Eric Wieser]

It's something like docs#Algebra.semiringToRing

[Antoine Chambert-Loir]

Thank you! Then it was probably a mistake of mine that triggered the problem.
Two additional questions regarding instances. Imagine I have some relation r on a CommSemiring R and I define a new type Aby def A := RingQuot r and I want Lean to know that A is a CommSemiring.

• There is an instanceRingQuot.instSemiring, but example : Semiring A := inferInstance does not work, unless I do dsimp [A]. Is this expected?

• Should I register all instances (CommSemiring…) explicitly, just the one which are the most general (hence CommSemiringbut not Semiring), or just the ones that I will specifically use?

[Eric Wieser]

Another option would be to make your A an abbrev

[Eric Wieser]

Or at least, do that until you have everything working, and copy across all the instances later

[Eric Wieser]

Just to give a warning about docs#Algebra.semiringToRing; I think I mispoke, and it's only used to construct the ring instance on the docs#FreeAlgebra; generally it should be a last resort when there is genuinely no reasonable way to inherit a ring structure