opposite rings

[Alizter]

This is a start on #1921. I've opened it now so I can get some comments before starting ideals.

TODO

• deduplicate theory of ideals
• right modules (perhaps in a later PR?)

[Alizter]

Mystery solved: Coq makes the :> fields in records "reversible" meaning that there is a term inserted during elaboration. We don't see this since we didn't include the following in our prelude:

#[universes(polymorphic=yes)] Definition ReverseCoercionSource (T : Type) := T.
#[universes(polymorphic=yes)] Definition ReverseCoercionTarget (T : Type) := T.
#[warning="-uniform-inheritance", reversible=no, universes(polymorphic=yes)]
Coercion reverse_coercion {T' T} (x' : T') (x : ReverseCoercionSource T)
  : ReverseCoercionTarget T' := x'.
Register reverse_coercion as core.coercion.reverse_coercion.

In this case, our CRing is being coerced (by a reversible coercion) to Ring. Then the involution happens definitionally giving us the same Ring. Coq then says this was coerced by a reversible coercion so let me insert the inverse and brings it back to a CRing.

I believe this is unintentional for this coercion to be marked as reversible and has been fixed upstream. coq/coq#18705 Edit: actually this won't fix this, but :> should always be regarded as reversible from now on. Not a big issue, but something to keep in mind.

We should add the code above so that Set Printing All better displays reversed coercions.

Thanks @SkySkimmer for explaining the behaviour on Zulip.

[jdchristensen]

Ok, that's interesting. In any case, I still think we want to define crng_op and should change test2 to use it.

[Alizter]

I simplified the theory of ideals using the opposite ring. However in doing so I redefined the quotient/colon ideal as an intersection of the "left" and "right" versions. This has made the entire thing much more complicated so I don't know what to do with it.

I have scoured all the literature I know on noncommutative rings and I couldn't find anything about colon ideals in this generality. It only seems to appear in commutative algebra/algebraic geometry, in fact this was my original motivation for adding them as they describe complements in the Zariski topology.

I'm tempted to just move all the colon ideal stuff to CRing and only have the single two-sided definition.

[jdchristensen]

I simplified the theory of ideals using the opposite ring.

That turned out quite well!

I'm tempted to just move all the colon ideal stuff to CRing and only have the single two-sided definition.

I don't know much about this, but specializing to commutative rings seems fine to me, if that's all you can find written about this.

[jdchristensen]

If we have mult_assoc_opp take its arguments in the reverse order, then lines 428 and 433 will become simpler, and so rng_op will be slightly smaller. Probably worth it. For Is1Cat too.

[jdchristensen]

Same for the distributivity laws (which also comes up in my last commit, where I needed a fun x y => ...).

[Alizter]

I've changed mult_assoc_opp like you've suggested but I don't think its worth touching the distributivity laws in general. Your specific case isn't actually using the mathclasses distributivity but the ring law version.

However changing the order of those arguments will be confusing during use. The opp field isn't supposed to actually be used by anybody anyway.

[jdchristensen]

Do you still want to simplify colon ideals? It's ok with me either way.

[Alizter]

I think I won't touch it for the moment.

[jdchristensen]

LGTM