Quotient of module by sum of ideals

Stream: Is there code for X?

[Brendan Seamas Murphy]

Is the isomorphism $\frac{M}{(I + J)M} \cong \frac{M/IM}{J(M/IM)}$ in mathlib?

[Adam Topaz]

possibly, but it probably depends on how you want to formulate it.

[Dean Young]

R/(I+J) ≅ R/I ⊗R/J, then tensor with M.

[Adam Topaz]

Well sort of. The spelling I have in mind is “base change along A/I then along the quotient induced by J is the same as base change along A/(I+J)

[Adam Topaz]

Yeah essentially that. With the rings!

[Adam Topaz]

(Sorry, I’m typing on the phone so a bit slow)

[Adam Topaz]

But in this case there’s a canonical map in both directions, so it might be worth while to have the more explicit iso as well to have good definitional properties if needed.

[Brendan Seamas Murphy]

I do know how to prove the statement, and have done so in my code (using the isomorphism theorems, not tensor products), I was just wondering whether this exact iso was defined yet

[Dean Young]

@Brendan Seamas Murphy my bad Brandan. Jiazhen & Coriver are still eager to meet you by the way

[Antoine Chambert-Loir]

It is probably easier to observe that the composition map $M \to M/I \to (M/I)/J\cdot(M/I)$ is surjective and its kernel is $(I+J)\cdot M$.