Inverse of a linear map ?

Stream: Is there code for X?

[Sophie Morel]

For functions between types, we have Function.invFun that produces a candidate inverse function (if the codomain of the function is nonempty) which is an actual inverse if the function is bijective. Is there a similar definition for linear maps ? I'm over a division ring, and my spaces are finite-dimensional, so choice wouldn't even be needed, but if there's a general solution using choice I'll take it too.
I think I can code what I want myself, but I'd rather not duplicate code if it already exists.

[Sophie Morel]

(I am aware of LinearPMap.inverse, but I really want a LinearMap defined on the whole space.)

[Eric Wieser]

If your map is an endomorphism you can use docs#Ring.inverse

[Sophie Morel]

It's not an endomorphism unfortunately.

[Sophie Morel]

(My first impulse was to write f⁻¹, which doesn't seem to exist.)

[Anatole Dedecker]

Do you actually know that your function is bijective? Or do you want junk values in cas it isn't?

[Anatole Dedecker]

If it's bijective the simplest would be to use docs#LinearEquiv.ofBijective and apply .symm to it.

[Antoine Chambert-Loir]

Given a function on a nonempty domain, it is easy to construct a function which is a right inverse iff your function is surjective, and is an inverse iff your function is bijective. Just map any element to some preimage if it has some, and to a dummy value otherwise.
But that's definitely not enough to define a linear map.
For vector spaces, something is possible, by taking complements, but there's no hope otherwise…

[Anatole Dedecker]

Yes we can't be as smart as invFun (since there's no hope of constructing a left/right inverse from injectivity/surjectivity), but maybe it's still useful from a UX point of view to have a "inverse" which is zero whenever there's no reasonable inverse.

[Sophie Morel]

Anatole Dedecker said:

Do you actually know that your function is bijective? Or do you want junk values in cas it isn't?

It's not always bijective. I want it to behave like Function.invFun, i.e. to give a preimage when such a preimage exists and a junk value otherwise. I'm using this to construct a LocalEquiv, which must be defined everywhere but only needs to take sensible values on its source.

[Sophie Morel]

Antoine Chambert-Loir said:

Given a function on a nonempty domain, it is easy to construct a function which is a right inverse iff your function is surjective, and is an inverse iff your function is bijective. Just map any element to some preimage if it has some, and to a dummy value otherwise.
But that's definitely not enough to define a linear map.
For vector spaces, something is possible, by taking complements, but there's no hope otherwise…

I need the "inverse" to be a linear map. I am over a division ring, so what I want is definitely possible ! The questions are: (1) does it already exist ? (2) is this the best way to proceed ? (Question (2) is for me to answer, I guess.)

[Sophie Morel]

The situation is the following: I am trying to defined charts for the Grassmannian of r-dimensional subspaces of a K-vector space E. The model space is (Fin r → K) →ₗ[K] E. These charts will be indexed by isomorphisms φ : E ≃ₗ[K] U × (Fin r → K), where U is a fixed K-vector space. The set where the chart indexed by φ makes sense is the set of subspaces W such that φ.snd.domRestrict W is an isomorphism, and the chart sends such a W to φ.fst ∘ (Submodule.subtype W) ∘ (φ.snd.domRestrict W)⁻¹, which is in (Fin r → K) →ₗ[K] E as desired. But I want the chart to be defined everywhere for Lean reasons, so it would be nice if the formula made sense for every W. (Barring that, I can of course define the chart by sending all "bad" W's to 0.)

[Eric Wieser]

Are you looking for the linear map analogue to the moore-penrose pseudoinverse?

[Sophie Morel]

Eric Wieser said:

Are you looking for the linear map analogue to the moore-penrose pseudoinverse?

Not really, because my maps are not endomorphisms and I don't care about "best fits". I was really just looking for a way to extend the inverse function maps from V ≃ₗ[K] W to V →ₗ[K] W, which seemed like a very "Lean" thing to do.

[Eric Wieser]

The pseudoinverse doesn't need endomorphisms either, but I guess the best fit comment makes sense

[Eric Wieser]

Sophie Morel said:

(I am aware of LinearPMap.inverse, but I really want a LinearMap defined on the whole space.)

You can use docs#LinearMap.exists_extend to go from one to the other

[Sophie Morel]

Ok, I thought it was square matrices. Anyway, I am doing something much less refined. What I am doing so far (in my actual problem) is set the pseudo-inverse at 0 when the linear map is not invertible. We'll see if that causes trouble later.

[Eric Wieser]

I interpreted
Sophie Morel said:

I want it to behave like Function.invFun, i.e. to give a preimage when such a preimage exists and a junk value otherwise.

as saying that you want a partial inverse

[Eric Wieser]

Your latest message is "give a preimage if all such preimages exist"

[Sophie Morel]

I don't understand your message. Your interpretation of my first message is probably correct. My last message says that I'm trying to make do with something weaker, since my final goal is not pseudo-inverses but charts for the grassmannian (I explained that in a previous message in this thread).

[Sophie Morel]

As I am not done proving all the properties of the charts, I hope that my "something weaker" will suffices but cannot be sure yet.

[Eric Wieser]

I can't make any judgement on whether the weaker condition will work, I'm afraid!

[Sophie Morel]

I'll just keep chugging on and come back if it does not work.

[Sophie Morel]

Update: the kind of thing that I wanted exists, but only for continuous linear maps ! Cf ContinuousLinearMap.inverse. It sends a ContinuousLinearMapto its inverse if it underlies a ContinuousLinearEquiv, and to $0$ otherwise. (Confusingly, LinearMap.inverse does something different.)
Funnily enough, I actually needed that construction for continuous linear maps in the end, so I guess all's well that ends well.