LawfulInv

Stream: mathlib4

[Jireh Loreaux]

In #33441 @Frédéric Dupuis is introducing a LawfulInv class for monoids with zero which satisfies a⁻¹ is the actual inverse when a is a unit, and a⁻¹ = 0 for all nonunits. In this way it behaves like Ring.inverse and the Inv instance on matrices. The point is to add this class as a requirement for C⋆-algebras so that we can talk about a⁻¹ freely.

One question is: would the community be okay if we just added an Inv field to MonoidWithZero? Overall, I think this would provide a nice usability boost to inverses in rings (there's a reason we've taken this approach with Matrix after all). However, it would have some perhaps surprising consequences, such that endowing ℕ and ℤ with ⁻¹.

I'll note that even making LawfulInv a requirement for CStarAlgebra would mean that C(X, ℂ) would have an Inv instance for X a compact space, but not otherwise, unless we put one on explicitly. Optionally, we could scope the CStarAlgebra instance of that type to the CStarAlgebra namespace which would avoid this.

[Kevin Buzzard]

My memory was that the only objection raised to this when we had a discussion about it a few years ago was "what if we want the inverse of a noninvertible matrix to be a best approximation to an inverse" but it looks like that we've decided not to do that. You raise the issue of inversion on Nat and Int and my take on this is that (a) your proposal gives the correct answer on those types and (b) in the past I've been surprised that Inv is not defined for Nat and Int. Is there anyone who is objecting to this idea? It sounds pretty natural to me given our current conventions.

[Aaron Liu]

Jireh Loreaux said:

One question is: would the community be okay if we just added an Inv field to MonoidWithZero?

What sort of conditions are you suggesting to put on the Inv in this case? I'm worried that it won't be satisfied by docs#Prod.instInv for docs#Prod.instMonoidWithZero.

[Jireh Loreaux]

oof, Aaron is correct, it is indeed not satisfied there. (Aaron, to explicitly answer your question: the same condition as LawfulInv mentioned in the post)

[Kevin Buzzard]

That example would then just be an awful Inv rather than a lawful Inv.

[Jireh Loreaux]

same for docs#Pi.instInv, unsurprisingly.

[Kevin Buzzard]

Lawful Inv is like some kind of connectivity statement. One would not expect it to be always true.

[Kevin Buzzard]

Looks like $\R\times\R$ will already have an unlawful Inv in mathlib

[Jireh Loreaux]

Sure, but if we add an Inv with arbitrary behavior on MonoidWithZero, then we break extensionality.

[Kevin Buzzard]

Yeah, maybe the lawful approach is the best one. How come you're not seeing this phenomenon in C^* algebras? Is $\mathbb{C}^2$ a C^* algebra? What Inv do you want it to have? One which is not the one it has right now?

[Jireh Loreaux]

@Frédéric Dupuis this actually throws a wrench in your LawfulInv for CStarAlgebra plan anyway, because you wouldn't be able to provide the instance:

instance {ι : Type*} {A : ι → Type*} [Fintype ι] [∀ i, CStarAlgebra (A i)] : CStarAlgebra (Π i, A i)

[Jireh Loreaux]

Kevin, we just want to provide a junk value of 0 for non-invertible elements, that's all.

[Kevin Buzzard]

Right but surely we already have a definition of Inv on $\mathbb{C}^2$ and it doesn't satisfy this?

[Jireh Loreaux]

Right, that was Aaron's point.

[Kevin Buzzard]

docs#Ring.inverse

[Kevin Buzzard]

This is already defined for monoids with zero and presumably the reason it's there as well as Inv is precisely Aaron's observation. So why not just use inverse?

[Jireh Loreaux]

This is what I've just suggested on the PR.

[Jireh Loreaux]

I think the reason he wanted to avoid Ring.inverse is that there is currently rather limited API for it, and obviously it doesn't currently have any notation. I suggested adding some scoped notation and expanding the API.

[Kevin Buzzard]

Wasn't there some weird 1/ notation for it at some point? Or was that something else?

[Jireh Loreaux]

That's for docs#Invertible (which is data carrying).

[Frédéric Dupuis]

Indeed this is a problem! I wonder how far we could get with only the condition that the inverse behaves well on invertible elements, i.e. imposing no particular condition on noninvertible ones.

[Eric Wieser]

Jireh Loreaux said:

I think the reason he wanted to avoid Ring.inverse is that there is currently rather limited API for it, and obviously it doesn't currently have any notation. I suggested adding some scoped notation and expanding the API.

A smaller disadvantage is that it's noncomputable. It's currently quite silly that we can't #eval matrix inverses

[Jireh Loreaux]

Frédéric Dupuis said:

Indeed this is a problem! I wonder how far we could get with only the condition that the inverse behaves well on invertible elements, i.e. imposing no particular condition on noninvertible ones.

That breaks extensionality.

[Frédéric Dupuis]

What do you mean? Suppose we go with

class LawfulInv (M₀ : Type*) [MonoidWithZero M₀] [Inv M₀] where
  inv_unit (u : M₀ˣ) : (u : M₀)⁻¹ = (u⁻¹ : M₀ˣ)

(i.e. removing the condition that the inverse of noninvertible elements is zero.) We would have fewer lemmas that apply generically to LawfulInv, but I'm not sure what would break.

[Jireh Loreaux]

Ah, you're not making MonoidWithZero extend Inv, which is what I was talking about. If you did that, then you would lose extensionality for MonoidWithZero.

[Jireh Loreaux]

I still think what you want is to develop API for Ring.inverse.

[Violeta Hernández]

What's the problem with LawfulInv? It seems to me like a smart idea if we want to reduce theorem duplication.

[Eric Wieser]

I think this message about the motivating instance not working is the problem?

[Violeta Hernández]

Ah, I see.

[Frédéric Dupuis]

Jireh Loreaux said:

I still think what you want is to develop API for Ring.inverse.

If we go down that route, do you have any suggestions for the notation? Maybe something like x⁻¹ʳ?

[Jireh Loreaux]

If that parses correctly, That's reasonable.

[Artie Khovanov]

Is the reason we cannot use x⁻¹ that this clashes with the field notation? Is there no way to overload?

[Frédéric Dupuis]

Yes, even if we could somehow overload the notation, it would be very confusing.

[Eric Wieser]

Jireh Loreaux said:

Frédéric Dupuis this actually throws a wrench in your LawfulInv for CStarAlgebra plan anyway, because you wouldn't be able to provide the instance:

instance {ι : Type*} {A : ι → Type*} [Fintype ι] [∀ i, CStarAlgebra (A i)] : CStarAlgebra (Π i, A i)

I don't quite follow the conclusion here; does this actually mean that LawfulInv is useless? It seems like it might still be a nice way to replace Ring.inverse.

[Eric Wieser]

(what the conclusion does seem to be is that Ring.inverse would be exactly as useful for CStarAlgebra as the proposed LawfulInv would be)

[Frédéric Dupuis]

The issue is that if we consider A × B where A and B are both C*-algebras with an inverse, the Inv that we get on A × B is different from Ring.inverse.

[Frédéric Dupuis]

So either we just work with Ring.inverse, or else we change the definition of LawfulInv as above to leave the junk value on non-invertible elements unspecified.

[Eric Wieser]

Ah ok, it's that docs#Prod.instInv (which I assume is the inverse you want for C* algebras) doesn't satisfy LawfulInv in any reasonable setting

[Kevin Buzzard]

I think it's the inverse they're stuck with rather than the one they were hoping to have!

[Frédéric Dupuis]

If we go with the x⁻¹ʳ notation, here's what it looks like: #34396

[Jireh Loreaux]

We should add a note to the docstring about why Ring.inverse can't become axiomatized into the definition of MonoidWithZero.

[Frédéric Dupuis]

Also, should we scope that notation? I think it's exotic enough not to step on any toes if we leave it global, but scoping is definitely an option.

[Eric Wieser]

Kevin Buzzard said:

I think it's the inverse they're stuck with rather than the one they were hoping to have!

So to be clear, we have docs#Prod.instInv with (x,0)⁻¹ = (x⁻¹, 0), while Ring.inverse (x,0) = 0.@Frédéric Dupuis, do you actually care which of these junk values are used for C-star algebras? If you don't, perhaps we should pursue LawfulInv as a partial characterization, which means we can still keep it as an instance for Prod

[Jireh Loreaux]

I'm not sure how useful LawfulInv would be without the specification on nonunits, which would mean that it wouldn't apply to docs#Prod.instInv anyway. In any case, I believe its clear that it would be hard / impossible to add Inv (in any flavor) to the extends list for CStarAlgebra, and even if someone wanted to, I would push back pretty hard at this point.

[Eric Wieser]

Why do we care how the inverse behaves on non-units?

[Jireh Loreaux]

convenience

[Jireh Loreaux]

I'm not declaring LawfulInv to be totally useless without the nonunits specification, but only that it has more limited value.

[Jireh Loreaux]

Frédéric Dupuis said:

Also, should we scope that notation? I think it's exotic enough not to step on any toes if we leave it global, but scoping is definitely an option.

In general I'm in favor of scoping anything that isn't both completely standard and very common. For perspective, we even scope 𝓝 and 𝓟 to Topology and Filter.

Probably no one else wants ⁻¹ʳ to mean anything, but I think we can be good stewards by scoping it. The biggest price we pay for now is that it still shows up as Ring.inverse in the docs, which is annoying. But that's really a docgen / Lean issue that needs sorting out.