direct sums of submodules

Stream: Is there code for X?

[Scott Morrison]

I would like to merely state the result:

Let M be a noetherian module over R, and suppose K and L are submodules of M such that K ≅ M ⊕ L. Then L = ⊥.

How do I talk about the direct sum of two submodules?

example (R M : Type) [ring R] [add_comm_group M] [module R M] [is_noetherian R M]
  (K L : submodule R M) (i : sorry) : L = ⊥ := sorry

[Scott Morrison]

I don't particularly mind if we treat L just as another R module, rather than a submodule.

[Kevin Buzzard]

Does the abstract product get a module structure?

[Kevin Buzzard]

I mean prod

[Scott Morrison]

Ah, okay!

example (R M : Type) [ring R] [add_comm_group M] [module R M] [is_noetherian R M]
  (K L : submodule R M) (i : K ≃ₗ[R] (M × L)) : L = ⊥ := sorry

typechecks at least. I'll see if I can prove it.

[Kevin Buzzard]

I don't even know a maths proof

[Scott Morrison]

There's a copy of K inside M. But since K ≃ₗ[R] (M × L), there an even smaller copy of K inside that, with a copy of L to spare. Repeat this over and over again, obtaining more and more copies of L. The successive direct sums of these form an ascending chain, so it stabilizes, which is only possible if L = ⊥.

[Eric Wieser]

Can you get here by showing the docs#module.rank of the prod of two modules is the sum of their ranks? So rank K = rank M + rank L, but K is a submodule of M so rank K ≤ rank M and rank L = 0

[David Wärn]

I think it's true more generally that if a submodule K of M surjects onto M via f, then f is an isomorphism. The proof is the same: let X 0 be the zero submodule of K, and recursively let X (i+1) be the preimage of X i under f. Then this must stabilise which is only possible if f has zero kernel

[David Wärn]

I don't think ranks will help you since L having zero rank does not mean L is zero, but it does provide the right intuition

[Eric Wieser]

You're right, docs#dim_zero_iff requires a field

[Eric Wieser]

Also we now have lots of lemmas about dim that didn't get renamed when rank did...

[Kevin Buzzard]

Yes, for general rings there is no good notion of rank. For integral domains you can tensor up to the field of factions and ask for the dimension, so then the rank of Z^n is Z but the rank of every finite abelian group and more generally every torsion abelian group will be 0

[Scott Morrison]

David Wärn said:

I think it's true more generally that if a submodule K of M surjects onto M via f, then f is an isomorphism. The proof is the same: let X 0 be the zero submodule of K, and recursively let X (i+1) be the preimage of X i under f. Then this must stabilise which is only possible if f has zero kernel

@David Wärn, could you explain this in more detail? I don't understand any of it. :-) Why are the X i increasing?

[Scott Morrison]

I actually just yesterday proved that a surjective endomorphism (of a noetherian module) is injective, by looking at (f ^ n).ker. In fact I think this argument goes through unchanged if f : K \to M, (i.e. a surjective map out of a submodule) rather than an endomorphism.

[Scott Morrison]

And... I'm an idiot. This is exactly what you said :-)