Assemble canonical and global Berkovich spaces

[dagurtomas]

Parent and dependencies

Final assembly subtask of #21, split from draft PR #34. Depends directly on #37, #38, #39, and #40, and therefore indirectly on the reusable G-site/G-ringed infrastructure in #35. Comparator targets were added or clarified in d960950.

Goal

Assemble canonical affinoid Berkovich spaces and then the global Berkovich-space category from the accepted ordinary locally ringed, analytic-domain, point-model, and analytic-sheaf layers.

Primary comparator target

• BerkovichSpace.toLocallyRingedSpaceOfAffinoidIso

Existing downstream targets

The final public-space projection adapters transferred from completed #37:

• BerkovichSpace.locallyRingedSpaceFunctor;
• BerkovichSpace.toLocallyRingedSpace;
• BerkovichSpace.pointHomeomorphToLocallyRingedSpace;
• BerkovichSpace.locallyRingedSpaceFunctorFaithful;
• pointHomeomorphToLocallyRingedSpace_naturality.

The canonical-affinoid and global targets:

• BerkovichSpace.ofAffinoid
• globalSectionsOfAffinoidEquiv
• pointsOfAffinoidHomeomorph
• AffinoidDomain.model and modelIso
• ofAffinoidMap, identity/composition, and point naturality
• goodness, strictness, paracompactness, and Hausdorffness of affinoid objects

Scope

1. Define the public Berkovich-space bundle with a projection to the completed ordinary locally ringed core from Implement the ordinary Berkovich locally ringed core #37, together with the analytic-domain/G-ringed and affinoid-atlas data from Build reusable G-site/G-ringed infrastructure and its rigid instantiation #35/Instantiate the G-site framework for Berkovich analytic domains #38.
2. Construct the canonical object attached to a strict affinoid algebra using the point and sheaf models from Construct the universe-controlled affinoid Berkovich point model #39/Construct the affinoid Berkovich structure sheaf and local stalks #40.
3. Identify its underlying ordinary locally ringed space with the object from Construct the affinoid Berkovich structure sheaf and local stalks #40.
4. Prove compatibility between its ordinary-open sheaf and analytic-domain G-sheaf.
5. Construct affinoid maps from algebra homomorphisms and prove functoriality.
6. Only then replace the corresponding Development bodies.

Explicit exclusions

• Do not redefine the G-site or G-ringed infrastructure owned by Build reusable G-site/G-ringed infrastructure and its rigid instantiation #35.
• Do not independently reconstruct the Berkovich analytic-domain topology from Instantiate the G-site framework for Berkovich analytic domains #38.
• Do not replace the specific analytic sheaf from Construct the affinoid Berkovich structure sheaf and local stalks #40 with arbitrary sheaf data.

Acceptance criteria

• No custom duplicate of mathlib locally ringed spaces or Build reusable G-site/G-ringed infrastructure and its rigid instantiation #35's G-ringed infrastructure.
• No affinoid domain is assumed open merely to use ordinary restriction APIs.
• The ordinary and admissible/G-topological sheaf presentations are compatible.
• No comparator target is closed by a point-only or arbitrary-sheaf scaffold.
• Production files contain no sorry and all required project checks pass.