Noether normalisation and residue fields of overconvergent algebras

A nonzero algebra finite over a finite-variable Monsky–Washnitzer algebra admits a finite injective algebra map from another Monsky–Washnitzer algebra, with no more variables. In particular this applies to every nonzero quotient of an overconvergent algebra, retaining nilpotents. The residue fields of such an algebra at its maximal ideals are finite over the coefficient field, as are its quotients by ideals with maximal radical. No characteristic or nontrivial valuation assumption is needed.

A distinguished relation in the kernel lets one remove a variable while retaining finiteness. Together with the distinguishing automorphisms, this gives an induction on the number of variables. This is the algebraic normalisation used to study residue fields and morphisms of dagger algebras.

Main results

• TauCeti.Dagger.washnitzerAlgebra.exists_finite_injective: Noether normalisation. A nonzero algebra finite over the Monsky–Washnitzer algebra K⟨X⟩† in finitely many variables X is finite over an injectively embedded K⟨Y_1, …, Y_n⟩† with n at most the number of variables X.
• TauCeti.Dagger.washnitzerAlgebra.finite_of_isField: a field finite over such a K⟨X⟩† is finite-dimensional over K.
• TauCeti.Dagger.washnitzerAlgebra.finite_quotient_of_isMaximal: an algebra finite over such a K⟨X⟩† has residue fields at its maximal ideals finite-dimensional over K.
• TauCeti.Dagger.washnitzerAlgebra.finite_quotient_of_isMaximal_radical: its quotients by ideals with maximal radical are finite-dimensional over K.
• TauCeti.Dagger.washnitzerAlgebra.finite_quotient_pow: in particular, the quotients of K⟨X⟩† by the powers of a maximal ideal are finite-dimensional over K.
• TauCeti.Dagger.IsDaggerAlgebra.finite_quotient_of_isMaximal, TauCeti.Dagger.IsDaggerAlgebra.finite_quotient_of_isMaximal_radical and TauCeti.Dagger.IsDaggerAlgebra.finite_quotient_pow_of_isMaximal_radical: the same finiteness for dagger algebras, which are finite over a Monsky–Washnitzer algebra through a presentation.

References

• E. Grosse-Klönne, Rigid analytic spaces with overconvergent structure sheaf, J. reine angew. Math. 519 (2000), §1.3(iii), §1.4(2)–(3).
• Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §6.1.2.

The induction adapts TauCeti.IsAffinoidAlgebra.exists_finite_injective in TauCeti.RingTheory.Affinoid.NoetherNormalization. Here division and changes of variables are performed in the overconvergent algebra itself, without passing to its completion.

theorem TauCeti.Dagger.washnitzerAlgebra.exists_finite_injective {K : Type u} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {σ : Type v} [Finite σ] {A : Type w} [CommRing A] [Algebra K A] [Nontrivial A] {π : ↥(washnitzerAlgebra σ K) →ₐ[K] A} (hπ : π.Finite) : ∃ (n : ℕ) (g : ↥(washnitzerAlgebra (Fin n) K) →ₐ[K] A), n ≤ Nat.card σ ∧ Function.Injective ⇑g ∧ g.Finite

Noether normalisation. If a nonzero K-algebra is finite over a Monsky–Washnitzer algebra in finitely many variables, it is finite over an injectively embedded Monsky–Washnitzer algebra with no more variables. In particular a surjective presentation suffices, by AlgHom.Finite.of_surjective. Finiteness uses the algebra structure induced by the displayed map.

theorem TauCeti.Dagger.washnitzerAlgebra.finite_of_isField {K : Type u} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {σ : Type u_1} [Finite σ] {A : Type u_2} [CommRing A] [Algebra K A] {π : ↥(washnitzerAlgebra σ K) →ₐ[K] A} (hπ : π.Finite) (hA : IsField A) : Module.Finite K A

A field finite over a finite-variable Monsky–Washnitzer algebra is finite-dimensional over the coefficient field K. The field is given as a commutative ring A with IsField A.

theorem TauCeti.Dagger.washnitzerAlgebra.finite_quotient_of_isMaximal {K : Type u} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {σ : Type u_1} [Finite σ] {A : Type u_2} [CommRing A] [Algebra K A] {π : ↥(washnitzerAlgebra σ K) →ₐ[K] A} (hπ : π.Finite) (m : Ideal A) [m.IsMaximal] : Module.Finite K (A ⧸ m)

Finiteness of residue fields. Every maximal-ideal quotient of an algebra finite over a finite-variable Monsky–Washnitzer algebra is finite-dimensional over the coefficient field.

theorem TauCeti.Dagger.washnitzerAlgebra.finite_quotient_of_isMaximal_radical {K : Type u} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {σ : Type u_1} [Finite σ] {A : Type u_2} [CommRing A] [Algebra K A] {π : ↥(washnitzerAlgebra σ K) →ₐ[K] A} (hπ : π.Finite) (q : Ideal A) [q.radical.IsMaximal] : Module.Finite K (A ⧸ q)

If A is finite over a finite-variable Monsky–Washnitzer algebra and the radical of q is maximal, then A ⧸ q is finite-dimensional over the coefficient field K. This covers the nilpotent thickenings A ⧸ m ^ n of a residue field, for m maximal and 0 < n. Such an ideal q is automatically primary, by Ideal.isPrimary_of_isMaximal_radical.

theorem TauCeti.Dagger.washnitzerAlgebra.finite_quotient_pow {K : Type u} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {σ : Type u_1} [Finite σ] (m : Ideal ↥(washnitzerAlgebra σ K)) [m.IsMaximal] (k : ℕ) : Module.Finite K (↥(washnitzerAlgebra σ K) ⧸ m ^ k)

The quotients of a finite-variable Monsky–Washnitzer algebra by all powers of a maximal ideal are finite-dimensional over the coefficient field, including the zero quotient for exponent zero.

theorem TauCeti.Dagger.IsDaggerAlgebra.finite_quotient_of_isMaximal (K : Type u) [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_1} [CommRing A] [Algebra K A] [IsDaggerAlgebra K A] (m : Ideal A) [m.IsMaximal] : Module.Finite K (A ⧸ m)

Residue fields of dagger algebras are finite. Every maximal-ideal quotient of a K-dagger algebra is finite-dimensional over K.

theorem TauCeti.Dagger.IsDaggerAlgebra.finite_quotient_of_isMaximal_radical (K : Type u) [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_1} [CommRing A] [Algebra K A] [IsDaggerAlgebra K A] (q : Ideal A) [q.radical.IsMaximal] : Module.Finite K (A ⧸ q)

If the radical of an ideal q of a K-dagger algebra A is maximal, then A ⧸ q is finite-dimensional over K.

theorem TauCeti.Dagger.IsDaggerAlgebra.finite_quotient_pow_of_isMaximal_radical (K : Type u) [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_1} [CommRing A] [Algebra K A] [IsDaggerAlgebra K A] (q : Ideal A) [q.radical.IsMaximal] (n : ℕ) : Module.Finite K (A ⧸ q ^ n)

The quotients of a K-dagger algebra by all powers of an ideal with maximal radical are finite-dimensional over K, including the zero quotient for exponent zero.