PR #15949: feat(ring_theory/finiteness): A morphism is fi...

Stream: triage

[Random Issue Bot]

Today I chose PR 15949 for discussion!

feat(ring_theory/finiteness): A morphism is finitely presented if the composition with a finite morphism is.
Created by @Andrew Yang (@erdOne) on 2022-08-09
Labels: awaiting-author, delegated, t-algebra

Is this PR still relevant? Any recent updates? Anyone making progress?

[Andrew Yang]

Although it is already delegated, I quite dislike the proof I have now and I will hopefully come back to it later.

[Ruben Van de Velde]

Is it worth landing now in case people want to build on it and postponing the proof improvements until you have time?

[Andrew Yang]

If anyone needs the result now I could get it merged now. I think I (and probably Junyan?) might be the only ones currently building on top of it now but I am more than happy to be proven wrong.

[Bryan Gin-ge Chen]

If you're confident the statement is the right one, I'd suggest going ahead and merging it (possibly with a TODO for improving the proof). In any case, if you don't decide to merge it now, I recommend posting a comment on the PR with your thoughts on the current status, to help anyone who happens to stumble on the PR in the future.