Zulip Chat Archive

Stream: Is there code for X?

Topic: A linear space injects into its dual space

Martin Winter (Oct 09 2025 at 14:33):

Is there a theorem that states that "there is an injection from a module into its dual space" (under suitable assumptions that make this true, for example if it is a vector space).

Something like Basis.linearEquiv_dual_iff_finiteDimensional which proves Nonempty (V ≃ₗ[K] Module.Dual K V) ↔ FiniteDimensional K V, but for injections and without the finiteness assumption.

Etienne Marion (Oct 09 2025 at 14:43):

Maybe this? https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Dual/Basis.html#Module.Basis.toDual_injective

Martin Winter (Oct 09 2025 at 15:10):

Certainly useful. But I was hoping to not first get a basis. I guess I can write my own using this (if there is none after all). Is there something like LinearEmbed or so, that is, a purely injective equivalent of LinearEquiv?

Kenny Lau (Oct 09 2025 at 15:13):

how do you plan to do it without a basis

Kevin Buzzard (Oct 09 2025 at 15:14):

Without a basis, how are you defining a map? For modules without a basis e.g. R/I as an R-module, it's unlikely that there will be an injection into the dual (Hom_R(R/I,R) is often going to be 0). You can temporarily pick a basis, get an injection and then forget the basis and just prove that there exists an injection; will that do?

Etienne Marion (Oct 09 2025 at 15:20):

Kevin Buzzard said:

You can temporarily pick a basis, get an injection and then forget the basis and just prove that there exists an injection; will that do?

I think this is what he meant with "I guess I can write my own using this"?

Etienne Marion (Oct 09 2025 at 15:21):

Martin Winter said:

Certainly useful. But I was hoping to not first get a basis. I guess I can write my own using this (if there is none after all). Is there something like LinearEmbed or so, that is, a purely injective equivalent of LinearEquiv?

I don’t think there is such, you would have to use docs#Function.Injective.

Jireh Loreaux (Oct 09 2025 at 15:23):

There's a natural map into the double dual. Is that what you're remembering?

Martin Winter (Oct 09 2025 at 16:00):

Kevin Buzzard said:

You can temporarily pick a basis, get an injection and then forget the basis and just prove that there exists an injection; will that do?

This is what I meant. I don't care about using a basis in the proof. But I want a theorem that does this for me.

Jireh Loreaux said:

There's a natural map into the double dual. Is that what you're remembering?

No, I definitely want an injection into the single-dual (if there is one). Since there is no canonical one, I want at least the statement that one exists.

Kenny Lau (Oct 09 2025 at 16:10):

@Martin Winter you can use loogle to help you find theorems, in this case my input was "exists", "basis", and the first result was the correct one: Module.Free.exists_basis

Martin Winter (Oct 09 2025 at 16:14):

I am aware of Loogle and I know how to gete a basis. Sorry if my question was unclear or I used the wrong channel. I know exactly how to prove the result. But I wanted to know whether something like it is already there and what would be the best way to state it. Thanks for the quick responses!