Linear embeddings

Stream: maths

[Oliver Nash]

I want to define/prove some stuff about submodules (actually lie_subalgebras ultimately, though this is irrelevant) and it seems to be far more convenient to work with a linear embedding than an actual submodule. So I had a poke around and it seems that there is no definition for linear embeddings. Have I missed something, or would this be a welcome addition to Mathlib?

[Oliver Nash]

The definition / lemmas I have in mind are approximately:

set_option old_structure_cmd true
structure linear_embedding (R : Type u) (M : Type v) (M₂ : Type w)
  [ring R] [add_comm_group M] [add_comm_group M₂] [module R M] [module R M₂]
  extends M →ₗ[R] M₂, M ↪ M₂

notation M ` ↪ₗ[`:25 R:25 `] `:0 M₂:0 := linear_embedding R M M₂

def submodule.embedding (M' : submodule R M) : M' ↪ₗ[R] M := sorry

lemma submodule.embedding_range' (M' : submodule R M) : M'.embedding.to_linear_map.range = M' := sorry

lemma submodule.range_embedding {M' : Type v} [add_comm_group M'] [module R M'] (f : M' ↪ₗ[R] M) :
  ∃ (e : M' ≃ₗ[R] f.to_linear_map.range), f.to_linear_map.range.embedding.to_linear_map.comp e.to_linear_map = f := sorry

[Oliver Nash]

(modulo tidy up / naming etc. ofc)

[Yury G. Kudryashov]

Phone doesn't show the notation. Which symbol do you use?

[Oliver Nash]

\hookrightarrow with the little l subscript.

[Oliver Nash]

The arrow is the same as the one already defined for structureless embedding

[Yury G. Kudryashov]

Lgtm.

[Oliver Nash]

OK thanks, I'll try to put together a PR and see what feedback I get there.

[Oliver Nash]

https://github.com/leanprover-community/mathlib/pull/2668

[Johan Commelin]

@Oliver Nash I completely agree that it is often a lot more useful to work with an embedding than a substructure. Good move!
The downside of your new structure is that you have to reprove lots of basic coercion and simp-lemma stuff. And then again for "ring embeddings" and "group embeddings" and "lie algebra embeddings" etc... An alternative approach to just use a linear map + assumption that it is injective. Have you considered that?

[Yury G. Kudryashov]

I wish we had a tactic that magically exports lemmas about a substructure while adjusting some types and coercions.

[Oliver Nash]

Thanks @Johan Commelin you have answered my implicit question perfectly, and unbundling properties like injectivity / surjectivity certainly seems like a plausible place to draw the line.

[Oliver Nash]

The dream would be @Yury G. Kudryashov 's suggestion of automatically creating these lemmas. I don't see any reason why we couldn't do that. Is there a fundamental obstruction or is this just something that has not been important enough yet?

[Oliver Nash]

Anyway, I should have some time again in a day or so and I'll try to push ahead with morphisms + injectivity assumption instead. In the meantime I'll close that PR.

[Scott Morrison]

I think the bottleneck is availability of tactic writing expertise*hours

[Oliver Nash]

Interesting. I currently have zero seconds experience writing tactics but I'd like to learn about it. Maybe in a few weeks when I get to a natural stopping point with the Lie algebra stuff I've been trying to set up, I'll see if I can at least learn enough about tactic writing to understand how challenging this would be.

[Oliver Nash]

Anyway, I better get back to the day job.

[Eric Wieser]

Is there some way to make something like this compile?

structure embedding_of {f : Sort u} [has_coe_to_fun.{u v} f]:=
(to_fun : f)
(inj'   : function.injective ⇑to_fun)