## Stream: maths

### Topic: Linear embeddings

#### Oliver Nash (May 12 2020 at 19:22):

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 (May 12 2020 at 19:23):

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 (May 12 2020 at 19:24):

(modulo tidy up / naming etc. ofc)

#### Yury G. Kudryashov (May 12 2020 at 19:57):

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

#### Oliver Nash (May 12 2020 at 19:58):

\hookrightarrow with the little l subscript.

#### Oliver Nash (May 12 2020 at 19:58):

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

Lgtm.

#### Oliver Nash (May 12 2020 at 19:59):

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

#### Oliver Nash (May 12 2020 at 21:58):

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

#### Johan Commelin (May 13 2020 at 03:02):

@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 (May 13 2020 at 05:38):

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

#### Oliver Nash (May 13 2020 at 07:45):

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 (May 13 2020 at 07:49):

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 (May 13 2020 at 07:49):

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 (May 13 2020 at 08:10):

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

#### Oliver Nash (May 13 2020 at 08:16):

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 (May 13 2020 at 08:17):

Anyway, I better get back to the day job.

#### Eric Wieser (Jul 28 2020 at 19:45):

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)


Last updated: May 19 2021 at 02:10 UTC