Develop maximal-spectrum topology and residue fields

[dagurtomas]

Goal

Develop the topology and residue-field API of the maximal spectrum of an affinoid algebra.

Suggested scope:

• relate MaximalSpectrum A to the closed points of PrimeSpectrum A;
• provide the induced Zariski topology and continuity of contravariant pullback;
• package residue fields at maximal ideals and their finite-dimensionality over the ground field;
• expose reusable functoriality lemmas for later rigid-affinoid point constructions.

Build on Rigid/AffinoidAlgebra/MaximalSpectrum.lean and the existing affinoid Nullstellensatz/finite-quotient results. This is independent of the current global-space cores and Tate acyclicity.

Comment claimed before starting.