Noether normalisation of affinoid algebras

Every nonzero affinoid algebra over a complete ultrametric field admits a finite injective algebra map from a Tate algebra. No reducedness, characteristic, or nontrivial valuation assumption is needed.

The argument follows Bosch–Güntzer–Remmert, Non-Archimedean Analysis, §6.1.2. Its distinguished-variable induction adapts the central construction in TauCeti.MvPowerSeries.finite_quotient_of_isMaximal: a nonzero relation becomes distinguished after a change of variables, so Weierstrass division makes the algebra finite over the image of a Tate algebra with one fewer variable. Applying induction to that image retains nilpotents.

The changes of variables are isometries of Gauss norms, so for a presentation π : K⟨X₁, …, Xₙ⟩ → A the normalisation can be chosen of the form π ∘ ι for a Gauss-norm preserving map ι : K⟨Y₁, …, Y_d⟩ → K⟨X₁, …, Xₙ⟩ (AlgHom.exists_norm_eq_finite_injective_comp). In particular it sends the Gauss unit ball into the image under π of the Gauss unit ball (AlgHom.exists_finite_injective_map_unitClosedBall_le). This compatibility relates the supremum seminorm of A to integrality over the presentation ring π(K⟨X₁, …, Xₙ⟩°), and lets coefficients over K⟨Y₁, …, Y_d⟩ be lifted along π without increasing their Gauss norms.

theorem TauCeti.IsAffinoidAlgebra.exists_finite_injective {K : Type u} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_1} [CommRing A] [Algebra K A] [Nontrivial A] (hA : IsAffinoidAlgebra K A) : ∃ (n : ℕ) (g : ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin n) => 1) →ₐ[K] A), Function.Injective ⇑g ∧ g.Finite

Affinoid Noether normalisation. Every nonzero affinoid algebra over a complete ultrametric field is finite over an injectively embedded finite-variable Tate algebra. Finiteness uses the algebra structure induced by the displayed map.

theorem AlgHom.exists_norm_eq_finite_injective_comp {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {σ : Type u_2} [_root_.Finite σ] {A : Type u_3} [CommRing A] [Algebra K A] [Nontrivial A] (π : ↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1) →ₐ[K] A) (hπ : Function.Surjective ⇑π) : ∃ (n : ℕ) (ι : ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin n) => 1) →ₐ[K] ↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1)), (∀ (x : ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin n) => 1)), ‖ι x‖ = ‖x‖) ∧ Function.Injective ⇑(π.comp ι) ∧ (π.comp ι).Finite

Affinoid Noether normalisation through a presentation. For a Tate presentation π of a nonzero algebra there is a map ι : K⟨Y₁, …, Y_d⟩ → K⟨X₁, …, Xₙ⟩ of Tate algebras, preserving Gauss norms, such that π ∘ ι is finite and injective.

theorem AlgHom.exists_finite_injective_map_unitClosedBall_le {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {σ : Type u_2} [_root_.Finite σ] {A : Type u_3} [CommRing A] [Algebra K A] [Nontrivial A] (π : ↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1) →ₐ[K] A) (hπ : Function.Surjective ⇑π) : ∃ (n : ℕ) (g : ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin n) => 1) →ₐ[K] A), Function.Injective ⇑g ∧ g.Finite ∧ Subring.map g.toRingHom (Subring.unitClosedBall ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin n) => 1)) ≤ Subring.map π.toRingHom (Subring.unitClosedBall ↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1))

Affinoid Noether normalisation adapted to a presentation. For a Tate presentation π of a nonzero algebra, a finite injective map g from a Tate algebra can be chosen to send the Gauss unit ball into the image under π of the Gauss unit ball.