Develop analytic functions on Berkovich rational and affinoid domains

[dagurtomas]

Goal

Extend the existing compact rational-domain loci and localization-spectrum homeomorphism to analytic function rings, restriction maps, and affinoid-domain models.

Existing foundations

• relative Berkovich spectra and completed residue fields;
• rational-domain compactness and denominator nonvanishing;
• rational localizations and their spectrum homeomorphism.

Dependencies

Coordinate-ring sheaf results may use Tate acyclicity (#20). Coordinate this issue with the global Berkovich core (#21).

This issue is available to claim. Comment before starting so it can be relabeled claimed.