Krull dimension of affinoid algebras

A nonzero affinoid algebra A over a complete nonarchimedean field is finite over an injectively embedded Tate algebra in exactly dim A variables. In particular A has finite Krull dimension, so the dimension theory of noetherian rings of finite Krull dimension applies to it.

The normalisation comes from TauCeti.IsAffinoidAlgebra.exists_finite_injective, and its number of variables is the Krull dimension by TauCeti.MvPowerSeries.ringKrullDim_eq_natCard_of_isIntegral, since finite injective extensions preserve Krull dimension.

When A is a domain, every maximal ideal m of A has height dim A. The Tate algebra T = K⟨X₁, …, Xₙ⟩ of a normalisation is a unique factorisation domain, hence integrally closed, so going down holds for the integral extension T → A of domains. Thus m has height at least that of its contraction to T, a maximal ideal of height n = dim A.

For a general affinoid algebra the corresponding statements are componentwise. Applied to the affinoid domains A ⧸ P, the domain case shows that a maximal ideal m ⊇ P has height dim (A ⧸ P) in A ⧸ P. Hence the height of m is the largest dimension of an irreducible component V(P) of Spec A through m. Components of different dimensions may occur, so a maximal ideal can have height smaller than dim A: in K⟨T⟩ × K the maximal ideal K⟨T⟩ × 0 has height zero although the ring has dimension one.

Main results

• TauCeti.IsAffinoidAlgebra.exists_ringKrullDim_eq_finite_injective: a nonzero affinoid algebra is finite over an injectively embedded Tate algebra in dim A variables.
• TauCeti.IsAffinoidAlgebra.height_eq_ringKrullDim_of_isDomain: every maximal ideal of an affinoid domain A has height dim A.
• TauCeti.IsAffinoidAlgebra.height_map_quotientMk_eq_ringKrullDim_quotient: for a prime P contained in a maximal ideal m, the image of m in A ⧸ P has height dim (A ⧸ P).
• TauCeti.IsAffinoidAlgebra.exists_mem_minimalPrimes_height_eq_ringKrullDim_quotient: the height of a maximal ideal m is the dimension of an irreducible component through m, and it bounds the dimension of every such component by TauCeti.IsAffinoidAlgebra.ringKrullDim_quotient_le_height.

References

• [Bosch, Güntzer, Remmert, Non-Archimedean Analysis][bosch-guntzer-remmert], §6.1.2.
• B. Conrad, Irreducible components of rigid spaces, Ann. Inst. Fourier 49 (1999), 473–541, Lemma 2.1.5.

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

Affinoid Noether normalisation in the dimension of the algebra. A nonzero affinoid algebra A is finite over an injectively embedded Tate algebra in n variables, where n is the Krull dimension of A. Every such normalisation has this number of variables, by TauCeti.MvPowerSeries.ringKrullDim_eq_natCard_of_isIntegral.

theorem TauCeti.IsAffinoidAlgebra.finiteRingKrullDim {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [CommRing A] [Algebra K A] [Nontrivial A] (hA : IsAffinoidAlgebra K A) : FiniteRingKrullDim A

A nonzero affinoid algebra has finite Krull dimension.

theorem TauCeti.IsAffinoidAlgebra.height_eq_ringKrullDim_of_isDomain {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [CommRing A] [Algebra K A] [IsDomain A] (hA : IsAffinoidAlgebra K A) (m : Ideal A) [m.IsMaximal] : ↑m.height = ringKrullDim A

Heights of maximal ideals of affinoid domains. Every maximal ideal of an affinoid domain A has height dim A.

theorem TauCeti.IsAffinoidAlgebra.height_map_quotientMk_eq_ringKrullDim_quotient {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [CommRing A] [Algebra K A] (hA : IsAffinoidAlgebra K A) {P m : Ideal A} [P.IsPrime] [m.IsMaximal] (hPm : P ≤ m) : ↑(Ideal.map (Ideal.Quotient.mk P) m).height = ringKrullDim (A ⧸ P)

Heights of maximal ideals on irreducible closed subsets. For a prime P of an affinoid algebra A contained in a maximal ideal m, the image of m in the affinoid domain A ⧸ P has height dim (A ⧸ P).

theorem TauCeti.IsAffinoidAlgebra.ringKrullDim_quotient_le_height {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [CommRing A] [Algebra K A] (hA : IsAffinoidAlgebra K A) {P m : Ideal A} [P.IsPrime] [m.IsMaximal] (hPm : P ≤ m) : ringKrullDim (A ⧸ P) ≤ ↑m.height

Every irreducible closed subset V(P) of Spec A through a maximal ideal m of an affinoid algebra A has dimension at most the height of m.

theorem TauCeti.IsAffinoidAlgebra.exists_mem_minimalPrimes_height_eq_ringKrullDim_quotient {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [CommRing A] [Algebra K A] (hA : IsAffinoidAlgebra K A) (m : Ideal A) [m.IsMaximal] : ∃ P ∈ minimalPrimes A, P ≤ m ∧ ↑m.height = ringKrullDim (A ⧸ P)

Heights of maximal ideals of affinoid algebras. The height of a maximal ideal m of an affinoid algebra A is the dimension of some irreducible component V(P) of Spec A through m, and is at least the dimension of every irreducible component through m, by TauCeti.IsAffinoidAlgebra.ringKrullDim_quotient_le_height. Different components through m may have different dimensions.