Maximal ideals of affinoid algebras

The residue field at every maximal ideal of an affinoid algebra over a complete ultrametric field is finite over the ground field. Consequently, an algebra map into an affinoid algebra contracts maximal ideals to maximal ideals, even when its source is not affinoid. This gives the contravariant map on maximal spectra used for classical points of affinoid spaces, which is surjective for integral injective maps; so residue fields of an integral subalgebra of an affinoid algebra are finite over the ground field as well. Every affinoid algebra is moreover a Jacobson ring, so its maximal ideals, the classical points, determine every radical ideal: each prime ideal is the intersection of the maximal ideals containing it.

The residue-field finiteness is the affinoid form of the Tate-algebra Nullstellensatz proved in TauCeti.RingTheory.MvPowerSeries.TateAlgebra.Nullstellensatz, and the Jacobson property descends from TauCeti.MvPowerSeries.isJacobsonRing along a presentation.

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

The residue field of a maximal ideal of an affinoid algebra is finite over the ground field.

theorem TauCeti.IsAffinoidAlgebra.isJacobsonRing {K : Type u} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type v} [CommRing A] [Algebra K A] (hA : IsAffinoidAlgebra K A) : IsJacobsonRing A

Affinoid algebras are Jacobson rings. Every prime ideal of an affinoid algebra is the intersection of the maximal ideals containing it.

theorem TauCeti.IsAffinoidAlgebra.comap_isMaximal {K : Type u} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type v} [CommRing A] [Algebra K A] {B : Type w} [CommRing B] [Algebra K B] (hB : IsAffinoidAlgebra K B) (f : A →ₐ[K] B) (m : Ideal B) [m.IsMaximal] : (Ideal.comap f m).IsMaximal

An algebra map into an affinoid algebra contracts a maximal ideal to a maximal ideal. The source algebra need not itself be affinoid.

def TauCeti.IsAffinoidAlgebra.maximalSpectrumComap {K : Type u} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type v} [CommRing A] [Algebra K A] {B : Type w} [CommRing B] [Algebra K B] (hB : IsAffinoidAlgebra K B) (f : A →ₐ[K] B) : MaximalSpectrum B → MaximalSpectrum A

The contravariant map on maximal spectra induced by an algebra map whose target is affinoid.

@[simp]

theorem TauCeti.IsAffinoidAlgebra.maximalSpectrumComap_asIdeal {K : Type u} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type v} [CommRing A] [Algebra K A] {B : Type w} [CommRing B] [Algebra K B] (hB : IsAffinoidAlgebra K B) (f : A →ₐ[K] B) (x : MaximalSpectrum B) : (hB.maximalSpectrumComap f x).asIdeal = Ideal.comap f x.asIdeal

@[simp]

theorem TauCeti.IsAffinoidAlgebra.maximalSpectrumComap_id {K : Type u} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type v} [CommRing A] [Algebra K A] (hA : IsAffinoidAlgebra K A) : hA.maximalSpectrumComap (AlgHom.id K A) = id

@[simp]

theorem TauCeti.IsAffinoidAlgebra.maximalSpectrumComap_comp {K : Type u} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type v} [CommRing A] [Algebra K A] {B : Type w} [CommRing B] [Algebra K B] {C : Type u_1} [CommRing C] [Algebra K C] (hB : IsAffinoidAlgebra K B) (hC : IsAffinoidAlgebra K C) (f : A →ₐ[K] B) (g : B →ₐ[K] C) : hC.maximalSpectrumComap (g.comp f) = hB.maximalSpectrumComap f ∘ hC.maximalSpectrumComap g

theorem TauCeti.IsAffinoidAlgebra.maximalSpectrumComap_injective {K : Type u} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type v} [CommRing A] [Algebra K A] {B : Type w} [CommRing B] [Algebra K B] (hB : IsAffinoidAlgebra K B) (f : A →ₐ[K] B) (hf : Function.Surjective ⇑f) : Function.Injective (hB.maximalSpectrumComap f)

A surjective algebra map into an affinoid algebra induces an injective map on maximal spectra.

theorem TauCeti.IsAffinoidAlgebra.maximalSpectrumComap_surjective {K : Type u} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type v} [CommRing A] [Algebra K A] {B : Type w} [CommRing B] [Algebra K B] (hB : IsAffinoidAlgebra K B) (f : A →ₐ[K] B) (hf : f.IsIntegral) (hfi : Function.Injective ⇑f) : Function.Surjective (hB.maximalSpectrumComap f)

An integral injective algebra map into an affinoid algebra induces a surjective map on maximal spectra.

theorem TauCeti.IsAffinoidAlgebra.finite_quotient_of_isIntegral {K : Type u} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type v} [CommRing A] [Algebra K A] {B : Type w} [CommRing B] [Algebra K B] (hB : IsAffinoidAlgebra K B) (f : A →ₐ[K] B) (hf : f.IsIntegral) (hfi : Function.Injective ⇑f) (m : Ideal A) [m.IsMaximal] : Module.Finite K (A ⧸ m)

The residue field of a maximal ideal of A is finite over the ground field when A maps integrally and injectively into an affinoid algebra, since the ideal lies under a maximal ideal of the affinoid algebra. The source algebra need not itself be affinoid.