Finiteness of MvPolynomial.map

MvPolynomial.map f is a finite ring map whenever f is: a family generating S over R generates MvPolynomial σ S over MvPolynomial σ R once its members are read as constants.

This is the coefficient-extension half of the finiteness that Stacks 10.161.13 (tag 032O) records as "R'[x^{1/q}] is finite over R[x]"; the expand half lives in TauCeti/RingTheory/MvPolynomial/Expand.lean. Nothing here mentions expand, which is why it sits in this file rather than that one.

Main results

• TauCeti.MvPolynomial.finite_map: MvPolynomial.map f is finite when f is.

Provenance

Roadmap: EllipticCurves, the Layers 0-1 target Function-field foundations and isogenies (TauCetiRoadmap/EllipticCurves/README.md:1096), through the support module RingTheory/IntegralClosure/NormalizationFinite. The argument is Stacks 10.161.13 (tag 032O), which is univariate and whose proof records it as "Since R is N-2 we see that R′ is finite over R and hence R′[x^{1/q}] is finite over R[x]"; the multivariate form is not claimed as source material.

theorem TauCeti.MvPolynomial.finite_map {σ : Type u_1} {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.Finite) : (MvPolynomial.map f).Finite

Polynomial rings preserve module-finiteness of the coefficient map: MvPolynomial.map f is a finite ring map whenever f is.