The maximum modulus principle for affinoid algebras

Let A be a nonzero affinoid algebra over a complete nonarchimedean field K. For every f : A the supremum |f|sup of the absolute values |f(x)| over the classical points x of A is attained: there is a maximal ideal x of A with |f(x)| = |f|sup. For the Tate algebra Tₙ = K⟨X₁, …, Xₙ⟩ the supremum seminorm is moreover the Gauss norm.

For Tₙ, a series f attains its Gauss norm at a point whose coordinates are m-th roots of unity in the cyclotomic extension E = K(μₘ), for a suitable m of norm one (MvPowerSeries.exists_norm_restrictedEval₂_eq_norm). The field E is finite over K and carries the spectral norm, so the kernel of evaluation at that point is a classical point x of Tₙ, at which |f(x)| is the norm of the value in E.

For a general affinoid algebra, |f|sup is attained on the quotient by a minimal prime, so it suffices to treat an affinoid domain B. Choose a finite injective map Tₙ → B, and let X ^ d + ∑_{i < d} aᵢ X ^ i be the minimal polynomial of f over the integrally closed domain Tₙ. Then |f|sup = max_{i < d} |aᵢ|sup ^ (1 / (d - i)); take an index i realising the maximum, and a classical point x of Tₙ with |aᵢ(x)| = |aᵢ|sup. A root of largest absolute value of the reduction of the minimal polynomial at x is the value of f at a classical point y of B, and |f|sup ≤ |aᵢ(x)| ^ (1 / (d - i)) ≤ |f(y)|.

Main results

• TauCeti.MvPowerSeries.exists_pointNorm_eq_norm: a Tate series attains its Gauss norm at a classical point.
• TauCeti.MvPowerSeries.supSeminorm_eq_norm: on a Tate algebra the supremum seminorm is the Gauss norm.
• TauCeti.IsAffinoidAlgebra.exists_pointNorm_eq_supSeminorm: the maximum modulus principle, the supremum seminorm of a nonzero affinoid algebra is attained at a classical point.

References

• [Bosch, Güntzer, Remmert, Non-Archimedean Analysis][bosch-guntzer-remmert], §5.1.4 and §6.2.1, Proposition 4.

theorem TauCeti.MvPowerSeries.exists_pointNorm_eq_norm {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {n : ℕ} (f : ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin n) => 1)) : ∃ (x : MaximalSpectrum ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin n) => 1)), pointNorm K x f = ‖f‖

Maximum modulus principle for Tate algebras. Every series f ∈ K⟨X₁, …, Xₙ⟩ attains its Gauss norm at a classical point: |f(x)| = ‖f‖ for some maximal ideal x.

@[simp]

theorem TauCeti.MvPowerSeries.supSeminorm_eq_norm {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {n : ℕ} (f : ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin n) => 1)) : supSeminorm K f = ‖f‖

On a Tate algebra the supremum seminorm is the Gauss norm: |f|sup = ‖f‖.

theorem TauCeti.IsAffinoidAlgebra.exists_pointNorm_eq_supSeminorm {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [CommRing A] [Algebra K A] [Nontrivial A] (hA : IsAffinoidAlgebra K A) (f : A) : ∃ (x : MaximalSpectrum A), pointNorm K x f = supSeminorm K f

The maximum modulus principle. On a nonzero affinoid algebra the supremum seminorm is attained at a classical point: for every f : A there is a maximal ideal x of A with |f(x)| = |f|sup.

theorem TauCeti.IsAffinoidAlgebra.supSeminorm_lt_iff {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [CommRing A] [Algebra K A] (hA : IsAffinoidAlgebra K A) {f : A} {r : ℝ} (hr : 0 < r) : supSeminorm K f < r ↔ ∀ (x : MaximalSpectrum A), pointNorm K x f < r

By the maximum modulus principle, a positive real bounds the supremum seminorm strictly exactly when it bounds every value strictly.