Finite infinitesimal quotients of affinoid algebras

An affinoid algebra over a complete nonarchimedean field is noetherian. Its quotient by any ideal with maximal radical is finite over the coefficient field; in particular, this applies to every positive power of a maximal ideal. Combined with Ideal.iInf_isMaximal_pow_eq_bot, these finite quotients separate elements of the algebra. These are the algebraic inputs to the closed-graph argument for automatic continuity.

No norm or topology on the affinoid algebra is selected. The results include nonreduced and zero algebras, and the zeroth-power quotient is included in the finite-power statement.

References

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

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

Every affinoid algebra over a complete nonarchimedean field is noetherian.

theorem TauCeti.IsAffinoidAlgebra.finite_quotient_of_isMaximal_radical {K : Type u_1} {A : Type u_2} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] [CommRing A] [Algebra K A] (hA : IsAffinoidAlgebra K A) (I : Ideal A) [I.radical.IsMaximal] : Module.Finite K (A ⧸ I)

An affinoid quotient whose defining ideal has maximal radical is finite over the coefficient field.

theorem TauCeti.IsAffinoidAlgebra.finite_quotient_pow {K : Type u_1} {A : Type u_2} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] [CommRing A] [Algebra K A] (hA : IsAffinoidAlgebra K A) (m : Ideal A) [m.IsMaximal] (n : ℕ) : Module.Finite K (A ⧸ m ^ n)

Quotients of an affinoid algebra by all powers of a maximal ideal are finite over the coefficient field, including the zero quotient for exponent zero.