Andrew Yang
Andrew Yang
@nick-kuhn said to me last month that he is working on showing `localization.away` is finitely presented. I'm not sure about his progress.
Is there a reason why [doc#tensor_product.left_module](https://leanprover-community.github.io/mathlib_docs/linear_algebra/tensor_product.html#tensor_product.left_module) is not used?
I meant that we should be able to get an `S`-action on `S ⊗[R] M` for free.
Sorry for the late reply -- I saw your last comment before the edit and there isn't a GitHub notification for comment edits.
Since this file mainly focuses on the diagonal morphism `Δ_{X/Y} ⟶ X`, there was only one lemma that I was able to generalize in terms of kernel pairs.
@alreadydone I also tried to incorporate the new lemmas you proposed on this result, but I couldn't find a way forward. It would be great if you can take a...
@YaelDillies I would like to define heights of primes, Krull dimensions of rings, codimensions of irreducible closed subsets etc. (cf [This Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Length.20of.20longest.20chain)) What is the reason behind the conclusion?...