Right exactness of tensor products

Stream: Is there code for X?

[Sophie Morel]

Is the right exactness of tensor products proved somewhere in mathlib ? I am also looking for the statement that, if u : A -> B and v : C -> D are surjective, then Ker(u\otimes v) is the image of (Ker u)\otimes C + A \otimes(Ker v), but the proof of this uses right exactness. Okay, I'm actually working over a field so everybody is flat and my statements simplify, but I checked Module.Flat in mathlib and it was pretty short, so maybe I have a better chance of finding the general statements. :grinning:

[Antoine Chambert-Loir]

I remembered having proved something like that by hand for the very reason you indicate. Unfortunately, the screen of my laptop doesn't light up hence I need to find an external screen to send you a precise link, and you'll certainly have proved the result for you then.

[Sophie Morel]

No, I'm very willing to wait for you to find another screen ! The lemma I was looking for is A, II, p. 59, prop. 6 in Bourbaki, to be precise.

[Antoine Chambert-Loir]

OK, and please send me a note if I forget...

[Adam Topaz]

I think mathlib knows that tensoring is a left adjoint, so it should be straightforward if you want to formulate right exactness as preserving finite colomits.

[Adam Topaz]

https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean

[Adam Topaz]

That closed monoidal structure comes with some universe restrictions, unfortunately.

[Sophie Morel]

Thanks! So now I need to determine the least painful way to get there, between doing stuff by hand or going the categorical route with potential universe trouble. (Probably the least painful way is to wait for Antoine's code. :grinning_face_with_smiling_eyes:)
I recently tried to do a left Kan extension and promptly ran into a horrible universe error, so I'm little wary of categories at the moment...

[Antoine Chambert-Loir]

I think it is important to share and discuss publicly the universe errors, that's an unavoidable question whenever one has to use large quantifiers. In my case, thanks to @Adam Topaz's help, it was enough yo restrict some types to a fixed universe, but this forced me to learn how to lift types.

[Alex J. Best]

Module.Flat is very short indeed, @Jujian Zhang did a lot of things about flatness in https://github.com/jjaassoonn/flat, but its in lean 3 and not yet ported (I started trying to extract the smallest independent piece of what Jujian did but got sidetracked)

[Antoine Chambert-Loir]

Sophie Morel said:

No, I'm very willing to wait for you to find another screen ! The lemma I was looking for is A, II, p. 59, prop. 6 in Bourbaki, to be precise.

Do you need the case of a noncommutative ground ring?

[Antoine Chambert-Loir]

I could see what I had proved: this is what you need in the restricted case where the modules are algebras. My proof does not work as in Bourbaki though, I rather redo the proof of A, II, p. 58, prop.5.

[Antoine Chambert-Loir]

I'll open a new branch to port it (I just have the mathlib3 -> mathport code, it is not yet fully ported to mathlib4), because it also requires to adjust a few things in mathlib's RingTheory.TensorProduct.

[Sophie Morel]

Thanks! I only need the case of a commutative ground ring. (My ground ring is even a commutative field.)

[Sophie Morel]

Alex J. Best said:

Module.Flat is very short indeed, Jujian Zhang did a lot of things about flatness in https://github.com/jjaassoonn/flat, but its in lean 3 and not yet ported (I started trying to extract the smallest independent piece of what Jujian did but got sidetracked)

Interesting, I'll have a look !

[Antoine Chambert-Loir]

See PR #6447 in branch#TensRightExact