[Merged by Bors] - refactor(algebra/ring_quot.lean): make ring_quot irreducible

[sgouezel]

The quotient of a ring by an equivalence relation which is compatible with the operations is still a ring. This is used to define several objects such as tensor algebras, exterior algebras, and so on, but the details of the construction are irrelevant. This PR makes ring_quot irreducible to keep the complexity down.

[eric-wieser]

This scares me a little - it sounds like algebra_map R 1 (clifford_algebra Q) is no longer defeq to 1, which seems like a useful property to have.

[sgouezel]

defeqness is nice when you can have it, but not really important IMHO: there are many situations where algebra_map R 1 S is not defeq to 1, but it is not a problem since you can rewrite it away.

[sgouezel]

For instance, I just checked and algebra_map ℕ ℝ 1 = 1 is not definitional.

[eric-wieser]

Sure, but that's because the reals just underwent the same refactor! From reading the source alone, I think that both matrix_algebra and triv_sq_zero_ext satisfy this.

[eric-wieser]

This is used to define several objects such as tensor algebras, exterior algebras, and so on, but the details of the construction are irrelevant.

While this is true, in principle ring_quot could be used for any of the things ideal.quotient is currently used for today, right? If there are reasons that it's useful for ideal.quotient to be reducible, presumably those translate here.

On the other hand, the performance is obviously a real issue now, but the definitional transparency is at worst a slight inconvenience,

[sgouezel]

I'd say ideal.quotient should also be irreducible for the same reasons.

[eric-wieser]

@Vierkantor, what was the original motivation for the refactor that made div no longer defeq to a combination of mul and inv? Was definitional equality relevant at all? I'm curious if the rationale there is relevant here.

[Vierkantor]

@Vierkantor, what was the original motivation for the refactor that made div no longer defeq to a combination of mul and inv? Was definitional equality relevant at all? I'm curious if the rationale there is relevant here.

The motivation was the following: the previous has_div instance deriving from group_with_zero was defeq-incompatible with the has_div instance on fractional_ideal. Under certain conditions you want group_with_zero (fractional_ideal _), so you need to be able to specify the value of has_div.div arising from group_with_zero, otherwise you get non-defeq diamond instances.

[Vierkantor]

For this PR, I'm willing to accept the non-defeqness, since it looks like you still have that one expression 1 : clifford_algebra Q is always defeq to another 1 : clifford_algebra Q.

[eric-wieser]

Ah, so the previous problem was a diamond which required control of definitional equality, whereas here there's no diamond to introduce.

[Vierkantor]

Looks good to me, and let's get this merged before it breaks again.

bors d+

[bors]

✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[sgouezel]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests