[Merged by Bors] - feat(RingTheory/Kaehler): The exact sequence B ⊗[A] Ω[A⁄R] → Ω[B⁄R] → Ω[B⁄A] → 0.

[erdOne]

---

[riccardobrasca]

Do we have enough technology to use CategoryTheory.ShortComplex.ShortExact or something like that? I mean, literally saying the sequence is exact.

[joelriou]

Do we have enough technology to use CategoryTheory.ShortComplex.ShortExact or something like that? I mean, literally saying the sequence is exact.

In general, we cannot use category theory here because of heterogeneous universes. Eventually, it may be useful to state exactness (by saying that a certain cokernel cofork is colimit) when all the modules are in the same universe, but I do not feel it has to be done in this PR. (It would be an application of https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Homology/ShortComplex/ModuleCat.html#CategoryTheory.ShortComplex.moduleCat_exact_iff_range_eq_ker)

Exactness could also be formulated also using the basic API in Mathlib.Algebra.Exact which allow different universes.

[riccardobrasca]

Can you add a short docstring as I wrote above? Anyway thanks a lot!

bors d+

[mathlib-bors]

✌️ erdOne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[erdOne]

Sorry it took so long to fix. I've incorporated some suggestions above and a few more and maybe @riccardobrasca can give it a final look before I send it to bors?

[riccardobrasca]

Sorry it took so long to fix. I've incorporated some suggestions above and a few more and maybe @riccardobrasca can give it a final look before I send it to bors?

I am boarding on a long flight, I can have a look tomorrow.

[riccardobrasca]

It still looks good, thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style