Opposite ring

[Alizter]

We should define the opposite ring and remove the duplication in the theory of ideals.

[Alizter]

It occurs to me that if we want R^op^op to be definitionally R then we need to duplicate the associativity data. For Ring, we could have an extra field that keeps track of the inverse of associativity and switches the data around when opped. I think the duplication op saves is much more of a benefit than the duplication in the definition.

[Alizter]

After some quick experimentation I noticed that a ring R has quite a few bits of duplicate data that causes equality not to hold:

sg_set0 = sg_set
sg_ass0 = sg_ass
monoid_left_id0 = monoid_left_id
monoid_right_id0 = monoid_right_id
negate_l0 = negate_l
negate_r0 = negate_r
abgroup_commutative0 = abgroup_commutative
sg_set1 = sg_set

This is obviously not ideal and needs to be cleaned up.

[jdchristensen]

Right, the issue is that IsRing contains ring_abgroup :: @IsAbGroup plus_is_sg_op zero_is_mon_unit _;.

About R^op^op being definitionally R, it's possible that it won't come up as often as opposite categories do, but it's worth thinking about. One can also reverse groups, semigroups, monoids, etc, and it's probably not worth adding extra associativity clauses for all of these.

[Alizter]

Hmm it's a lot more work to change up the definitions in mathclasses. I've wanted to refine the hierarchy for a while now, but I don't have to motivation to do it here. I managed to get opposites working by carefully picking apart the data and making sure the correct data gets put back. This should be good enough for now.

[mikeshulman]

If one were designing an algebraic hierarchy from the ground up, one might consider abstracting out a notion of "involutive equality", proving general properties about it, and then just phrasing all the algebraic definitions in terms of it.

[Alizter]

If I were designing things from the ground up, I would even consider making everything a setoid and having equality as a special case. There is would make sense to have "involutive equality". It would have a lot of unifying potential with non-set based structures.

However I am not particular keen on doing this. At the end of the day, the real motivation behind any algebra that I do is to do some actual calculations in homotopy theory. :)

[jdchristensen]

Hmm it's a lot more work to change up the definitions in mathclasses

Why do you need to change things there? Can't you just drop the abelian group structure from the Ring Record you defined, and then define a coercion to AbGroup? Carrying around two abelian group structures seems like a recipe for problems.

(Edit: changed "here" to "there" in first sentence.)

[Alizter]

Hmm it's a lot more work to change up the definitions in mathclasses

Why do you need to change things there? Can't you just drop the abelian group structure from the Ring Record you defined, and then define a coercion to AbGroup? Carrying around two abelian group structures seems like a recipe for problems.

(Edit: changed "here" to "there" in first sentence.)

Oh I see what you mean now. Maybe that is possible.

[Alizter]

This is finished now, but I'll make an issue about removing some of the redundant fields from Ring and AbGroup.