Splitting lemma for modules

Stream: Is there code for X?

[Pierre-Alexandre Bazin]

If I have a [module R M] and A : submodule R M and a splitting (f : (M ⧸ A) →ₗ[R] M) (h : ∀ x, submodule.quotient.mk (f x) = x), we can get a linear equiv A × (M ⧸ A) ≃ₗ[R] M.

• Do we have this (or anything similar) in Lean ?

• If not, should it be stated as I said above or with a more general short exact sequence (that is, two R-modules A and B with (j : A →ₗ[R] M) (g : M →ₗ[R] B) (hj : function.injective j) (exac : j.range = g.ker) (f : B →ₗ[R] M) (h : g.comp f = linear_map.id) ?

• And should we derive it from a more general category theory lemma or not ?

[Pierre-Alexandre Bazin]

(actually, in my use case I'd rather have the second version with A and B)

[Johan Commelin]

In LTE we have a bunch of API for split exact sequences. But you would need a bit of glue to use it for unbundled modules.

[Johan Commelin]

https://github.com/leanprover-community/lean-liquid/blob/a6e2d9568b65df034a44098ba389f06e988afc47/src/for_mathlib/split_exact.lean

[Eric Wieser]

I feel like I've seen an equiv pretty similar to this, maybe for additive groups

[Kevin Buzzard]

Yes it's one of those things which will work in a large number of abelian situations (and perhaps even some nonabelian ones)

[Eric Wieser]

Sure; my point is that I think if we look for one of those variants we'll find it it mathlib