Finiteness of MvPolynomial.expand

The polynomial ring R[X_i] is a finite module over its image under MvPolynomial.expand n (the subring R[X_i ^ n]), spanned by the monomials whose exponents are all below n.

Composed with the finiteness of MvPolynomial.map f — a separate result, proved in TauCeti/RingTheory/MvPolynomial/Basic.lean and not imported here — this gives that k'[X_1, …, X_r] is a finite module over k[X_1 ^ q, …, X_r ^ q] for a finite extension k' / k, the finiteness that Stacks 10.161.13 (tag 032O) records as "R'[x^{1/q}] is finite over R[x]" and that the purely inseparable half of normalization-finiteness rests on.

Also here is the coefficient-level Frobenius computation behind Stacks' "some details omitted": if every coefficient of g acquires a q-th root in S, then g(X ^ q) becomes a q-th power in S[X_i].

Main results

• TauCeti.MvPolynomial.span_monomial_lt_eq_top: over the image of expand n, the monomials with all exponents below n span the polynomial ring.
• TauCeti.MvPolynomial.finite_expand: expand n is a finite ring map for 0 < n.
• TauCeti.MvPolynomial.exists_pow_eq_map_expand: (map f) (expand (p ^ n) g) is a p ^ n-th power once the coefficients of g have p ^ n-th roots in S.

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.

All three results are the multivariate form of the univariate argument in Stacks, Lemma 10.161.13 (tag 032O), whose proof records only "R′[x^{1/q}] is finite over R[x]" for the first two. The third is the coefficient half of the details that lemma omits: "There exists a finite purely inseparable field extension L′/K and q = p^e such that L ⊂ L′(x^{1/q}); some details omitted". Concretely, with h = ∑ d_α X ^ α for d_α ^ (p ^ n) = f (coeff α g), Frobenius gives h ^ (p ^ n) = ∑ f (coeff α g) X ^ (p ^ n • α). The multivariate forms are not claimed as source material.

The argument is the finiteness sentence of Stacks 10.161.13 (tag 032O). That lemma is univariate: it is stated for the rings R[x] and R'[x^{1/q}] in a single variable. What is formalized here is its multivariate form, over a finite variable type σ, which is what the n-variable Noether normalization downstream needs. The mathematical content of each step is Stacks'; the passage to several variables at once is not, and is not claimed as such below.

theorem TauCeti.MvPolynomial.span_monomial_lt_eq_top {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Finite σ] {n : ℕ} (hn : 0 < n) : Submodule.span (↥(MvPolynomial.expand n).range) (Set.range fun (β : σ → Fin n) => (MvPolynomial.monomial (Finsupp.equivFunOnFinite.symm fun (i : σ) => ↑(β i))) 1) = ⊤

Over the image of MvPolynomial.expand n, the finitely many monomials with all exponents below n span the whole polynomial ring.

theorem TauCeti.MvPolynomial.finite_expand {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] {n : ℕ} (hn : 0 < n) : (MvPolynomial.expand n).Finite

MvPolynomial.expand n is a finite ring map for 0 < n: the polynomial ring is spanned over R[X_i ^ n] by the monomials with exponents below n.

theorem TauCeti.MvPolynomial.exists_pow_eq_map_expand {σ : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] (f : R →+* S) (p : ℕ) [ExpChar S p] (n : ℕ) {g : MvPolynomial σ R} (hg : ∀ i ∈ g.support, ∃ (d : S), d ^ p ^ n = f (g.coeff i)) : ∃ (h : MvPolynomial σ S), h ^ p ^ n = (MvPolynomial.map f) ((MvPolynomial.expand (p ^ n)) g)

If every coefficient of g has a p ^ n-th root in S, then g(X ^ (p ^ n)), read in S[X_i], is a p ^ n-th power.