Inv instances

Stream: mathlib4

[Antoine Chambert-Loir]

For what rings should there be an Inv instance that “computes” the inverse of an invertible element, extended in some way or some other?
My question stems out the will to extend MvPowerSeries.inv from fields to arbitrary rings. However, for the moment, this is made difficult by the fact that it relies on some implicit Inv k instance for a field k, and assuming Inv R when Ris a general ring does not seem to be sufficient. Replacing explicit inverses by Ring.inverse seems to be possible, though, but that will probably have a large number of side effects (maybe not…).

[Antoine Chambert-Loir]

What seems awkward to me is that rings have no Inv instance (that could rely on docs#Ring.inverse) while matrix rings (over a commutative ring) have one, given by docs#Matrix.inv.

[Kevin Buzzard]

What's the problem with just defining inv on an arbitrary monoid with 0 to be 0 if the element isn't invertible? I'm surprised we're not already doing this but something at the back of my mind is telling me that there's an issue with this idea

[Eric Wieser]

The issue is that makes inverse on Rat noncomputable

[Eric Wieser]

(and on matrices)

[Eric Wieser]

Also it means you can't write f \inv to mean "fun x => (f x)\inv`

[Mitchell Lee]

What's the inverse of $(0, 1) \in \mathbb{R} \times \mathbb{R}$? According to docs#Pi.inv_apply, it needs to be $(0, 1)$, not $0$. So I think it's not possible to declare the inverse of every noninvertible element to be $0$.

[Andrew Yang]

My guess: x ^ 2 * x⁻¹ = x.

[Ralf Stephan]

Niven (1969) defines the subtypes $P_0$ and $P_1$, where the power series have 0 or 1 as constant coefficient. Would subtyping be a solution?

[Antoine Chambert-Loir]

I should be clearer about what I intended to do.

For all rings, there is a docs#Ring.inverse function that returns their inverse for invertible elements, and zero otherwise.
Some rings have a docs#Inv instance that may coincide with docs#Ring.inverse, or not.
For example, docs#Pi.inv returns the pointwise inverse (so differs from docs#Ring.inverse), but docs#Matrix.inv is an docs#Inv instance that provides the same result as docs#Ring.inverse. Consequently, the identification of a product of matrix rings with the matrix ring of their products is not compatible with the two docs#Inv instances on that rings. They could be aligned by not using docs#Ring.inverse of the determinant, but a preferred docs#Inv instance on the coefficient ring.

For the moment, power series over a field have an docs#Inv instance, which is compatible with the output of docs#Ring.inverse, that relies on the natural (and reasonable) docs#Inv instance on a group with zero.
My goal was to extend it somewhat to arbitrary rings. The most natural thing would be to use a given docs#Inv instance on the coefficients, but docs#Inv does not provide any of the natural functional equations that make the construction meaningful. (I have not taken the time to check precisely which functional equations would be needed.)

[Eric Wieser]

I've thought about this issue too; but I think the only way out here is to add an inv field to monoids, constrained only when the argument is a unit, and defaulting this to Ring.inverse.

[Eric Wieser]

Note that if we don't build this into Monoid itself, then we end up with the unpleasantness of not being able to invert the identity matrix over integers

[Eric Wieser]

But if we do that, then docs#Monoid.ext stops being true!

[Antoine Chambert-Loir]

Of course, this new structure would be a “monoid with inv”, which is not at all a monoid. Possibly, this class structure would partially play the role that is now played by docs#GroupWithZero.
But maybe we could do things differently, for example, locally, we could start asking what Inv map we wish to use (thus removing most ambiguous Inv instances).

[Yaël Dillies]

I mean you're basically reinventing docs#DivisionMonoid. I even have a comment explaining the various axioms that you could weaken so that it applies to matrices

[Eric Wieser]

What would you weaken to make it apply to Int? (With inv defined on the units and zero everywhere else)

[Eric Wieser]

You don't even get div_eq_mul_inv there!