Hom-tensor adjunction?

Stream: Is there code for X?

[Matej Penciak]

Do we have the tensor-hom adjunction for modules over commutative rings? (is this just currying the definition?)

Really all I want is that tensoring is right exact, so if there's some slick way of deriving that from what's already known I'd be happy with that too.

[Adam Topaz]

How do you want to phrase "right exact"ness?

[Adam Topaz]

If you're just looking for the surjectivity claim, then the easiest approachh would be to use docs#tensor_product.induction_on (if the statement is not already in mathlib)

[Matej Penciak]

I have a proof of the surjective part. Indeed the induction_on made it a breeze. But exactness in the middle (which I'm stating as (ltensor N f).range = (ltensor N g).ker) turns out to be a slog to do by hand...

[Matej Penciak]

Where f : M →ₗ[R] M' and g : M' →ₗ[R] M'' are the maps of the exact sequence.

[Adam Topaz]

I see. Well, the "tensor hom adjunction" is essentially this docs#tensor_product.lift.equiv

[Adam Topaz]

I don't know if we have it in mathlib in terms of a categorical statement involving docs#category_theory.adjunction

[Adam Topaz]

Scratch that, we do have docs#Module.category_theory.monoidal_closed

[Matej Penciak]

Oh right, I remember Scott Morrison mentioned that in another thread a while back but I forgot about it. Thanks!

[Johan Commelin]

What we are missing (afaik) is a good bit of glue between (right/left) exact functors and docs#category_theory.exact