feat(ring_theory/finiteness): A morphism is finitely presented if the composition with a finite morphism is.

[erdOne]

---

[erdOne]

@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 look as well.

[jcommelin]

bors d+

[bors[bot]]

:v: 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.

[alreadydone]

I can't quite fit it into the lemmas I introduced for the case of fp modules, but I was able to golf down the proof a bit using quotient ring and double algebra.adjoin_induction.

~~One way to make use of my lemmas would be to show that the span of {1} ∪ s over RX is the same as the span of {1} ∪ s over AX (which is the whole AX),~~ (Correction: this isn't quite right, we need to consider RX{1} + AX(g''t), see below.) but we don't have the algebra RX AX and scalar tower instances for the mv_polynomial rings; I tried to manually introduce them by e.g. (mv_polynomial.map $ algebra_map R A).to_algebra but it makes things slow.

[alreadydone]

Update: I'm now able to adapt the proof to make use of my lemmas, but unfortunately the proof becomes longer; I also need an additional lemma that says AX is spanned by RX as an A-module. The approach is to define the R-submodule N := I₀ ⊔ RX of AX and show it's an A-submodule, so by the new lemma it's the whole of AX. To write down N as a R-submodule I have to use the lengthy expression

N := I₀.restrict_scalars R ⊔ 
    ((⊤ : ideal RX).restrict_scalars R).map (map_alg_hom $ algebra.of_id R A).to_linear_map

I think it's unlikely that we can get a proof shorter than the previous one.

[erdOne]

bors merge

[bors[bot]]

Build failed:

• Lint mathlib

[erdOne]

bors merge

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests