Tensor product and exact sequences

Stream: maths

[Andrew Yang]

Say we have two exact sequence of $R$-modules: $0 \to A \to B \to C \to 0$ and $0 \to A' \to B' \to C \to 0$ with $B$ flat. If $A \otimes D \to B \otimes D$ is injective, how can I show that $A' \otimes D \to B' \otimes D$ is also injective? This is trivial by showing $\operatorname{Tor}_1(C, D) = 0$ but is there a more mathlib-friendly proof?

[Brendan Seamas Murphy]

You can prove it by taking a flat resolution $P \to Q \to D \to 0$. First apply the snake lemma to part of the diagram you get by tensoring this resolution and $0 \to A \to B \to C \to 0$ and you'll find that $C \otimes P \to C \otimes Q$ is injective. Then this allows you to apply to the snake lemma to part of the diagram you get by tensoring the resolution with $0 \to A' \to B' \to C \to 0$, and this implies that $A' \otimes D \to B' \otimes D$ is a kernel of $B' \otimes D \to C \otimes D$ (hence injective). I think this is what you would get by unraveling the Tor proof.

Here are some pictures with the subdiagrams you'd want to apply the :snake: lemma too highlighted in orange 257c32c9-4d5c-42c3-bb76-04b0e73b89e6.png

4d8ca4fd-2d44-4516-94e1-0078c60a5cdd.png

[Brendan Seamas Murphy]

Can't say this is especially "mathlib-friendly" though

[Brendan Seamas Murphy]

Oops, I swapped the order in the tensor product without noticing when drawing the diagrams. I'll leave fixing that to the reader

[Andrew Yang]

Thanks a lot! Now let me try to make this work in mathlib...

[Brendan Seamas Murphy]

What I wrote above isn't right. You need to take an exact sequence $0 \to P \to Q \to D \to 0$ (and we can't assume $P$ is flat here). Without this injectivity of $C \otimes P \to C \otimes Q$ is hopeless. The proof still works but the top left zero in each diagram shouldn't be there (bc tensoring with $P$ isn't left exact)

[Brendan Seamas Murphy]

This makes the second part of the argument even more annoying, bc you need to argue that the image of $A' \otimes P \to A' \otimes Q$ is the same as the image of $\ker(B' \otimes P \to C \otimes P) \to A' \otimes Q$, but I think it's fine in the end