restrict linear equiv to submodules

Stream: Is there code for X?

[Johan Commelin]

Suppose that I have a linear equiv e between two vector spaces V₁ ≅ V₂.
And suppose that I have subspace W₁ : submodule K V₁ and W₂ : submodule K V₂.
And suppose that I can show that W₁ maps precisely to W₂ under e.
How do I get a linear equiv W₁ ≅ W₂?

[Eric Wieser]

Do we have docs#submodule.map_equiv?

[Adam Topaz]

docs#submodule.equiv_map_of_injective seems useful.

[Filippo A. E. Nuccio]

Not directly related: I just needed the same for order equiv rather than linear equiv and came up with

lemma order_iso.restrict {α β : Type} [linear_order α] [preorder β] (e : α ≃o β) (s : set α) :
  s ≃o e '' s := strict_mono_on.order_iso e.1 s (λ _ _ _ _ h, (order_iso.strict_mono e) h)

[Eric Wieser]

docs#linear_equiv.of_submodules

[Filippo A. E. Nuccio]

If you replace the strict_mono to injective, can't you adapt this?

[Eric Wieser]

The naming is all over the place; docs#linear_equiv.of_submodule is analogous to docs#mul_equiv.submonoid_equiv_map but the name doesn't suggest it

[Johan Commelin]

@Eric Wieser Thanks a lot. Exactly what I needed.

[Eric Wieser]

I think we might be missing the add_subgroup version