Krull dimension of Tate algebras

Over a complete nonarchimedean field K, the Tate algebra K⟨X₁, …, Xₙ⟩ has Krull dimension n. Consequently every ring that is integral over an injectively embedded Tate algebra K⟨X₁, …, X_d⟩ has Krull dimension d. Applied to the finite injective maps given by Noether normalisation, this identifies the number of variables of a normalisation of an affinoid algebra with its Krull dimension.

The proof is by induction on the number of variables, writing K⟨X, Y⟩ as the univariate Tate algebra K⟨X⟩⟨Y⟩.

• Lower bound. Setting Y = 0 is a surjection K⟨X⟩⟨Y⟩ → K⟨X⟩ killing the non-zero-divisor Y, so dim K⟨X⟩ + 1 ≤ dim K⟨X, Y⟩.
• Upper bound. For a nonzero f, an automorphism makes f distinguished in Y, and Weierstrass division makes K⟨X, Y⟩ ⧸ (f) finite over K⟨X⟩, so dim K⟨X, Y⟩ ⧸ (f) ≤ dim K⟨X⟩. A chain of primes of length k + 1 gives a chain of length k above a nonzero element, so dim K⟨X, Y⟩ ≤ dim K⟨X⟩ + 1.

The same induction shows that every maximal ideal M of K⟨X₁, …, Xₙ⟩ has height n. Choose a nonzero f ∈ M and make it distinguished in Y. Then K⟨X, Y⟩ ⧸ (f) is finite free over K⟨X⟩, so going down holds for it, as for every flat extension. The image of M lies over a maximal ideal of K⟨X⟩, of height n - 1, so going down gives it height at least n - 1. Quotienting by the non-zero-divisor f lowers heights by one, so M has height at least n.

The maximal-ideal height proof follows the finite-variable induction and transport under renaming of MvPolynomial.height_eq_natCard_of_isMaximal in TauCeti.RingTheory.KrullDimension.FiniteType. Its Jacobson-ring step is replaced here by Weierstrass quotients and going down for finite free extensions.

Main results

• TauCeti.MvPowerSeries.ringKrullDim_isRestricted_subring: the Tate algebra in the variables σ, for finite σ, has Krull dimension Nat.card σ.
• TauCeti.MvPowerSeries.ringKrullDim_eq_natCard_of_isIntegral: a ring that is integral over an injectively embedded Tate algebra in the variables σ has Krull dimension Nat.card σ.
• Ideal.height_eq_natCard_of_isMaximal_isRestricted_subring: every maximal ideal of the Tate algebra in the variables σ has height Nat.card σ.

References

• [Bosch, Güntzer, Remmert, Non-Archimedean Analysis][bosch-guntzer-remmert], §§5.2.2 and 6.1.2.

theorem TauCeti.MvPowerSeries.ringKrullDim_isRestricted_subring {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {σ : Type u_2} [Finite σ] : ringKrullDim ↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1) = ↑(Nat.card σ)

Krull dimension of Tate algebras. Over a complete nonarchimedean field K, the Tate algebra K⟨X₁, …, Xₙ⟩ in finitely many variables has Krull dimension n.

instance TauCeti.MvPowerSeries.finiteRingKrullDim {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {σ : Type u_2} [Finite σ] : FiniteRingKrullDim ↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1)

The Tate algebra in finitely many variables has finite Krull dimension.

theorem TauCeti.MvPowerSeries.ringKrullDim_eq_natCard_of_isIntegral {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {σ : Type u_2} [Finite σ] {A : Type u_3} [CommRing A] [Algebra (↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1)) A] [Algebra.IsIntegral (↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1)) A] [FaithfulSMul (↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1)) A] : ringKrullDim A = ↑(Nat.card σ)

The degree of a normalisation is the Krull dimension. A ring that is integral over an injectively embedded Tate algebra K⟨X₁, …, X_d⟩ has Krull dimension d. This applies to the finite injective maps from Tate algebras supplied by Noether normalisation, TauCeti.IsAffinoidAlgebra.exists_finite_injective.

@[simp]

theorem Ideal.height_eq_natCard_of_isMaximal_isRestricted_subring {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {σ : Type u_2} [Finite σ] (M : Ideal ↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1)) [M.IsMaximal] : M.height = ↑(Nat.card σ)

Heights of maximal ideals of Tate algebras. Over a complete nonarchimedean field, every maximal ideal of the Tate algebra K⟨X₁, …, Xₙ⟩ has height n, its Krull dimension.