Draft: prototype global Berkovich-space core

[dagurtomas]

Status

Early draft — currently does not compile and must not be merged. Tracks #21.

This preserves the Berkovich-space agent's partial implementation for review. It does not replace any comparator sorry.

Implemented prototype

• PreBerkovichSpace, a locally ringed topological-space interface;
• sections, restrictions, gluing, stalks, and germs;
• analytic morphism data with identity and composition;
• category and underlying-topological-space functors;
• an attempted affinoid core using the relative Berkovich spectrum;
• affinoid chart and atlas structures;
• a proposed public BerkovichSpace bundle and morphism/category API.

Current build blocker

lake build -q Rigid.Berkovich.Space first fails while constructing AffinoidBerkovichCore: AffinoidAlgebraModel supplies only CommRing and Algebra, while BerkovichSpectrumOver needs the normed/complete structures associated to an affinoid presentation. Errors after that point are cascading unknown-declaration failures.

Required redesign before merge

• Obtain the canonical normed and complete structures from an affinoid presentation without introducing conflicting instances.
• Define the affinoid structure sheaf rather than leaving arbitrary sheaf/stalk fields on an object whose point space happens to be a Berkovich spectrum.
• Derive stalks from that sheaf or state their universal property.
• Express charts as genuine locally ringed-space open embeddings/local isomorphisms.
• Review the duplicated category/morphism layer and adapt the comparator only after a canonical affinoid object exists.
• Resolve the current linter warnings.

Checks

Passed:

• ./scripts/check_root_imports.sh
• ./scripts/check_challenge_development.sh
• git diff --check
• no sorry in Rigid/Berkovich/Space.lean

Failing as described above:

• lake build -q Rigid.Berkovich.Space
• consequently lake build -q Rigid

[dagurtomas]

Review confirms that this prototype is too broad for one implementation track. It also has two architectural problems: PreBerkovichSpace duplicates mathlib's locally ringed-space API, and affinoid domains are represented as ordinary opens even though general Berkovich affinoid domains need not be open.

The work is now split into:

• Implement the ordinary Berkovich locally ringed core #37 — mathlib LocallyRingedSpace bridge;
• Instantiate the G-site framework for Berkovich analytic domains #38 — analytic-domain G-topology;
• Construct the universe-controlled affinoid Berkovich point model #39 — universe-controlled affinoid point model;
• Construct the affinoid Berkovich structure sheaf and local stalks #40 — affinoid structure sheaf and local stalks;
• Assemble canonical and global Berkovich spaces #41 — canonical/global assembly and functoriality.

Commit d960950 adds matching Challenge/Development targets for these boundaries. This draft remains useful as an archive of proof shapes and naming experiments, but new implementation should proceed on the focused issues rather than extending the custom scaffold.